CNF-Kompression (Implementierung)

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

das sind minimale Klauseln Pi mathend000# mit FPi mathend000#

(minimal bezüglich Inklusion von Literalen)


dann bestimme eine kleinste Teilmenge MP mathend000# mit $ \bigwedge$MF 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



2014-03-31