Sökning: onr:"swepub:oai:DiVA.org:kth-246573" >
Seeking practical C...
Seeking practical CDCL insights from theoretical SAT benchmarks
-
- Elffers, Jan (författare)
- KTH,Skolan för elektroteknik och datavetenskap (EECS)
-
- Giráldez-Crú, Jesús (författare)
- KTH,Teoretisk datalogi, TCS
-
- Gocht, Stephan (författare)
- KTH,Skolan för elektroteknik och datavetenskap (EECS)
-
visa fler...
-
- Nordström, Jakob (författare)
- KTH,Teoretisk datalogi, TCS
-
- Simon, L. (författare)
- Université de Bordeaux, France
-
visa färre...
-
(creator_code:org_t)
- California : International Joint Conferences on Artificial Intelligence, 2018
- 2018
- Engelska.
-
Ingår i: IJCAI International Joint Conference on Artificial Intelligence. - California : International Joint Conferences on Artificial Intelligence. ; , s. 1300-1308
- Relaterad länk:
-
https://doi.org/10.2...
-
visa fler...
-
https://www.ijcai.or...
-
https://urn.kb.se/re...
-
https://doi.org/10.2...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Artificial intelligence
- Formal logic
- Boolean satisfiability
- Clause learning
- Extremal
- Intriguing questions
- Proof search
- Resolution proofs
- Systematic study
- Benchmarking
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)