Umwandlung zwischen k-SAT und XOR-SAT

Laut dem XOR Satisfiability Solver-Modul für die DPLL-Integration von Tero Laitinen benötigen wir CNF-Klauseln, um eine Literal-XOR-SAT-Klausel zu konvertieren , wenn wir die Anzahl der Literale nicht erhöhen möchten. Ich verstehe also, dass der Rechenaufwand für die Umwandlung eines XOR-SAT-Ausdrucks in einen streng CNF -SAT exponentiell ist.$2^{n-1}$$n$$k$

Meine Frage: Was sind die Rechenkosten, wenn ich den Prozess umkehren möchte? Was sind die Berechnungskosten für die Umwandlung eines CNF -SAT-Ausdrucks in einen XOR-SAT-Ausdruck? Ich gehe davon aus, dass in diesem Fall nur die SAT-Ausdrücke mit äquivalenten XOR-SAT-Ausdrücken berücksichtigt werden.$k$$k$

Wenn alle XOR-Beziehungen zwischen Variablen in CNF-Formeln in Polynomzeit erfasst werden könnten, würde dies die Lösung von UNAMBIGUOUS-SAT in Polynomzeit ermöglichen. Nach dem Valiant-Vazirani-Theorem würde dieses Ergebnis implizieren, dass NP = RP ist.

Um UNAMBIGUOUS-SAT zu lösen, denken Sie daran, dass impliziert . Suchen Sie die XOR-Beziehung zwischen jedem Variablenpaar und teilen Sie die Variablen anhand der Ergebnisse in zwei Gruppen äquivalenter Variablen auf. Sobald dies erledigt ist, sind nur zwei Testzuweisungen erforderlich, um die Erfüllbarkeit zu bestimmen.$a \oplus b$$a \neq b$

In dem begrenzten Fall der Wiederherstellung von XOR-Beziehungen, die auf die übliche Weise codiert sind, d. H.

$a \oplus b \oplus c$

zu

$\lnot a \lor b \lor c \\ a \lor \lnot b \lor c \\ a \lor b \lor \lnot c \\ \lnot a \lor \lnot b \lor \lnot c$

Dies kann in Polynomzeit erfolgen, indem die Klauseln sortiert werden, gefolgt von einem linearen Zeitscan.