Using Resolution Proofs to Analyse CDCL Solvers
(2020) 26th International Conference on Principles and Practice of Constraint Programming, CP 2020 In Lecture Notes in Computer Science 12333. p.427-444- Abstract
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... (More)
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.
(Less)
- author
- Kokkala, Janne I. LU and Nordström, Jakob LU
- organization
- publishing date
- 2020
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Proceedings
- series title
- Lecture Notes in Computer Science
- editor
- Simonis, Helmut
- volume
- 12333
- pages
- 18 pages
- publisher
- Springer
- conference name
- 26th International Conference on Principles and Practice of Constraint Programming, CP 2020
- conference location
- Louvain-la-Neuve, Belgium
- conference dates
- 2020-09-07 - 2020-09-11
- external identifiers
-
- scopus:85091284248
- ISSN
- 0302-9743
- 1611-3349
- ISBN
- 9783030584740
- DOI
- 10.1007/978-3-030-58475-7_25
- language
- English
- LU publication?
- yes
- id
- 9b09658a-006e-45e4-ae90-c557cf25b672
- date added to LUP
- 2020-10-28 10:33:35
- date last changed
- 2024-05-15 19:42:30
@inproceedings{9b09658a-006e-45e4-ae90-c557cf25b672,
abstract = {{<p>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.</p>}},
author = {{Kokkala, Janne I. and Nordström, Jakob}},
booktitle = {{Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Proceedings}},
editor = {{Simonis, Helmut}},
isbn = {{9783030584740}},
issn = {{0302-9743}},
language = {{eng}},
pages = {{427--444}},
publisher = {{Springer}},
series = {{Lecture Notes in Computer Science}},
title = {{Using Resolution Proofs to Analyse CDCL Solvers}},
url = {{http://dx.doi.org/10.1007/978-3-030-58475-7_25}},
doi = {{10.1007/978-3-030-58475-7_25}},
volume = {{12333}},
year = {{2020}},
}