{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:25:21Z","timestamp":1767338721933},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,7]]},"abstract":"<jats:p>Over the last decades Boolean satisfiability (SAT) solvers based on\n\nconflict-driven clause learning (CDCL) have developed to the point\n\nwhere they can handle formulas with millions of variables.  Yet a\n\ndeeper understanding of how these solvers can be so successful has\n\nremained elusive.  In this work we shed light on CDCL performance by\n\nusing theoretical benchmarks, which have the attractive features of\n\nbeing a) scalable, b) extremal with respect to different proof search\n\nparameters, and c) theoretically easy in the sense of having short\n\nproofs in the resolution proof system underlying CDCL. This allows for\n\na systematic study of solver heuristics and how efficiently they\n\nsearch for proofs.  We report results from extensive experiments on a\n\nwide range of benchmarks. Our findings include several examples where\n\ntheory predicts and explains CDCL behaviour, but also raise a number\n\nof intriguing questions for further study.<\/jats:p>","DOI":"10.24963\/ijcai.2018\/181","type":"proceedings-article","created":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T01:49:10Z","timestamp":1530755350000},"page":"1300-1308","source":"Crossref","is-referenced-by-count":10,"title":["Seeking Practical CDCL Insights from Theoretical SAT Benchmarks"],"prefix":"10.24963","author":[{"given":"Jan","family":"Elffers","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology"}]},{"given":"Jes\u00fas","family":"Gir\u00e1ldez-Cru","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology"}]},{"given":"Stephan","family":"Gocht","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology"}]},{"given":"Laurent","family":"Simon","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Bordeaux"}]}],"member":"10584","event":{"number":"27","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)"],"acronym":"IJCAI-2018","name":"Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}","start":{"date-parts":[[2018,7,13]]},"theme":"Artificial Intelligence","location":"Stockholm, Sweden","end":{"date-parts":[[2018,7,19]]}},"container-title":["Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T01:50:34Z","timestamp":1530755434000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2018\/181"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2018\/181","relation":{},"subject":[],"published":{"date-parts":[[2018,7]]}}}