Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
A long line of research has studied the power of conflict-driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adver
- PDF / 571,326 Bytes
- 17 Pages / 439.37 x 666.142 pts Page_size
- 36 Downloads / 139 Views
KTH Royal Institute of Technology, Stockholm, Sweden {elffers,jakobn,vinyals}@kth.se Ludwig-Maximilians-Universit¨ at M¨ unchen, Munich, Germany [email protected] 3 Universitat Polit`ecnica de Catalunya, Barcelona, Spain [email protected] 4 ´ Ecole Normale Sup´erieure, Paris, France [email protected]
Abstract. A long line of research has studied the power of conflictdriven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgotten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that captures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL without any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.
1
Introduction
For two decades the dominant strategy for solving the Boolean satisfiability problem (SAT) in practice has been conflict-driven clause learning (CDCL) [5,27,28]. Although SAT is an NP-complete problem, and is hence widely believed to be intractable in the worst case, CDCL SAT solvers have turned out to be immensely successful over a wide range of application areas. An important problem is to understand how such SAT solvers can be so efficient and what theoretical limits exist on their performance. Previous Work. At the core, CDCL searches for proofs in the proof system resolution [14]. While pre- and inprocessing techniques can, and sometimes do, go c Springer International Publishing Switzerland 2016 N. Creignou and D. Le Berre (Eds.): SAT 2016, LNCS 9710, pp. 160–176, 2016. DOI: 10.1007/978-3-319-40970-2 11
Trade-offs Between Time and Memory in CDCL
161
significantly beyond resolution (incorporating, e.g., solving of linear equations mod 2 and reasoning with cardinality constraints), understanding the power of even just the fundamental CDCL algorithm seems like an interesting and challenging problem in its own right. Three crucial aspects of CDCL solvers, which are the focus of our work, are running time, memory usage, and restart policy. In resolution, time is modelled by the size/length complexity measure, in that lower bounds on proof size yield lower bounds on the running time of CDCL solvers. Resolution proof size is a well-studied measure. It is not hard to show that
Data Loading...
