Seeking practical CDCL insights from theoretical SAT benchmarks

Jan Elffers, Jesús Giráldez Cru, Stephan Gocht, Jakob Nordström, Laurent Simon

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceedingPeer review

13 Citeringar (SciVal)

Sammanfattning

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.

Originalspråkengelska
Titel på gästpublikationProceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
RedaktörerJerome Lang
FörlagInternational Joint Conferences on Artificial Intelligence
Sidor1300-1308
Antal sidor9
ISBN (elektroniskt)9780999241127
DOI
StatusPublished - 2018
Externt publiceradJa
Evenemang27th International Joint Conference on Artificial Intelligence, IJCAI 2018 - Stockholm, Sverige
Varaktighet: 2018 jul 132018 jul 19

Publikationsserier

NamnIJCAI International Joint Conference on Artificial Intelligence
Volym2018-July
ISSN (tryckt)1045-0823

Konferens

Konferens27th International Joint Conference on Artificial Intelligence, IJCAI 2018
Land/TerritoriumSverige
OrtStockholm
Period2018/07/132018/07/19

Ämnesklassifikation (UKÄ)

  • Datavetenskap (datalogi)

Fingeravtryck

Utforska forskningsämnen för ”Seeking practical CDCL insights from theoretical SAT benchmarks”. Tillsammans bildar de ett unikt fingeravtryck.

Citera det här