DPLL-Begriffe

für partielle Belegung b (Bsp: {(x₁, 1),(x₃, 0)}): Klausel c ist

• erfüllt, falls ∃l∈c : b(l )= 1, Bsp: (¬x₁∨x₂∨¬x₃)
• Konflikt, falls ∀l∈c : b(l )= 0, Bsp: (¬x₁∨x₃)
• unit, falls ∃l∈c : b(l )= $\bot$∧∀l'∈(c $\setminus$ {l}) : b(l') = 0,

  Bsp: (¬x₁∨¬x₂∨x₃). Dabei ist l = ¬x₂ das Unit-Literal.

• offen, sonst. Bsp: (x₂∨x₃∨x₄).

Eigenschaften: für CNF F und partielle Belegung b:

• wenn ∃c∈F : c ist Konflikt für b, dann ¬∃b'⊇b mit b' $\models$ F

  (d.h., die Suche kann dort abgebrochen werden)

• wenn ∃c∈F: c ist Unit für b mit Literal l, dann ∀b'⊇b : b' $\models$ F⇒b'(l )= 1

  (d.h., l kann ohne Suche belegt werden)