---
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.'
author:
- Carmine Dodaro
- Philip Gasteiger
- Nicola Leone
- |
    \
    Benjamin Musitsch
- Francesco Ricca
- Konstantin Schekotihin
title: Driving CDCL Search
---

Introduction
============

The Conflict Driven Clause Learning (CDCL) algorithm [@DBLP:journals/tc/Marques-SilvaS99] is the leading solution adopted by state-of-the-art solvers for Boolean Satisfiability (SAT) [@DBLP:series/faia/2009-185], Satisfiability Modulo Theories (SMT) [@DBLP:journals/jacm/NieuwenhuisOT06], and Answer Set Programming (ASP) [@DBLP:journals/cacm/BrewkaET11] to mention a few. Notably, CDCL solvers have been applied with success for solving several real-world problems ranging from hardware and 