Ist verallgemeinertes XOR-SAT effizient lösbar?

12

Ich habe gesehen, wie XOR-3-SAT effizient lösbar ist (siehe zum Beispiel den Abschnitt "XOR-Erfüllbarkeit" im Wikipedia-Eintrag für das Boolesche Erfüllbarkeitsproblem ).

Ich frage mich eine grundlegende Frage: Ist XOR-k-SAT für Formeln mit unterschiedlich vielen Literalen pro Klausel effizient lösbar?

Ich möchte wirklich wissen, ob wir die Anzahl der Literale pro Klausel über 3 hinaus erhöhen können und ob wir gemischte Klausellängen haben können.

complexity-theory satisfiability Matt Groff
quelle
2
Welche Recherchen haben Sie durchgeführt? Wir erwarten von Ihnen, dass Sie sich zuerst selbst ernsthaft anstrengen, bevor Sie fragen, und uns in der Frage zeigen, welche Forschung Sie durchgeführt und was Sie versucht haben. Wikipedia erwähnt, dass der Algorithmus zur Lösung von XOR-3-SAT die Gaußsche Eliminierung ist. Haben Sie versucht zu verstehen, wie das funktioniert und ob es für XOR-k-SAT gilt?
DW
@DW Ich gebe zu, dass ich nicht viel darüber recherchiert habe. Ich sah die Erwähnung der Gaußschen Eliminierung und stellte fest, dass dies für verallgemeinertes XOR-SAT funktionieren würde. Aber ich schätze, ich habe nach Bestätigung gesucht. Ich hoffe, Sie werden meine Faulheit vergeben. Ich werde versuchen, in Zukunft mehr zu forschen, bevor ich solche Fragen stelle.
Matt Groff

Antworten:

11

Der Wikipedia-Artikel, mit dem Sie verlinkt haben, besagt, dass XORSAT (nicht nur 3-XORSAT) in P enthalten ist. Die Methode, mit der diese 3-XORSAT-Formel in ihrem Beispiel gelöst wird, lässt sich sehr leicht auf Formeln verallgemeinern, in denen die Klauseln beliebig sein können große Anzahl von Variablen und unterschiedliche Anzahl von Variablen.

Sie betrachten die Formel einfach als ein System linearer Gleichungen, bei dem Sie für jeden Satz eine Gleichung und für jede Variable eine Variable haben. Zum Beispiel die Formel:

(x1⊕x2⊕¬x3⊕x5)∧(x2⊕x3)

hat genau dann eine befriedigende Aufgabe, wenn das folgende Gleichungssystem eine Lösung hat:

x1+x2+(1+x3)+x5≡1mod2
x2+x3≡1mod2

Und wir können Lösungen für lineare Gleichungssysteme wie diese in polynomialer Zeit unter Verwendung der Gaußschen Elimination finden!

Dylan McKay
quelle
6

Ja. Es ist lösbar durch Gaußsche Eliminierung. Die Gaußsche Eliminierung kann jedes Gleichungssystem lösen, das linear modulo ist. XOR fungiert als Additionsmodulo 2, sodass jede XOR-SAT-Klausel als lineares Gleichungsmodulo 2 fungiert. Folglich kann die Gaußsche Eliminierung jede XOR-k-SAT-Formel oder jede XOR-SAT-Formel lösen, selbst wenn es eine unterschiedliche Anzahl von Literalen gibt pro Satz oder gemischte Satzlängen in Polynomzeit.

DW
quelle