A Common Interface to SAT and MP Solvers

B-Prolog provides a common interface to SAT and MP solvers. The interface comprises primitives for creating decision variables, specifying constraints, and invoking a solver, possibly with an objective function to be optimized. Users can change the invoking call in order to change the solver that a program calls. Therefore, the interface greatly facilitates experimentation with different solvers and models. When used together with other features of B-Prolog, such as arrays and loop constructs, the interface makes B-Prolog a powerful modeling language for the SAT and MP solvers.

The implementation of the interface uses attributed variables in B-Prolog in order to accumulate constraints. When a constraint is posted, it is added into the global list of constraints. The constraints are only interpreted when a solver-invoking call is executed. If the solver is SAT, then all of the variables are Booleanized, and all of the constraints are sent to the SAT solver after they are compiled into CNF. If the solver is LP/MIP, all of the constraints are converted to disequalities, and sent to the LP/MIP solver. An answer that is found by the solver is returned to B-Prolog as a group of bindings of the decision variables.

The released package of B-Prolog does not include a SAT solver. Users need to install a SAT solver separately, and must make the OS command satsolver available to B-Prolog. B-Prolog dumps the generated CNF code into a file that is named '__tmp.cnf' in the working directory, and uses the command

      system('satsolver __tmp.cnf > __tmp.res',_)

in order to solve the CNF file. The solver's result file, '__tmp.res', must only contain solution literals.