Eigenschaften, die in 2-CNF oder 2-SAT ausgedrückt werden können

12

Wie zeigt man, dass eine bestimmte Eigenschaft nicht in 2-CNF (2-SAT) ausgedrückt werden kann? Gibt es irgendwelche Spiele, wie zum Beispiel Kieselspiele? Das klassische Schwarzkieselspiel und das Schwarz-Weißkieselspiel scheinen dafür ungeeignet zu sein (laut Hertel und Pitassi, SIAM J of Computing, 2010, sind sie PSPACE-vollständig).

Oder andere Techniken als Spiele?

Bearbeiten : Ich dachte an Eigenschaften, die das Zählen (oder die Kardinalität) eines unbekannten Prädikats beinhalten ( SO- Prädikat, wie Theoretiker endlicher Modelle sagen würden). Zum Beispiel wie in Clique oder ungewichtetes Matching. (a) Clique : Gibt es eine Clique in der gegebenen Grafik so dass eine bestimmte Anzahl ? (b) Matching : Gibt es ein passendes in so dass ?CG|C|K MG|M|K

Kann 2-SAT zählen? Hat es einen Zählmechanismus? Scheint zweifelhaft.

Sameer Gupta
quelle
Ich verstehe, dass es Ehrenfeucht-Fraïssé-Spiel (für FO) und Ajtai-Fagin-Spiel (für monadische SO) in der Finite-Model-Theorie gibt. Aber nicht sicher, ob sie hier ausreichen. Auch die Spiele in FMT werden mit geordneten Strukturen kompliziert, oder?
Sameer Gupta
@Marzio es scheint ein Beweis zu sein, dass nicht alle Booleschen Funktionen in 2CNF ausgedrückt werden können, wie Sie die Frage beantworten würden (da Sie sich nicht sicher sind, sehen Sie es nicht als offensichtlich an). Was ist das für ein Beweis? Wird es irgendwo veröffentlicht?
VZN
5
@vzn: eine triviale Booleschen Funktion , die nicht in exprimierbarer 2-CNF ist: (x1x2x3)
Marzio De Biasi
2
@SameerGupta: Nach der Neuformulierung wird die Frage vielleicht schwierig :-); in der Tat , wo φ Klauseln mit zwei Variablen ist begrenzt (SO-Krom) erfasst über NL geordnete Strukturen, während die Existenz SO Captures NP. Offensichtlich auf FO 2-SAT beschränkt, kann nicht gezählt werden (und die Ehrenfeucht-Fraïssé-Spiel- oder Kompaktheitstechniken sind weit genug, weil Sie damit beweisen können, dass PARITÄT nicht für FO definierbar ist).P1...Pnz¯φ(P1,...,Pn,z¯)φ
Marzio De Biasi
1
in Ordnung. Es scheint eine allgemeine Theorie zu geben, dass SAT nicht alle booleschen Funktionen für die Konstante k ausdrücken kann . Was ist das für eine Theorie? Diese Frage fragt nach dem Sonderfall k = 2 . Es ist zu beachten, dass es ein Konzept zum "Reduzieren" von n -SAT zu 3-SAT über die Tseitin-Transformation gibt . habe auch gesehen, dass ein ähnliches Konzept in monotonen Schaltkreisuntergrenzen Beweisen (Razborov) auftaucht. kkk=2n
VZN

Antworten:

19

Eine Familie von Bitvektoren ist die Klasse von Lösungen für ein 2-SAT-Problem, wenn und nur wenn sie die Median-Eigenschaft hat: Wenn Sie die bitweise Mehrheitsfunktion auf drei beliebige Lösungen anwenden, erhalten Sie eine andere Lösung. Siehe zB https://en.wikipedia.org/wiki/Median_graph#2-satisfiability und seine Referenzen. Wenn Sie also drei Lösungen finden, für die dies nicht zutrifft, wissen Sie, dass es nicht in 2-CNF ausgedrückt werden kann.

