Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Seeking practical CDCL insights from theoretical SAT benchmarks

Elffers, Jan LU ; Cru, Jesús Giráldez ; Gocht, Stephan LU ; Nordström, Jakob LU and Simon, Laurent (2018) 27th International Joint Conference on Artificial Intelligence, IJCAI 2018 In IJCAI International Joint Conference on Artificial Intelligence 2018-July. p.1300-1308
Abstract

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... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
; ; ; and
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
series title
IJCAI International Joint Conference on Artificial Intelligence
editor
Lang, Jerome
volume
2018-July
pages
9 pages
publisher
International Joint Conferences on Artificial Intelligence
conference name
27th International Joint Conference on Artificial Intelligence, IJCAI 2018
conference location
Stockholm, Sweden
conference dates
2018-07-13 - 2018-07-19
external identifiers
  • scopus:85055682692
ISSN
1045-0823
ISBN
9780999241127
DOI
10.24963/ijcai.2018/181
language
English
LU publication?
no
id
e1e4f2b2-e67a-4e8b-bf65-ebda0fc3e184
date added to LUP
2020-12-18 22:18:00
date last changed
2022-04-26 22:42:12
@inproceedings{e1e4f2b2-e67a-4e8b-bf65-ebda0fc3e184,
  abstract     = {{<p>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.</p>}},
  author       = {{Elffers, Jan and Cru, Jesús Giráldez and Gocht, Stephan and Nordström, Jakob and Simon, Laurent}},
  booktitle    = {{Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018}},
  editor       = {{Lang, Jerome}},
  isbn         = {{9780999241127}},
  issn         = {{1045-0823}},
  language     = {{eng}},
  pages        = {{1300--1308}},
  publisher    = {{International Joint Conferences on Artificial Intelligence}},
  series       = {{IJCAI International Joint Conference on Artificial Intelligence}},
  title        = {{Seeking practical CDCL insights from theoretical SAT benchmarks}},
  url          = {{http://dx.doi.org/10.24963/ijcai.2018/181}},
  doi          = {{10.24963/ijcai.2018/181}},
  volume       = {{2018-July}},
  year         = {{2018}},
}