04/01/1995 09:00 AM
Computer Science
A new algorithm for testing satisfiability of propositional formulas in conjunctive normal form (CNF) is described. It applies reasoning in the form of certain resolution operations, and identification of equivalent literals. Resolution produces growth in the size of the formula, but within a global quadratic bound; most previous methods avoid operations that produce any growth, and generally do not identify equivalent literals. Computational experience indicates that the method does substantially less ``guessing\'\' than previously reported algorithms, while keeping a polynomial time bound on the work done between guesses. Experiments indicate that, for larger problems, the time investment in reasoning returns a profit in reduced searching, and the profit increases with increasing problem size. Experimental data compares six branching strategies of the proposed algorithm on a variety of problems, including several Dimacs benchmarks. These branching strategies were shown to perform differently with statistical significance. A new scheme based on Johnson\'s maximum satisfiability approximation algorithm was found to be the best overall. Both satisfiable and unsatisfiable random 3-CNF formulas with 50--283 variables and 4.27 ratio of clauses to variables have been tested; this class is generally acknowledged to be relatively ``hard\'\' and required extensive backtracking by other algorithms. Unsatisfiable random problems were found to deviate from the easy-hard-easy pattern. The new algorithm solves random formulas with surprisingly little backtracking: the average number of guesses was 3,267 for 200 variables at this ratio, and 57,503 for 283 variables. Larger unsatisfiable formulas from circuit-fault analysis, with 500--12,800 variables were solved with no backtracking in some cases. Extensive statistics on guesses and time are reported. Statistical and experimental techniques and traps are discussed. An exponential growth rate for random formulas is estimated.
