Algorithm 1: CDCL solver Input: a CNF formula Σ
Output: SAT or UNSAT
1 I = /0 ; /* interpretation */
2 dl = 0 ; /* decision level */
3 xc = 0 ; /* number of conflicts */
4 **while** *(true)* do 5 γ = BCP(Σ,I);
6 if (γ*!=null)* then 7 xc = xc +1; 8 β =conflictAnalysis(Σ,I,c); 9 bl = computeBackjumpingLevel(γ,I);
10 if (bl < 0) **then return** UNSAT;
11 Σ = Σ∪ {γ};
12 if *(restart())* **then** bl = 0; 13 backjump(Σ,I,bl);
14 dl = bl; 15 else 16 if *(all variables are instanciated)* then 17 **return** SAT;
18 ℓ = chooseDecisionLiteral(Σ);
19 dl = dl +1; 20 I = I ∪ {ℓ};
21 22 end are assigned, then I is a model of Σ (lines 16–17). Each time a conflict is reached by unit propagation
(then γ is the conflict clause) A nogood β is computed (line 8) using a given scheme, usually the first-UIP
(Unique Implication Point) one [31] and a backjump level is computed. At this point, It may have proved the unsatisfiability of the formula Σ. If it is not the case, the nogood β is added to the clause database and backjump is done (lines 11–14). Finally, sometimes CDCL solvers enforce restarts (different strategies are possible [20]). In this case, one backjump in the top of the search tree.

## 2.4 Muses

Minimum unsatisfiable sub-formulas (MUS) of a CNF formula represent the smallest explanations for the inconsistency in term of the number of clauses. MUS are very important in order to circumscribe and highlight the source of contradiction of a given formula. Formally, one has:
Definition 1 Let Σ be a CNF formula. A MUS Γ of Σ is a set of clauses such that:
1. Γ ⊆ Σ;
2. Γ is unsatisfiable; 3. ∀∆ ⊂ Γ,∆ is satisfiable.