is undefined otherwise. A clause $\varphi$ is a set of literals, and a formula $\Gamma$ is a set of clauses. An interpretation $I$ satisfies a clause $\varphi$ if $\varphi \cap I \neq \emptyset$. A consistent, total interpretation $I$ is a model of a formula $\Gamma$ if all clauses in $\Gamma$ are satisfied. A formula $\Gamma$ is said to be consistent if it admits some model, inconsistent otherwise. Given a formula $\Gamma$, the SAT problem consists in determining whether $\Gamma$ is consistent.

\[ex:ex1\] Consider the formula $\Gamma=\{\{a, b,\neg c\}, \{a\},$ $ \{\neg b\}, \{c, d\}, \{c, \neg d\}\}$. $I=\{a,\neg b, c, d\}$ is a model of $\Gamma$.

#### CDCL algorithm.

The CDCL algorithm takes as input a formula $\Gamma$, and determines whether it is consistent. The first step of the algorithm consists of the simplification of $\Gamma$. Polynomial algorithms for clause rewriting and variable elimination are applied on $\Gamma$, which strengthen and/or remove redundant clauses [@DBLP:conf/sat/EenB05]. After the simplifications step, the partial interpretation $I$ is set to $\{\lnot \bot\}$, and the backtracking search starts. First, $I$ is extended with all the literals that can be deterministically inferred by applying some inference rule (*propagation* step). The main inference rule of a SAT 