A Computational Study of Satisfiability Algorithms for Propositional Logic

We implement several recent algorithms for the satisfiabiiity problem in propositional logic and test them on a wide variety of benchmark problems. We focus on algorithms based on some kind of tree search, including three versions of the classical Davis-Putnam-Loveland method, the method of Jeroslow and Wang, the Horn Relaxation method of Gallo and Urbani, the branch and cut method of Hooker and Fedjki, and the column subtraction method of Harche and Thompson. We design experiments so as to identify the important factors that influence the performance of tree search algorithms. We find that the choice of which variable to branch on is a key factor. Methods based on weak relaxations (e.g., Horn relaxation) are best for easy problems, and the column subtraction method is clearly the most robust, as it was the only algorithm to solve the hardest problems. if Davis-Putnam-Loveland is properly implemented, it and the remaining methods generally excel on problems that are neither too easy nor too hard.

INFORMS Journal on Computing, ISSN 1091-9856, was published as ORSA Journal on Computing from 1989 to 1995 under ISSN 0899-1499.