Abstract
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.
This research was supported by IISI, Cornell University (AFOSR grant FA9550-04-1-0151), NSF Expeditions in Computing award for Computational Sustainability (Grant 0832782) and NSF IIS award (Grant 0514429). Part of this work was done while the second author was visiting McGill University.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in AI and Applications, vol. 185. IOS Press, Amsterdam (2009)
Eén, N., Sörensson, N.: MiniSat: A SAT solver with conflict-clause minimization. In: 8th SAT, St. Andrews, UK (June 2005)
Gerevini, A., Dimopoulos, Y., Haslum, P., Saetti, A. (Organizers): IPC-5 international planning competition (June 2006), http://zeus.ing.unibs.it/ipc-5
Kautz, H.A., Selman, B.: BLACKBOX: A new approach to the application of theorem proving to problem solving. In: Workshop on Planning as Combinatorial Search, held in conjunction with AIPS 1998, Pittsburgh, PA (1998)
Kroc, L., Sabharwal, A., Gomes, C.P., Selman, B.: Integrating systematic and local search paradigms: A new strategy for MaxSAT. In: 21st IJCAI (July 2009)
Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. JAIR 30 (2007)
Li, C.M., Wei, W., Zhang, H.: Combining adaptive noise and look-ahead in local search for SAT. In: 10th SAT, Lisbon, Portugal, May 2007, pp. 121–133 (2007)
Marques-Silva, J.P., Manquinho, V.M.: Towards more effective unsatisfiability-based maximum satisfiability algorithms. In: 11th SAT, May 2008, pp. 225–230 (2008)
Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. In: The Second DIMACS Implementation Challenge, pp. 521–532 (1996)
Sinz, C. (Organizer).: SAT-race 2008 (May 2008)
Tompkins, D.A.D., Hoos, H.H.: Scaling and probabilistic smoothing: Dynamic local search for unweighted MAX-SAT. In: 16th Canadian AI, pp. 145–159 (2003)
Tompkins, D.A.D., Hoos, H.H.: UBCSAT: An impl. and experim. env. for SLS algorithms for SAT and MAX-SAT. In: 7th SAT, Vancouver, BC (May 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kroc, L., Sabharwal, A., Selman, B. (2009). Relaxed DPLL Search for MaxSAT. In: Kullmann, O. (eds) Theory and Applications of Satisfiability Testing - SAT 2009. SAT 2009. Lecture Notes in Computer Science, vol 5584. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02777-2_41
Download citation
DOI: https://doi.org/10.1007/978-3-642-02777-2_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02776-5
Online ISBN: 978-3-642-02777-2
eBook Packages: Computer ScienceComputer Science (R0)