3-SAT, wobei Variablen als positives und als negatives Literal gleich oft vorkommen

Sei eine 3-CNF-Formel über die Variablen . Jede Variable , , kommt in gleich oft als positives Literal und als negatives Literal vor .$\phi$$x_1,x_2,\ldots,x_n$$x_i$$i \in [n]$$\phi$

Ist es NP-vollständig, über die Erfüllbarkeit einer solchen Formel zu entscheiden? Vorausgesetzt, es ist, würde mich interessieren, ob es einen speziellen Namen hat. Wurde es vielleicht auch irgendwo untersucht?

Das Problem wurde von Ryo Yoshinaka als P N-SAT-Problem in Matching höherer Ordnung im linearen Lambda-Kalkül untersucht (in der 16. Internationalen Konferenz, RTA 2005, Nara, Japan, 19.-21. April 2005, Proceedings) .$m$$n$

Das P N-SAT ist ein SAT-Problem, bei dem jedes positive Literal genau mal und jedes negative Literal genau mal auftritt . Es wurde gezeigt, dass sogar P N-SAT NP-vollständig ist. Beachten Sie, dass P N-SAT in P ist, da jede Variable nach einem einzelnen Auflösungsschritt leicht entfernt werden kann, wodurch die Anzahl der Klauseln in der Formel nicht erhöht wird.$m$$n$$m$$n$$2$$1$$1$$1$

Es ist NP-vollständig (aber ich weiß nicht, ob es einen Namen hat): Angenommen, eine Variable erscheint öfter als positives Literal als als negatives Literal.$x_i$$n$

Dann können Sie es "ausgleichen", indem Sie neue 3CNF-Klauseln mit neuen Variablen hinzufügen :$n$$n$$y_1,...,y_n$

$-x_i \lor y_1 \lor -y_2$
$-x_i \lor y_2 \lor -y_3$
...
$-x_i \lor y_{n-1} \lor -y_n$
$-x_i \lor y_n \lor -y_1$

Wenn mehrmals als negatives Literal angezeigt wird, wenden Sie dieselbe Erweiterung an, verwenden Sie jedoch in den neuen 3CNF-Klauseln anstelle von .$x_i$$x_i$$-x_i$

Die sind ausgeglichen und die resultierende Formel (die in Polynomzeit erstellt werden kann) ist genau dann eindeutig erfüllbar, wenn die ursprüngliche 3CNF-Formel erfüllt werden kann : Was auch immer der Wert von die neuen Klauseln können erfüllt werden, indem wird "stören" Sie nicht die Erfüllbarkeit der ursprünglichen Formel.$y_i$$x_i$$y_i = true$