CNF-Kompression (Implementierung)

zu gegebener Formel F bestimme Menge der Prim-Implikanten P = {P1,...},

das sind minimale Klauseln Pi mit F $ \rightarrow$ Pi

(minimal bezüglich Inklusion von Literalen)


dann bestimme eine kleinste Teilmenge M $ \subseteq$ P mit $ \bigwedge$M $ \rightarrow$ F.

das ist eine ganzzahlige lineare Optimierungsaufgabe, kann durch entsprechende Constraint-Solver gelöst werden (glpsol, scip)



2009-06-22