CNF-Kompression (Implementierung)

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

das sind minimale Klauseln P_i mathend000# mit F→P_i mathend000#

(minimal bezüglich Inklusion von Literalen)

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

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