David Eppstein
quelle
David, danke, wird das nachschlagen. @vzn - Bezieht sich Davids Antwort auf das, was Sie vor zwei Tagen auf der Chat-Site kommentiert haben, darauf, dass 3SAT-Formeln für alle Bitvektorsätze existieren und nach einem Ergebnis für 2SAT-Formeln für Bitvektorsätze gesucht wird?
Sameer Gupta
David, Yuval - Sicher funktionieren Ihre Beweise, wenn Sie denselben Variablensatz verwenden. Was aber, wenn der verwendete Variablensatz völlig anders sein kann? Schauen Sie sich die Antwort von Martin Seymour hier an: cstheory.stackexchange.com/questions/200/… - Um zu zeigen, dass es keine gleichwertige Reduktion (vorzugsweise logspace) von K-Clique oder K-Matching auf 2SAT gibt, wäre ein anderer Beweis erforderlich . Gedanken?
Sameer Gupta
1
Das Hinzufügen und anschließende Projizieren von Hilfsvariablen hilft nicht weiter, denn wenn die Median-Eigenschaft für das erweiterte Variablensystem zutrifft, ist sie in der Projektion immer noch wahr.
David Eppstein
4
Eine andere Art zu sagen ist, dass der Median (oder die Mehrheit) ein Polymorphismus für 2SAT-Einschränkungen ist. Tatsächlich ist bekannt, dass jede CSP (auch nicht-boolesche), die die Mehrheit als Polymorphismus hat, in (Dalmau-Krokhin '08) steht. NLP
Arnab
10

Sei eine Eigenschaft von n Variablen. Nehmen wir an, dass es eine 2CNF Formel φ ( x 1 , ... , x n , y 1 , ... , y m ) derart , dass P ( x 1 , ... , x n ) y 1y m φ ( x 1P(x1,,xn)nφ(x1,,xn,y1,,ym) Wir behaupten, dass φ einer 2CNF-Formel ψ mit nur x 1 , , x n entspricht . Um dies zu beweisen, genügt es zu zeigen, wie man y m eliminiert. Schreib φ = & khgr; s k = 1 ( y mU k ) t l =

P(x1,,xn)y1ymφ(x1,,xn,y1,,ym).
φψx1,,xnym wobeiUk,VLiterale sind undχymnicht mit einbezieht. Die Formelφist äquivalent zu χ( ¯ y m s k = 1 Uk)(ym t = 1 V)
φ=χk=1s(ymUk)=1t(ym¯V),
Uk,Vχymφ Dies beweist die Ansprüchewenn y m in einer Einheit Klausel nicht erscheint; Wenn dies der Fall ist, können wir es direkt beseitigen.
χ(ym¯k=1sUk)(ym=1tV)χ(k=1sUk=1tV)χk=1s=1t(UkV)
ym

Wir schließen daraus, dass als 2CNF-Formel ausgedrückt werden kann, wenn es eine 2CNF-Formel ψ ( x 1 , , x n ) gibt , die P entspricht . Daher kann eine Eigenschaft P als 2CNF ausgedrückt werden, wenn jede fälschende Zuweisung von höchstens zwei Literalen erzwungen wird. Insbesondere können K- Klasse und K- Übereinstimmung nicht als 2CNF ausgedrückt werden (mit Ausnahme des Eckfalles n- Klasse).P(x1,,xn)ψ(x1,,xn)PPKKn

Yuval Filmus
quelle
yichψx1x2xnϕ1ϕ2ϕ2
1
yichyich
5

L -L

(Ja, ich kenne diese Additions-, Multiplikations- und Zählberechnungsfunktionen, aber es ist einfach, sie in Entscheidungsversionen ihrer jeweiligen Probleme umzuwandeln.)

LNLNLEINC0EINC0

(c) , so zum Zählen , obwohl sie nicht in der Lage sein können , eine äquivalente Expression in 2-CNF, unter Verwendung des Verfahrens in (b) umrissenen zu erhalten, kann man eine erhalten equisatisfiable 2-CNF - Expression.

Also ja, 2-SAT kann zählen.

NL|M|NL

Martin Seymour
quelle
1
Zu (c): Wenn Sie meiner Antwort glauben, kann eine gleichwertige 2-CNF-Expression in eine echte äquivalente 2-CNF-Expression umgewandelt werden.
Yuval Filmus
-  
Sie können meine Antwort lesen und selbst sehen. Beachten Sie, dass es in diesem Fall keine Zeit- / Raumgrenzen gibt.
Yuval Filmus
1
LEINC0fxLf(x)
Emil, genau! In die andere Richtung, wenn Yuval mit einem beginntϕxichϕ-xich