Driving CDCL Search

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.