Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Seeking practical CDCL insights from theoretical SAT benchmarks
KTH.
KTH.
KTH.
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-2700-4285
Show others and affiliations
2018 (English)In: IJCAI International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence , 2018, p. 1300-1308Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
International Joint Conferences on Artificial Intelligence , 2018. p. 1300-1308
Keywords [en]
Artificial intelligence, Formal logic, Boolean satisfiability, Clause learning, Extremal, Intriguing questions, Proof search, Resolution proofs, Systematic study, Benchmarking
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-246573Scopus ID: 2-s2.0-85055682692OAI: oai:DiVA.org:kth-246573DiVA, id: diva2:1319749
Conference
27th International Joint Conference on Artificial Intelligence, IJCAI 2018, 13 July 2018 through 19 July 2018
Note

QC 20190603

Available from: 2019-06-03 Created: 2019-06-03 Last updated: 2019-06-03Bibliographically approved

Open Access in DiVA

No full text in DiVA

Scopus

Authority records BETA

Elffers, Jan

Search in DiVA

By author/editor
Elffers, JanCru, Jesús GiráldezGocht, StephanNordström, Jakob
By organisation
KTHTheoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 83 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf