A pearl on SAT and SMT solving in Prolog (Q428887)

A succinct and elegant solver of twenty two Prolog clauses for the Boolean satisfiability problem (SAT solver) is presented. The brevity of the program is achieved using Prolog to transform a propositional formula into a conjunctive normal form (CNF). The match between Prolog, SAT, Davis-Putnam-Logeman-Loveland (DPLL) algorithm with watched literals -- one of the most power features in speeding up SAT solvers -- promotes a lot the author's success. The solver provides an easy entry into the SAT and SAT modulo theories (SMT). The SAT solver exploits the control provided by delay declarations to implement watched literals and unit propagation. The SAT solver can be integrated into an SMT framework which uses the constraint solvers that are available in many Prolog systems. The presented SAT solver is not going to be competitive on large, difficult problems set as challenges in the international SAT and SMT competitions. Nevertheless, the solver does provide a declarative description of SAT solving with watched literals in a succinct and self-contained manner, and one which can be extended in a number of ways. For instance, its incorporation into an SMT scheme using the constraint packages often distributed with Prolog systems gives a straightforward realization of the theory of linear real arithmetic.