A Comparison of CP, IP, and SAT Solvers through a Common Interface

This paper presents a common interface for Prolog to three different types of discrete solvers including Constraint Programming (CP), Integer Programming (IP), and SAT solvers. The interface comprises primitives for creating decision variables, specifying constraints, and invoking a solver, possibly with an objective function to be optimized. Before a solver is actually called, the accumulated variables and constraints are transformed into a form acceptable to the solver. For a SAT solver, in particular, variables are Booleanized and constraints are compiled into CNF. Implemented in B-Prolog, the interface allows the programmer to use the features of the host language such as recursion, pattern matching, arrays, and loops to describe problems. The interface provides an easy and uniform platform for exploring different solvers and models. This paper compares the performance of the CLP(FD) of B-Prolog, the CPLEX IP solver, and the Lingeling SAT solver on several problems through the same interface and for each problem it compares a model that uses Boolean variables and another model that uses general integer variables. Our experience tells that it is effortless to switch from one solver to another.