Using Resolution Proofs to Analyse CDCL Solvers

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceeding


We propose that CDCL SAT solver heuristics such as restarts and clause database management can be analysed by studying the resolution proofs produced by the solvers, and by trimming these proofs to extract the clauses actually used to reach the final conclusion. We find that for non-adaptive Luby restarts higher frequency makes both untrimmed and trimmed proofs smaller, while adaptive restarts based on literal block distance (LBD) decrease proof size further mainly for untrimmed proofs. This seems to indicate that restarts improve the reasoning power of solvers, but that making restarts adaptive mainly helps to avoid useless work that is not needed to reach the end result. For clause database management we find that switching off clause erasures often, though not always, leads to smaller untrimmed proofs, but has no significant effect on trimmed proofs. With respect to quality measures for learned clauses, activity in conflict analysis is a fairly good predictor in general for a clause ending up also in the trimmed proof, whereas for the very best clauses the LBD score gives stronger correlation. This gives more rigorous support for the currently popular heuristic of prioritizing clauses with very good LBD scores but sorting the rest of the clauses with respect to activity when deciding which clauses to erase. We remark that for these conclusions, it is crucial to use the actual proof found by the solver rather than the one reconstructed from the DRAT proof log.


Enheter & grupper
Externa organisationer
  • University of Copenhagen

Ämnesklassifikation (UKÄ) – OBLIGATORISK

  • Datavetenskap (datalogi)
Titel på värdpublikationPrinciples and Practice of Constraint Programming - 26th International Conference, CP 2020, Proceedings
RedaktörerHelmut Simonis
Antal sidor18
ISBN (tryckt)9783030584740
StatusPublished - 2020
Peer review utfördJa
Evenemang26th International Conference on Principles and Practice of Constraint Programming, CP 2020 - Louvain-la-Neuve, Belgien
Varaktighet: 2020 sep 72020 sep 11


NamnLecture Notes in Computer Science
ISSN (tryckt)0302-9743
ISSN (elektroniskt)1611-3349


Konferens26th International Conference on Principles and Practice of Constraint Programming, CP 2020