$I:=\{\lnot \bot\}$. Unit propagation extends $I$ with $a$ and $\neg b$ to satisfy clauses $\{a\}$ and $\{\neg b\}$. No other inferences can be done, thus a choice is performed among $c$, $\neg c$, $d$, and $\neg d$. Choosing $\neg c$ would lead to an inconsistency, while all other choices would directly lead to a model.

#### Heuristics.

It is well-known that the selection the branching literal plays a crucial role for efficiency. Nowadays, state-of-the-art solvers, such as [<span style="font-variant:small-caps;">lingeling</span>]{} [@DBLP:conf/sat/BiereF15] and [<span style="font-variant:small-caps;">glucose</span>]{} [@DBLP:conf/ijcai/AudemardS09], implement branching criteria belonging to the VSIDS [@DBLP:conf/dac/MoskewiczMZZM01] family that are a variant of the [<span style="font-variant:small-caps;">minisat</span>]{} [@DBLP:conf/sat/EenS03] heuristic. Thus, in the following, the [<span style="font-variant:small-caps;">minisat</span>]{} [@DBLP:conf/sat/EenS03] heuristic is referred to as the *default branching heuristic* of a CDCL solver. The [<span style="font-variant:small-caps;">minisat</span>]{}heuristic is based on the *activity* value for each atom in the input formula $\Gamma$, which is initially set to 0. The activity of $atom(\ell)$ is incremented by a value $inc$ when a literal $\ell$ occurs in a learned clause. Then, after learning the clause, the value of $inc$ is multiplied by a constant slightly greater than 1, to give more and more importance to variables that occur in recently-learned clauses. Once a choice 