Polynomiell zeitlösbare Instanzen von Max-Sat

18

Das Problem Max-Sat fordert Sie auf, eine Zuordnung einer CNF-Formel zu finden, die möglichst viele Klauseln erfüllt.

Für das einfachere Problem SAT gibt es viele bekannte Spezialfälle, die in Polynomzeit gelöst werden können, zB können wir 2-SAT in Polynomzeit lösen.

Für Max-Sat ist die Situation anders, da Max-Sat auch für 2-CNF-Formeln NP-hart ist (jede Klausel enthält nur 2 Variablen).

Gibt es interessante spezielle Eingänge, für die Max-Sat polynomisch ist?

Insbesondere würde mich eine Standardreferenz zum Lösen von Max-Sat interessieren, wenn der Inzidenzgraph die Baumbreite begrenzt hat.

sat treewidth max2sat Martin Vatshelle
quelle

3

Planar max-cut ist ein Sonderfall von max-cut, in gewisser Weise ein Sonderfall von max-2-sat.

Jukka Suomela

6

Dies beantwortet Ihr Max-SAT-Problem nicht direkt, aber die Referenzen können Sie zur vollständigen Antwort führen.

Szeider hat gezeigt, dass die Zufriedenheit fest parametrierbar ist, wenn sie durch die Breite des Inzidenzgraphen parametrisiert wird. Samer und Szeider gaben einen effizienten dynamischen Programmieralgorithmus.

Verweise

S. Szeider. Festparametrierbare Parametrierungen von SAT. In Proc. 6. Internationale Konferenz über Theorie und Anwendungen der Zufriedenheit (SAT'03), Selected and Revised Papers, vol. 2919 von LNCS, Seiten 188–202. Springer-Verlag, 2004.

M. Samer und S. Szeider. Algorithmen zum Zählen von Aussagenmodellen. In Proc. 14. Internationale Konferenz über Logik für Programmierung, künstliche Intelligenz und Argumentation (LPAR'07), vol. 4790 von LNCS, Seiten 484–498. Springer-Verlag, 2007.

Samer und Szeider, Tractability mit festen Parametern. In A. Biere, M. Heule, H. van Maaren und T. Walsh, Herausgeber, Handbuch der Zufriedenheit, Teil 1, Kapitel 13. IOS Press

Mohammad Al-Turkistany
quelle

Ich weiß, dass einige von Stefan Szeiders Arbeiten, eine neuere Veröffentlichung zeigt, dass #SAT polynomisch ist, wenn das Inzidenzdiagramm eine begrenzte Clique-Breite hat, die auch eine begrenzte Tree-Breite impliziert (obwohl wir hier XP-Laufzeit anstelle von FPT haben). Friedrich Slivovsky und Stefan Szeider, Modellzählung für Formeln der begrenzten Cliquenbreite, Algorithmen und Berechnung, vol. 8283, p. 677-687, LNCS, 2013 Ich weiß, dass diese Art von Ergebnissen oft in MAX-SAT übersetzt wird, aber es wäre viel einfacher, eine Referenz zu haben, in der dies bereits erfolgt, anstatt es selbst zu tun.

Martin Vatshelle

0

Wir haben eine Art solcher Immobilien gefunden:

$F$ $F$ $x$ $C$ $x$ $C$ $C$ $C$ $x$ $x$

siehe: http://arxiv.org/abs/1402.6485

Sind noch andere Eigenschaften bekannt?

Martin Vatshelle
quelle

Polynomiell zeitlösbare Instanzen von Max-Sat

Antworten: