File SatSolvers.h

↰ Parent directory (ADS/backtrack)

Two solvers of the satisfiability of a formula in conjunctive normal form [see File Problems.h for the formula and the backtrack of the reductions], after Knuth (7.2.2.2), beyond the book.

Definition (ADS/backtrack/SatSolvers.h)

Detailed Description

  • dpll() is the procedure of Davis, Putnam, Logemann and Loveland: unit propagation (a clause with all its literals false but one forces it), then a branch on a literal of a shortest open clause, and back on a contradiction; the propagation scans the clauses, simple and slow.

  • Cdcl is conflict-driven clause learning (Algorithm 7.2.2.2C): each clause watches two of its literals, which need attention only when one becomes false, so that the propagation touches few clauses; a conflict is analyzed back to its first unique implication point, which gives a learned clause implied by the formula, and the search jumps back to the level where the clause forces its literal; the variables in the conflicts gain activity (VSIDS), and the decisions take the most active one, with the value it had last (phase saving); restarts follow the sequence of Luby, Sinclair and Zuckerman. The learned clauses are kept (no deletion), which suits formulae of moderate size. The heap of the variables is a parameter of BasicCdcl (Cdcl is the one on std::priority_queue), so that the same algorithm runs on the heaps of std, Boost or Namespace ADS with the same decisions and conflicts.

The contracts [see File Contract.h]: the literals are :math:` pm ( v + 1 ) ` with v in [ 0 , n ); a model returned passes satCertificate(), a postcondition. A formula declared unsatisfiable has no certificate here (a proof of the learned clauses, as DRAT, would be one). The functions are defined in SatSolvers.tpp.

    1. Knuth, The Art of Computer Programming, vol. 4B, Addison-Wesley, 2022, section 7.2.2.2

  1. Davis, H. Putnam, A computing procedure for quantification theory, Journal of the ACM 7(3), 201-215, 1960, doi:10.1145/321033.321034

  1. Davis, G. Logemann, D. Loveland, A machine program for theorem-proving, Communications of the ACM 5(7), 394-397, 1962, doi:10.1145/368273.368557

    1. Marques-Silva, K. A. Sakallah, GRASP: a search algorithm for propositional satisfiability, IEEE Transactions on Computers 48(5), 506-521, 1999, doi:10.1109/12.769433

    1. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: engineering an efficient SAT solver, DAC 2001, 530-535, doi:10.1145/378239.379017

  1. Luby, A. Sinclair, D. Zuckerman, Optimal speedup of Las Vegas algorithms, Information Processing Letters 47(4), 173-180, 1993, doi:10.1016/0020-0190(93)90029-9

  1. Pipatsrisawat, A. Darwiche, A lightweight component caching scheme for satisfiability solvers, SAT 2007, LNCS 4501, 294-299, doi:10.1007/978-3-540-72788-0_28 (phase saving)

Donato Meoli

Dipartimento di Informatica Universita’ di Pisa

by Donato Meoli

Includes

Namespaces

Classes

Functions

Typedefs