A computational study of satisfiability algorithms for propositional logic

A computational study of satisfiability algorithms for propositional logic

0.00 Avg rating0 Votes
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: , ,
Keywords: logic
Abstract:

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.

Reviews

Required fields are marked *. Your email address will not be published.