Graphentheoretische Beschränkung auf Beweise in der Beweiskomplexitätstheorie

Die Komplexität von Beweisen ist ein grundlegendster Bereich der Theorie der rechnerischen Komplexität. Ein letztendlicher Zweck dieses Bereichs besteht darin, zu beweisen , dh, jeder Prüfer kann keinen Beweis für die Unzufriedenheit der gegebenen Eingabeformel erbringen. $NP\neq coNP$

Ein Graph ist ein formales Beweismodell. Meine Frage betrifft eine weitere Einschränkung dieses Modells.

Ein Beweis wird als DAG dargestellt. Knoten mit Fan-In 0 haben Axiom-Labels. Der eindeutige Knoten mit Fan-Out 0 entspricht "false". Für gegebene Eingaberegeln für den Abzug hat jeder Knoten, der sowohl In-Grad- als auch Out-Grad hat, die Bezeichnung, die den Satz darstellt.

Meine Frage ist:

Gibt es Beweissysteme und verwandte Untersuchungen für den Fall, dass die Klasse der Beweis-DAGs eingeschränkt ist? Beiträge, Umfragen und Vorlesungsunterlagen sind willkommen.

Haben zuvor untersuchte Beweissysteme wie Nullstellensatz, Auflösung, LS, AC0-Frege, RES (k), Polynomkalukulus und Schnittebenen eine graphentheoretische Charakterisierung?

Die natürlichste Einschränkung für die Beweis-DAG ist, dass es sich um einen Baum handelt - das heißt, jedes "Lemma" (Zwischenschluss) wird nicht mehr als einmal verwendet. Diese Eigenschaft wird als "baumartig" bezeichnet. Die allgemeine Auflösung ist exponentiell leistungsfähiger als die baumartige Auflösung, wie beispielsweise von Ben-Sasson, Impagliazzo und Wigderson gezeigt . Das Konzept wurde auch für andere Beweissysteme in Betracht gezogen - suchen Sie einfach nach "baumartigem X", wobei X ein für Sie interessantes Beweissystem ist. Im besonderen Fall der Auflösung können andere Einschränkungen berücksichtigt werden. Siehe zum Beispiel ein Papier von Alekhnovich, Johannsen, Pitassi und Urquhart zur regelmäßigen Lösung.

Die baumartige Auflösung ist besonders wichtig, da herkömmliche Implementierungen von DPLL den Widerlegungen der baumartigen Auflösung entsprechen. Die in der Praxis wichtige Technik des Klausellernens entspricht dem Zulassen allgemeiner DAGs. Daher hängt die Struktur der Beweis-DAG auch stark von dem Algorithmus ab, der sie erzeugt.

Müller und Szeider untersuchen Auflösungsbeweise, bei denen die Beweis-DAG die Baumbreite oder die Pfadbreite begrenzt hat (für geeignete Erweiterungen dieser Graphenkomplexitätsmaße auf gerichtete Graphen).

Sie zeigen, dass die Pfadbreite der DAG im Wesentlichen der räumlichen Komplexität des Beweises entspricht, und definieren einen verallgemeinerten Begriff des Beweisraums, der der Baumbreite entspricht.

Für ausreichend starke Beweissysteme scheint die grafische Darstellung eines Beweises im System weniger folgenreich zu sein, da (wie Joshua Grochow bereits kommentierte) DAG-ähnliche und baumartige Frege-Beweise polynomiell äquivalent sind (siehe Krajiceks Monographie von 1995 für einen Beweis dieser Tatsache ).

Bei schwächeren Beweissystemen wie der Auflösung ist baumartig exponentiell schwächer als DAG-ähnliche Beweise (wie Yuval Filmus oben beschrieben).

Beckmann und Buss [1] (nach Beckmann [2] ) erwogen, die Höhe (äquivalent Tiefe) des Proof-Graphen von Frege-Proofs mit konstanter Tiefe zu beschränken, und untersuchten die Beziehung zwischen DAG-ähnlich, Baumgröße und Höhe mit konstanter Tiefe Frege Beweise. (Beachten Sie den Unterschied zwischen der Einschränkung der Tiefe des Proof-Graphen und der Einschränkung der Tiefe eines Schaltkreises, der in einer Proof-Linie erscheint.)

Es kann auch Trennungen zwischen baumartigen und DAG-ähnlichen Nullstellensatz- (und Polynomkalkül-) Beweisen geben, an die ich mich derzeit nicht erinnere.