Abstract
Satisfiability solvers targeting industrial instances are currently almost always based on conflict-driven clause learning (CDCL) [5]. This technique can successfully solve very large instances. Yet on small, hard problems lookahead solvers [3] often perform better by applying much more reasoning in each search node and then recursively splitting the search space until a solution is found.
The 2nd and 3rd author are supported by FWF, NFN Grant S11408-N23 (RiSE). The 2nd author is supported by DARPA contract number N66001-10-2-4087.
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
References
Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Technical Report 10/1, Johannes Kepler University, Linz, Austria (2010)
Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. ENTCS 89(4), 543–560 (2003)
Heule, M.J.H.: SmArT Solving: Tools and techniques for satisfiability solvers. PhD thesis, Delft University of Technology (2008)
Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding CDCL SAT solvers by lookaheads, Accepted for HVC (2011)
Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT Solvers. FAIA, vol. 185, ch. 4, pp. 131–153. IOS Press (February 2009)
Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: Portfolio-based algorithm selection for sat. J. Artif. Intell. Res. (JAIR) 32, 565–606 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van der Tak, P., Heule, M.J.H., Biere, A. (2012). Concurrent Cube-and-Conquer. In: Cimatti, A., Sebastiani, R. (eds) Theory and Applications of Satisfiability Testing – SAT 2012. SAT 2012. Lecture Notes in Computer Science, vol 7317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_42
Download citation
DOI: https://doi.org/10.1007/978-3-642-31612-8_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31611-1
Online ISBN: 978-3-642-31612-8
eBook Packages: Computer ScienceComputer Science (R0)