Umwandeln zu CNF

[ipsec]

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 $n^4$ dieser Formeln ($n$ 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 $n^4$ Formeln $n^4\log^8 n$ 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 $n^4 + 8n^4$ Klauseln, was akzeptabel sein sollte. Leider handelt man sich aber auch $8n^4$ neue Variablen ein, was etwas ärgerlich ist, da meine Variablenanzahl bisher nur $n^2 \log n$ 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?