Ein direkter Summensatz für die Raumkomplexität der Auflösungsklausel?

Die Auflösung ist ein Schema zum Nachweis der Unzufriedenheit von CNFs. Ein Beweis in der Auflösung ist eine logische Ableitung der leeren Klausel für die anfänglichen Klauseln in der CNF. Insbesondere kann jede Anfangsklausel abgeleitet werden, und aus zwei Klauseln $A \lor x$ und $B \lor \neg{x}$ die Klausel $A \lor B$ abgeleitet werden. Eine Widerlegung ist eine Folge von Abzügen, die mit einer leeren Klausel endet.

Wenn eine solche Widerlegung implementiert ist, können wir eine Prozedur in Betracht ziehen, die einige Klauseln im Speicher behält. Falls eine Nicht-Anfangsklausel erneut verwendet werden muss und sich nicht mehr im Speicher befindet, sollte der Algorithmus sie erneut von Grund auf neu oder von denjenigen im Speicher verwenden.

Sei $Sp(F)$ die kleinste Anzahl von Klauseln, die gespeichert werden müssen, um die leeren Klauseln zu erreichen. Dies wird als Klauselraumkomplexität von $F$ . Wir sagen, dass $Sp(F)=\infty$ ist. $F$ ist erfüllbar.

Das Problem, das ich vorschlage, ist folgendes: Betrachten Sie zwei CNFs $A=\bigwedge_{i=1}^m A_i$ und $B=\bigwedge_{j=1}^n B_j$ und lassen Sie den CNF

A \lor B = ⋀_{i = 1}^{m} ⋀_{j = 1}^{n} A_{i} \lor B_{j}

$A \lor B = \bigwedge_{i=1}^m \bigwedge_{j=1}^n A_i \lor B_j$

Wie ist die Beziehung von $Sp(A \lor B)$ zu $Sp(A)$ und $Sp(B)$ ?

Die offensichtliche Obergrenze ist $Sp(A \lor B) \leq Sp(A) + Sp(B) -1$ . Ist das eng?

cc.complexity-theory lo.logic proof-complexity proof-search MassimoLauria
quelle

Gute Frage! Kennen Sie die Antwort für die Größe der direkten Summe? Ich denke, der schlimmste Fall ist, wenn A und B keine gemeinsamen Variablen haben. Ein interessanter Fall könnte sein, wenn A und B bis zum Umbenennen der Variablen gleich sind. Übrigens sehe ich nicht, wie Sie diese Obergrenze erreichen, es fühlt sich an, als könnte es viel schlimmer sein.

Kaveh

B

$B$

A_{i} \lor B_{j}

$A_i \lor B_j$

1 \leq j \leq n

$1 \leq j \leq n$

A_{i}

$A_i$

1 \leq i \leq m

$1 \leq i \leq m$

A

$A$

m . (S i z e (B) + O (1)) + S i z e (A)

$m.(Size(B)+O(1))+Size(A)$ .

Kaveh

F_{1} \lor F_{2} \lor \dots F_{k}

$F_1 \lor F_2 \lor \ldots F_k$

F_{i}

$F_i$

F

$F$

L e n g t h (A \lor B) \leq L e n g t h (B) | A | + L e n g t h (A)

$Length(A \lor B) \leq Length(B)|A|+Length(A)$

Die Trivialraum-Obergrenze erfordert tatsächlich eine Klausel weniger im Speicher. Ich habe entsprechend bearbeitet.

MassimoLauria

Antworten:

Ich wollte dies als Kommentar posten, aber da ich den Weg dazu nicht genau herausfinden kann, muss es stattdessen eine "Antwort" sein.

Ich stimme zu, dass die Frage nett ist. Dieselbe Frage kann natürlich auch über die Länge der Widerlegungen der Auflösung (dh die Anzahl der in der Widerlegung auftretenden Klauseln, gezählt mit Wiederholungen) und die Breite der Widerlegung (dh die Größe oder Anzahl der in der Widerlegung auftretenden Literale) gestellt werden , die größte Klausel in der Widerlegung).

In all diesen Fällen gibt es "offensichtliche" Obergrenzen, aber mir ist nicht klar, ob man mit übereinstimmenden Untergrenzen rechnen sollte oder nicht. Daher wollte ich eine Frage und einen Kommentar hinzufügen.

Die Frage betrifft die Widerlegungsdauer. Es scheint vernünftig zu glauben, dass die im Kommentar von Massimo angegebene Längengrenze eng ist, aber wissen wir das?

$A$ $B_i$ $w_A$ $B$ $B$ $w_B$ $\max (w_A, w_B)$

Dies ist natürlich eine einfache Beobachtung, aber der Punkt ist, dass es darauf hindeuten könnte, dass die Frage nach dem Raum schwierig sein könnte. Dies ist so, da fast alle unteren Grenzen des Raums in der Widerlegung, von denen wir wissen, über die unteren Grenzen der Breite gehen. (Das heißt, die unteren Raumgrenzen wurden unabhängig voneinander abgeleitet, aber im Nachhinein folgen sie alle als Folge des schönen Papiers "Eine kombinatorische Charakterisierung der Auflösungsbreite" von Atserias und Dalmau.) Aber wenn es einen direkten Summensatz für die Auflösungsklausel gibt Raum, es wird nicht aus Breite Untergrenzen folgen, sondern muss direkt argumentiert werden, was zumindest bisher viel schwieriger schien. Aber natürlich könnte es ein leichtes Argument geben, das mir fehlt.

Jakob Nordstrom
quelle

Willkommen, Jakob!

Arnab

Kommentare sind leider auf Personen mit einem Ruf von mindestens 50 beschränkt - dies ist eine Seltsamkeit der Software und bezieht sich auf die Spam-Prävention. Ich bin sicher, Sie werden diese Schwelle schnell überschreiten.

Suresh Venkat

Hallo Jakob, es ist schön dich hier zu sehen. (ps: Ich denke, Sie haben die Schwelle überschritten.)

Kaveh

Hallo Jakob, ich frage mich, ob diese Art von Aussage einige Konsequenzen in Bezug auf Kompromisse hat. Als Technik der unteren Grenze wäre dies kein sehr leistungsfähiges Werkzeug: Die Formellänge quadriert, während der Raum linear zunimmt. Auf jeden Fall kann diese Eigenschaft zu einer Formel mit kleiner Breite und großem Raum führen (beachten Sie, dass auch die Breite zunimmt, wenn eine nicht konstante Anzahl von Wiederholungen durchgeführt wird).

MassimoLauria