Different choice of branching variables

set of clauses:

{ ¬x₁ ∨ x₃ ∨ x₄, ¬x₂ ∨ x₆ ∨ x₄, ¬x₂ ∨ ¬x₆ ∨ ¬x₃, ¬x₄ ∨ ¬x₂, x₂ ∨ ¬x₃ ∨ ¬x₁, x₂ ∨ x₆ ∨ x₃, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, ¬x₆ ∨ x₃ ∨ ¬x₅, x₁ ∨ ¬x₃ ∨ ¬x₅ }

First branching

branch on x₃

First recursive call

recursive call with x₃=true

Propagate x₃=true

{ ¬x₁ ∨ x₃ ∨ x₄, ¬x₂ ∨ x₆ ∨ x₄, ¬x₂ ∨ ¬x₆ ∨ ¬x₃, ¬x₄ ∨ ¬x₂, x₂ ∨ ¬x₃ ∨ ¬x₁, x₂ ∨ x₆ ∨ x₃, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, ¬x₆ ∨ x₃ ∨ ¬x₅, x₁ ∨ ¬x₃ ∨ ¬x₅ }
=
{ ¬x₂ ∨ x₆ ∨ x₄, ¬x₂ ∨ ¬x₆, ¬x₄ ∨ ¬x₂, x₂ ∨ ¬x₁, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }

no contradiction, choose a branching variable

Branch on x₄

Propagate x₄=true

{ ¬x₂ ∨ x₆ ∨ x₄, ¬x₂ ∨ ¬x₆, ¬x₄ ∨ ¬x₂, x₂ ∨ ¬x₁, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }
=
{ ¬x₂ ∨ ¬x₆, ¬x₂, x₂ ∨ ¬x₁, x₂ ∨ ¬x₆, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }
=   (with ¬x₂)
{ ¬x₂ ∨ ¬x₆, ¬x₂, x₂ ∨ ¬x₁, x₂ ∨ ¬x₆, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }
=
{ ¬x₁, ¬x₆, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }
=
contradiction: ¬x₁, ¬x₆, x₁ ∨ x₆

Contradiction generated

Backtrack, propagate x₄=false

{ ¬x₂ ∨ x₆ ∨ x₄, ¬x₂ ∨ ¬x₆, ¬x₄ ∨ ¬x₂, x₂ ∨ ¬x₁, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }
=
{ ¬x₂ ∨ x₆, ¬x₂ ∨ ¬x₆, x₂ ∨ ¬x₁, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }

no contradiction, no unit clause

Choice of another branching variable

Set x₂=true

{ ¬x₂ ∨ x₆, ¬x₂ ∨ ¬x₆, x₂ ∨ ¬x₁, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }
=
{ x₆, ¬x₆, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }

contradiction

Backtrack, propagate x₂=false

{ ¬x₂ ∨ x₆, ¬x₂ ∨ ¬x₆, x₂ ∨ ¬x₁, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }
=
{ ¬x₁, x₁ ∨ x₅, x₁ ∨ x₆, x₁ ∨ ¬x₅ }

contradictin: from ¬x₁ both x₅ and ¬x₅ follow

Backtrack, propagate x₃=false

{ ¬x₁ ∨ x₃ ∨ x₄, ¬x₂ ∨ x₆ ∨ x₄, ¬x₂ ∨ ¬x₆ ∨ ¬x₃, ¬x₄ ∨ ¬x₂, x₂ ∨ ¬x₃ ∨ ¬x₁, x₂ ∨ x₆ ∨ x₃, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, ¬x₆ ∨ x₃ ∨ ¬x₅, x₁ ∨ ¬x₃ ∨ ¬x₅ }
=
{ ¬x₁ ∨ x₄, ¬x₂ ∨ x₆ ∨ x₄, ¬x₄ ∨ ¬x₂, x₂ ∨ x₆, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, ¬x₆ ∨ ¬x₅ }

no contradiction, no unit clause

Choose another branching variable

Set x₁=true, propagate

{ ¬x₁ ∨ x₄, ¬x₂ ∨ x₆ ∨ x₄, ¬x₄ ∨ ¬x₂, x₂ ∨ x₆, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, ¬x₆ ∨ ¬x₅ }
=
{ x₄, ¬x₂ ∨ x₆ ∨ x₄, ¬x₄ ∨ ¬x₂, x₂ ∨ x₆, x₂ ∨ ¬x₆ ∨ ¬x₄, ¬x₆ ∨ ¬x₅ }
=   (with x₄=true)
{ x₄, ¬x₂ ∨ x₆ ∨ x₄, ¬x₄ ∨ ¬x₂, x₂ ∨ x₆, x₂ ∨ ¬x₆ ∨ ¬x₄, ¬x₆ ∨ ¬x₅ }
=
{ ¬x₂, x₂ ∨ x₆, x₂ ∨ ¬x₆, ¬x₆ ∨ ¬x₅ }

contradiction: ¬x₂ generates both x₆ and ¬x₆

Backtrack, propagate x₁=false

{ ¬x₁ ∨ x₄, ¬x₂ ∨ x₆ ∨ x₄, ¬x₄ ∨ ¬x₂, x₂ ∨ x₆, x₂ ∨ ¬x₆ ∨ ¬x₄, x₁ ∨ x₅, x₁ ∨ x₆, ¬x₆ ∨ ¬x₅ }
=
{ ¬x₂ ∨ x₆ ∨ x₄, ¬x₄ ∨ ¬x₂, x₂ ∨ x₆, x₂ ∨ ¬x₆ ∨ ¬x₄, x₅, x₆, ¬x₆ ∨ ¬x₅ }

contradiction: x₅, x₆, ¬x₆ ∨ ¬x₅

Backtrack

set is unsatisfiable