Darstellung von Modellmengen

Ordnung auf Variablen festlegen: x_n > … > x₂ > x₁

und dann binärer Entscheidungsbaum:

• Blätter: beschriftet mit 0, 1

  repräsentiert leere (bzw. volle) Modellmenge ∅ bzw. {∅}

• innere Knoten t auf Höhe k
  • Schlüssel: Variable x_k, Kinder: Bäume l, r
  repräsentiert Teilmenge von {x₁,…, x_k}→$\mathbb {B}$

  [t] = {{(x_k, 0)}∪b | b∈[l]}∪{{(x_k, 1)}∪b | b∈[r]}

Für jede Formel F exist. genau ein solcher Baum B mit [B] = Mod(F).

Jeder Pfad von Wurzel zu 1 repräsentiert ein b∈{x₁,…, x_k}→$\mathbb {B}$ (ein Modell).