Ein einfacher Fall von SAT, der für die Baumauflösung nicht einfach ist

Gibt es eine natürliche Klasse von CNF-Formeln - vorzugsweise eine, die zuvor in der Literatur untersucht wurde - mit den folgenden Eigenschaften:$C$

• ist ein einfacher Fall von SAT, wie z. B. Horn oder 2-CNF, dh die Zugehörigkeit zu C kann in Polynomzeit getestet werden, und die Formeln F ∈ C können auf Erfüllbarkeit in Polynomzeit getestet werden.$C$$C$$F\in C$
• Es ist nicht bekannt, dass unbefriedigende Formeln kurze (polynomiale) baumartige Auflösungs widerlegen. Noch besser wäre: Es gibt in C unbefriedigende Formeln, für die eine Superpolynom-Untergrenze für die baumartige Auflösung bekannt ist.$F\in C$$C$
• Andererseits ist bekannt, dass unbefriedigende Formeln in kurze Beweise in einem stärkeren Beweissystem haben, z. B. in einer dag-ähnlichen Auflösung oder einem noch stärkeren System.$C$

sollte nicht zu spärlich sein, dh viele Formeln mit n Variablen für jedes (oder zumindest für die meisten Werte von) n ∈ N enthalten . Es sollte auch nicht trivial sein, da es sowohl befriedigende als auch unbefriedigende Formeln enthält.$C$$n$$n\in \mathbb{N}$

Der folgende Ansatz zur Lösung einer beliebigen CNF-Formel sollte sinnvoll sein: Finden Sie eine Teilzuordnung α st, die Restformel F α befindet sich in C , und wenden Sie dann den Polynomzeitalgorithmus für Formeln in C auf F α an . Daher möchte ich neben den völlig anderen Einschränkungen andere Antworten als die derzeit akzeptierte Antwort, da ich denke, dass es selten vorkommt, dass eine beliebige Formel nach Anwendung einer Einschränkung zu einer völlig anderen Einschränkung wird.$F$$\alpha$$F\alpha$$C$$C$$F\alpha$

Es hört sich so an, als wären Sie an ganz unterschiedlichen Einschränkungen interessiert (und Ihr letzter Satz ist auf dem richtigen Weg). Dies sind nicht triviale Fälle des Taubenlochprinzips, bei denen die Anzahl der Tauben nicht unbedingt größer als die Anzahl der Löcher ist und außerdem einige Tauben von einigen Löchern ausgeschlossen werden können.

All unterschiedliche Bedingungen können durch Abgleichen in der Polynomzeit niedriger Ordnung entschieden werden.

• Jean-Charles Régin, Ein Filteralgorithmus für Unterschiede in CSPs , AAAI 1994, 362–367.
• DE Knuth und A. Raghunathan, Das Problem kompatibler Vertreter , SIAM J. Discrete Math. 5 422–427, 1992. doi: 10.1137 / 0405033

Wenn alle unterschiedlichen Einschränkungen (unter Verwendung einer von mehreren Codierungen) als SAT-Instanzen ausgedrückt werden, findet das konfliktgesteuerte Lernen von Klauseln normalerweise schnell eine Lösung, wenn es existiert. Bei einer reinen Auflösung für PHP muss jedoch eine superpolynomiell große Menge von Klauseln erstellt werden, um zu zeigen, dass die Instanz nicht zufriedenstellend ist. Diese Grenze gilt eindeutig für dieses allgemeinere Problem. Denken Sie andererseits daran, dass Cooks Codierung des PHP Widerlegungen mit erweiterter Auflösung in Polynomgröße ermöglicht .

• SA Cook, Ein kurzer Beweis des Taubenlochprinzips mit erweiterter Auflösung , SIGACT News 8 28–32, 1976. doi: 10.1145 / 1008335.1008338

Neuere Arbeiten in dieser Richtung sind Kapitel 5 der Arbeit von Sergi Oliva , die die Grundlage für eine Arbeit mit Alberto Atserias auf der CCC 2013 bildete.

Ich gehe davon aus, dass Sie das klassische Ergebnis von Cook kennen. Vielleicht wollten Sie die Leistung des Beweissystems in Ihrem dritten Zustand einschränken?

Ich bin mir nicht sicher, warum man auch Sat-Formeln benötigen würde, aber es gibt einige Artikel über die Trennung zwischen allgemeiner und Baumauflösung, z. B. [1]. Es klingt für mich so, als ob Sie das wollen.

[1] Ben-Sasson, Eli, Russell Impagliazzo und Avi Wigderson. "Nahezu optimale Trennung von baumartiger und allgemeiner Auflösung." Combinatorica 24.4 (2004): 585 & ndash; 603.

Möglicherweise interessieren Sie sich für SAT-Formeln mit kleiner (logarythmischer) "Bandbreite" oder "Baumbreite". Diese Formeln sind rekursiv so partitionierbar, dass die Kommunikationsgrenze zwischen Partitionen klein ist und daher ein enumerativer dynamischer Programmieransatz verwendet werden kann, um sie zu lösen. Das Thema war in den neunziger Jahren beliebt. Ich habe einmal genau die Anzahl der Hamilton-Zyklen in einem kleinen Baumbreitendiagramm mit 24.000 Eckpunkten gezählt, sodass auch # P-Probleme mit kleiner Baumbreite lösbar sind. Bodlaender ist eine wichtige Referenz.

Dieses folgende Papier scheint in gewisser Weise nahe an dem zu sein, was angefordert wird (wenn es nicht passt, kann JJ vielleicht klären, warum). Die Frage möchte PHP-Instanzen (Pigeonhole) aufgrund des Fehlens beider wahrer / falscher Formeln ausschließen, aber (wie in den anderen Antworten zitiert) PHP ist einer der am besten untersuchten Fälle / Instanzgeneratoren von der theoretischen Seite und hat war schon immer ein Generator für beide erfüllbaren / nicht erfüllbaren Formeln, obwohl die zufriedenstellenden Formeln weniger hervorgehoben / untersucht werden.

${^m_n}$$m$$n$$m>n$$m \leq n$

• Die baumartige Auflösung ist superpolynomial langsamer als die DAG-ähnliche Auflösung für das Pigeonhole-Prinzip (1999) von Kazuo Iwama, Shuichi Miyazaki

Ein anderer Ansatz wäre, in einen empirischeren Blickwinkel zu gehen und nur zufällige Instanzen zu generieren (vermutlich um den leicht-schwer-leicht zu 50% erfüllbaren Übergangspunkt) und sie zu filtern, um die angegebenen Kriterien zu erfüllen. man würde Implementierungen von Baumauflösung / DAG-Auflösung oder "stärkeren Systemen" erfordern.