(CDCL) [@DBLP:journals/tc/Marques-SilvaS99] backtracking search algorithm is a de facto standard for the satisfiability problem (SAT) [@DBLP:conf/ijcai/AudemardS09; @DBLP:conf/sat/BiereF15]. During the recent years, CDCL has been extended in order to fit specific requirements of formalisms in the neighborhood of SAT, e.g. Satisfiability Modulo Theories and Answer Set Programming. In the following, we first introduce some basic concepts of the satisfiability problem and then we describe the CDCL algorithm.

#### SAT.

Let $\A$ be a fixed, countable set of propositional atoms including $\bot$. A literal $\ell$ is either an atom $a$ or its negation $\neg a$, and $atom(\ell)=a$ denotes the atom associated to $\ell$. The complement of $\ell$ is denoted by $\overline{\ell}$, where $\overline{a} = \neg a$ and $\overline{\neg a} = a$ for an atom $a$. For a set $L$ of literals, $\overline{L} := \{\overline{\ell} \mid \ell \in L\}$, $L^+ :=L \cap \A$, and $L^- := \overline{L} \cap \A$. A (partial) interpretation is a set of literals $I$ containing $\lnot \bot$. $I$ is inconsistent if $I^+ \cap I^- \neq \emptyset$, otherwise $I$ is consistent. $I$ is total if $I^+ \cup I^- = \A$. Given an interpretation $I$, a literal $\ell$ is true if $\ell \in I$; is false if $\overline{\ell} \in I$, and 