A two phase algorithm for solving a class of hard satissfiability problems

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.