Yesterday I spent some time on unification which is a building block of Prolog programs. Another important concept used in Prolog is satisfiability of propositional formulae.

In general, propositional formulae satisfiability, or SAT problem, is…