Darstellung von Modellmengen

Ordnung auf Variablen festlegen: x₁ < x₂ < … < x_n mathend000#

und dann binärer Entscheidungsbaum:

• Blätter: 0, 1

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

• innere Knoten t mathend000#
  • Variable v mathend000#
  • Kinder (Bäume) l, r mathend000#

    alle Variablen in l mathend000# und r mathend000# sind größer als v mathend000#

  repräsentiert Modellmenge [t] = {{(v, 0)}∪b | b∈[l]}∪{{(v, 1)}∪b | b∈[r]} mathend000#

Für jede Formel F mathend000# existiert Baum B mathend000# mit [B] = Mod(F) mathend000#.