出版社：Institute for Operations Research and the Management Sciences
摘要：Finding a feasible as opposed to optimal solution of an integer program model comes under the heading of constraint programming and if a model is also a binary integer program (BIP) it is known to be equivalent to the satisfiability (SAT) problem from Boolean logic. Many of the puzzles treated in this column over the years and a host of others fall into this category, that is, they may be modeled purely using binary variables and the aim is to fulfil the conditions of the puzzle rather than to optimize a function. This leads to the possibility that there may be gains in efficiency to be found by looking beyond general IP solvers to more specialized programs. The following article presents five puzzles together with IP formulations where the writer has experienced significant improvements in solution times using a SAT solver rather than a general purpose IP solver. The puzzles will be modeled and solved using three freely available open source packages, namely GLPK, Minisat and SCIP. GLPK and Minisat are both available in the GUSEK distribution from http://gusek.sourceforge.net/gusek.html and SCIP is available from http://scip.zib.de/ . GLPK is a general purpose linear and mixed integer solver, SCIP solves both Integer Programs and Constraint Programs and Minisat is exclusively an SAT solver. The GUSEK environment provides direct access to GLPK and Minisat. It also has the option to generate MPS formatted files of Mathprog models which may be read into SCIP and solved.
