Motivation

gesucht ist eine Datenstruktur, die eine aussagenlogische Formel kanonisch repräsentiert und für die aussagenlog. Operationen effizient ausführbar sind.

Ansätze:

• Formel F selbst?
• Modellmenge Mod(F) als Menge von Belegungen?

Lösung: bessere Darstellung für Mod(F)

Literatur: Kroening, Struchman: Decision Procedures, 2.4.