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.

, , ,
Software Engineering [SEN]

Warners, J.P, & van Maaren, H. (1998). A two phase algorithm for solving a class of hard satissfiability problems. Software Engineering [SEN]. CWI.