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.