is needed, the literal $\lnot at$ is chosen, where $at$ is the undefined atom having the highest activity value (ties are broken randomly).

For the sake of completeness, we mention that the CDCL is usually complemented with heuristics that control the number of learned clauses, and restart the computation to explore different branches of the search tree [@DBLP:series/faia/2009-185].

Driving CDCL Search {#sec:heur}
===================

[|p[.9]{}|]{}\
\
\
*Triggered when the backtracking search starts. $\Gamma'$ and $\A'$ are the formula and the atoms after the simplifications, resp.*\
\
\
*Triggered when the choice $\ell$ led to an inconsistency.*\
\
\
*Triggered when a conflict is detected after the choice of $\ell$.*\
\
\
*Triggered when the clause $\varphi$ is learned.*\
\
\
*Triggered when the literal $\ell$ is involved in the creation of a clause to learn, e.g., while applying the first UIP schema.*\
\
\
*Triggered when the clause $\varphi$ has been removed.*\
\
\
*Triggered when a restart of the search occurs.*\
\
\
*Triggered during backtracking if the literal $\ell$ is set to undefined.*\

In this section we present the results of our studies pinpointing the key ingredients needed to drive the search of CDCL solvers. These were distilled 