A two-phase algorithm for solving a class of hard satisfiability problems

The DIMACS suite of satisfiability 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–Logemann–Loveland algorithm. We conclude with reporting on our computational results on the parity instances.