CNF-Kompression (Implementierung)

zu gegebener Formel F bestimme Menge der Prim-Implikanten P = {P₁,…},

das sind minimale Klauseln P_i mit F→P_i

(minimal bezüglich Inklusion von Literalen)

dann bestimme eine kleinste Teilmenge M⊆P mit $\bigwedge$M→F.

das ist eine ganzzahlige lineare Optimierungsaufgabe (Übung: welche?), kann durch entsprechende Constraint-Solver gelöst werden (glpsol, scip, clp)

Diskussion: http://groups.google.com/group/minisat/msg/012bb4712c7e90a7

Anwendung: https://github.com/jwaldmann/satchmo/blob/master/Satchmo/Binary/Op/Common.hs#L118