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 mathend000# selbst?
• Modellmenge Mod(F) mathend000# als Menge von Belegungen?

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

Literatur: Kroening, Strichman: Decision Procedures, 2.4.