I
Für einen SAT-Solver muss ich eine größere Formel zu CNF umwandeln. Das geht auch ganz gut, Sorgen machen mir jedoch eine Reihe von Noch-Nicht-Klauseln der folgenden Form:
x \implies (x_{1,1} \land … \land x_{1,\log n}) \lor … \lor (x_{8,1} \land … \land x_{8,\log n})
Insgesamt habe ich n4n^4n4 dieser Formeln (nnn ist hier meine Problemgröße).
Beim Umwandeln in CNF mit der naiven Methode (Implikation zu \lnot x \lor … umwandeln, dann Distributivgesetz) werden damit insgesamt aus den n4n^4n4 Formeln n4log8nn^4\log^8 nn4log8n Klauseln, was leider zu viel ist.
Beim Suchen nach einer besseren Möglichkeit bin ich schon auf die Tseitin-Transformation gestoßen. Wenn man diese auf diesen speziellen Fall anwendet, müsste man für jede Unterklausel eine neue Variable einführen und käme insgesamt auf n4+8n4n^4 + 8n^4n4+8n4 Klauseln, was akzeptabel sein sollte. Leider handelt man sich aber auch 8n48n^48n4 neue Variablen ein, was etwas ärgerlich ist, da meine Variablenanzahl bisher nur n2lognn^2 \log nn2logn beträgt.
(Er)Kennt deshalb jemand eine besser geeignete Transformation, diesen speziellen Formeltyp erfüllbarkeitserhaltend und mit möglichst wenig neuen Variablen und Klauseln in CNF umzuwandeln?
