Relaxed DPLL Search for MaxSAT

11 years 8 months ago
Relaxed DPLL Search for MaxSAT
We propose a new incomplete algorithm for the Maximum Satisfiability (MaxSAT) problem on unweighted Boolean formulas, focused specifically on instances for which proving unsatisfiability is already computationally difficult. For such instances, our approach is often able to identify a small number of what we call “bottleneck” constraints, in time comparable to the time it takes to prove unsatisfiability. These bottleneck constraints can have useful semantic content. Our algorithm uses a relaxation of the standard backtrack search for satisfiability testing (SAT) as a guiding heuristic, followed by a low-noise local search when needed. This allows us to heuristically exploit the power of unit propagation and clause learning. On a test suite consisting of all unsatisfiable industrial instances from SAT Race 2008, our solver, RelaxedMinisat, is the only (MaxSAT) solver capable of identifying a single bottleneck constraint in all but one instance.
Lukas Kroc, Ashish Sabharwal, Bart Selman
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SAT
Authors Lukas Kroc, Ashish Sabharwal, Bart Selman
Comments (0)