Two Phase Algorithm for Solving a Class of Hard Satisfiability Problems; Software engineering rept

摘要

The DIMACS suite of satisfiability (SAT) benchmarks contains a set of instances that are very hard for existing algorithms. These instances arise from learning the parity function on 32 bits. In this paper we develop a two phase algorithm that is capable of solving these instances. In the first phase, a polynomially solvable subproblem is identified and solved. Using the solution to this problem, we can considerably restrict the size of the search-space in the second phase of the algorithm, which is an extension of the well-known Davis-Putnam-Loveland algorithm for SAT problems. We conclude with reporting on our computational results on the parity instances.