Open Collections

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

Banff International Research Station for Mathematical Innovation and Discovery

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 try to shed light on CDCL performance by using theoretical benchmarks. While these are crafted instances, they 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 successfully they implement efficient proof search.

We report results from extensive experiments with different CDCL parameter configurations on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raises a number of intriguing questions for further study.

This is a presentation of a paper that is published at IJCAI '18.

Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science

video/mp4

Author affiliation: KTH Royal Institute of Technology

2019-03-31

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/69363

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/