Driving CDCL Search
Carmine Dodaro, Philip Gasteiger, Nicola Leone, Benjamin Musitsch,, Francesco Ricca, and Konstantin Schekotihin

TL;DR
This paper presents a general framework for designing heuristics in CDCL solvers, demonstrating significant performance improvements on industrial ASP problems by effectively integrating domain-specific criteria.
Contribution
The authors introduce a novel framework for embedding heuristics into CDCL solvers and validate it with an ASP implementation that outperforms existing solvers on industrial problems.
Findings
Our implementation finds all solutions on hard industrial instances.
State-of-the-art solvers fail to solve these instances efficiently.
The framework effectively integrates domain-specific heuristics into CDCL.
Abstract
The CDCL algorithm is the leading solution adopted by state-of-the-art solvers for SAT, SMT, ASP, and others. Experiments show that the performance of CDCL solvers can be significantly boosted by embedding domain-specific heuristics, especially on large real-world problems. However, a proper integration of such criteria in off-the-shelf CDCL implementations is not obvious. In this paper, we distill the key ingredients that drive the search of CDCL solvers, and propose a general framework for designing and implementing new heuristics. We implemented our strategy in an ASP solver, and we experimented on two industrial domains. On hard problem instances, state-of-the-art implementations fail to find any solution in acceptable time, whereas our implementation is very successful and finds all solutions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Formal Methods in Verification · Constraint Satisfaction and Optimization
