Algorithms for testing the satisfiability of propositional formulae

AbstractThe best-known algorithm for the satisfiability problem in the case of propositional formulae (SAT) is the implicit enumeration version of the Davis–Putnam algorithm, as described in Loveland's book. We review this algorithm, which we call DPL, and some recent variants. As it is often the case with enumerative algorithms for decision type problems, neither DPL nor its variants incorporate any effective device to prune the search tree. We investigate the idea of using the solution of related subproblems as such a pruning device. It is well known that HORN-SAT, the satisfiability problem in the case of Horn clauses, is easy: in fact an algorithm, DG, has been proposed by Dowling and Gallier, which solves HORN-SAT in linear time. Here we show by means of a set of experiments that the efficiency of DG is not only theoretical but practical as well. In fact we show that on a set of randomly generated problems the complexity of DG grows almost linearly with the problem size, while, for instance, the complexity of the unit resolution approach grows almost quadratically. Then we propose two relaxation schemes which map instances of SAT into instances of HORN-SAT; such relaxation schemes are used to derive two new enumerative algorithms for SAT: HORN1 and HORN2. These algorithms have been compared experimentally with DPL and with its variants. Our results show that HORN2 outperforms the other algorithms; in particular it runs several times faster than DPL on almost all the test problems we have generated