solver is *unit propagation* that extends $I$ by an undefined literal $\ell$ whenever there is a clause $\varphi\in\Gamma$ such that $\ell \in \varphi$ and $\varphi \setminus \ell \subseteq \overline{I}$. Three cases are possible after a propagation step is completed: $(i)$ $I$ is consistent but not total. In that case, an undefined literal $\ell$ (called *branching literal*) is chosen according to some heuristic criterion, and is added to $I$. Then, a propagation step is performed that infers the consequences of this choice. $(ii)$ $I$ is inconsistent, thus there is a conflict, and $I$ is analyzed. The reason of the conflict is modeled by a fresh clause $\varphi$ that is added to $\Gamma$ (clause *learning*), e.g. by applying the *first Unique Implication Point (UIP)* technique [@DBLP:conf/iccad/ZhangMMM01]. Moreover, the algorithm backtracks (i.e. choices and their consequences are undone) until the consistency of $I$ is restored. Then the algorithm propagates inferences starting from the fresh clause $\varphi$. Otherwise, if the consistency of $I$ cannot be restored, the algorithm terminates returning [<span style="font-variant:small-caps;">inconsistent</span>]{}. Finally, in case $(iii)$ $I$ is consistent and total, i.e. $I$ is a model, the algorithm terminates returning [<span style="font-variant:small-caps;">consistent</span>]{}.

\[ex:ex2\] Consider the formula $\Gamma$ of Example \[ex:ex1\]. The search starts with 