CNF-Kompression (Implementierung)

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

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

(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)