Article ID: | iaor19982328 |
Country: | United States |
Volume: | 6 |
Issue: | 4 |
Start Page Number: | 423 |
End Page Number: | 435 |
Publication Date: | Sep 1994 |
Journal: | ORSA Journal On Computing |
Authors: | Hooker J.N., Thompson G.L., Harche F. |
Keywords: | logic |
We implement several recent algorithms for the satisfiability problem in propositional logic and test them on a wide variety of benchmark problems. We focus on algorithms based on some tkind 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.