Seeking practical CDCL insights from theoretical SAT benchmarks
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Seeking practical CDCL insights from theoretical SAT benchmarks. / Elffers, Jan; Cru, Jesús Giráldez; Gocht, Stephan; Nordström, Jakob; Simon, Laurent.
Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018. ed. / Jerome Lang. International Joint Conferences on Artificial Intelligence, 2018. p. 1300-1308 (IJCAI International Joint Conference on Artificial Intelligence, Vol. 2018-July).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Seeking practical CDCL insights from theoretical SAT benchmarks
AU - Elffers, Jan
AU - Cru, Jesús Giráldez
AU - Gocht, Stephan
AU - Nordström, Jakob
AU - Simon, Laurent
PY - 2018
Y1 - 2018
N2 - Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.
AB - Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.
UR - http://www.scopus.com/inward/record.url?scp=85055682692&partnerID=8YFLogxK
U2 - 10.24963/ijcai.2018/181
DO - 10.24963/ijcai.2018/181
M3 - Article in proceedings
AN - SCOPUS:85055682692
T3 - IJCAI International Joint Conference on Artificial Intelligence
SP - 1300
EP - 1308
BT - Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
A2 - Lang, Jerome
PB - International Joint Conferences on Artificial Intelligence
T2 - 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
Y2 - 13 July 2018 through 19 July 2018
ER -
ID: 251867360