Driving CDCL Search
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.
Keywords
Cite
@article{arxiv.1611.05190,
title = {Driving CDCL Search},
author = {Carmine Dodaro and Philip Gasteiger and Nicola Leone and Benjamin Musitsch and Francesco Ricca and Konstantin Schekotihin},
journal= {arXiv preprint arXiv:1611.05190},
year = {2016}
}
Comments
Paper presented at the 1st Workshop on Trends and Applications of Answer Set Programming (TAASP 2016), Klagenfurt, Austria, 26 September 2016, 15 pages, LaTeX, 5 figures