

![0_image_0.png](0_image_0.png)

Figure 1: All MUS of the formula Σ (example 1)
Example 1 Let Σ = {d¯∨ e, b ∨ c¯, d¯, a¯ ∨ b, a, a ∨ c¯∨ e, a¯ ∨ c ∨ d, b¯} *be a CNF formula. Figure 1* represents all MUS of Σ.

Due to unsatisfiability of MUS, one has the following property:
Proposition 1 Let Σ be an unsatisfiable CNF formula, Γ *a MUS of* Σ.

∀I an interpretation over VΣ, ∃c ∈ Γ *such that* I 6|= c Let us consider a CNF formula Σ and a complete interpretation Ic. We say that the literal ℓ satisfies
(resp. falsifies) a clause β ∈ Σ if ℓ ∈ Ic ∩β (resp. ℓ ∈ Ic ∩ ¯β). We note L +
Ic
(β) (resp. L −
Ic
(β)), the set of literals satisfying (resp. falsifying) a clause β. The following definitions were introduced in [13].

Definition 2 (once-satisfied clause) A clause β *is said* once-satisfied by an interpretation Ic on literal z if L +
Ic
(β) = {z}.

Definition 3 (critical and linked clauses) Let Ic be a complete interpretation. A clause α *is critical* wrt Ic if |L +
Ic
(α)| = 0 and ∀ℓ ∈ α, ∃α
′ ∈ Σ *with* ¯ℓ ∈ α
′ and |L +
Ic
(α
′)| = 1*. Clauses* α
′ *are linked to* α for the interpretation Ic.

Example 2 Let Σ = (a¯∨b¯ ∨c¯)∧(a∨b¯)∧(b∨c¯)∧(c∨a¯) be a formula and Ic = {a,b,c} *an interpretation. The clause* α1 = (a¯∨b¯ ∨c¯) is critical. The other clauses of Σ are linked to α1 for Ic.

The following properties was proposed and exploited in order to compute MUS by [13].

Proposition 2 *In a minimum (local or global), the set of falsified clauses are critical.*
Proposition 3 *In a minimum (local or global), at least one of clause of each MUS is critical.*

## 3 Related Works

As it was suggested in the introduction, a lot of different approaches have been proposed to combine local search and DPLL based ones. One can divide such hybridizations in three different categories depending on the kind of the main solver. First, the main solver can be the SLS one. In that case, DP is used in order to help SLS [26, 5, 1, 17]. All of these approaches use the local search component as an assistance for the heuristic choice for variable assignment. Some of them try to focus the search on the unsatisfiable part of the formula [26], others on the satisfiable one [2, 1]. Furthermore, this step can be achieved before the search [5] or dynamically at each decision nodes [26].

d¯∨e