Das Problem der maximalen Erfüllbarkeit (Max-Sat) ist das Problem, die maximale Anzahl von Klauseln zu finden, die in einer Booleschen Erfüllbarkeitsinstanz erfüllt werden können. Das genau 1: 2-Sat-Problem fragt, ob es bei einer Reihe von Klauseln mit jeweils zwei Literalen eine Reihe von Literalen gibt, sodass jede Klausel genau ein Literal aus dieser Menge enthält.
Die Komplexität der Auswahl einzigartiger Entscheidungen: Die Approximation von 1-in-k-SAT durch Guruswami und Trevisan bietet eine Methode zur Approximation von Max 1 in 2 Sat. Sie geben monoton an (keine negierten Literale). Max 1 in 2 Sat "lässt eine e-Approximation in der Polynomzeit zu".
Ich möchte einen genauen Algorithmus für das max monotone 1 in 2 Sat-Problem finden.
graph-algorithms
sat
max2sat
Russell Easterly
quelle
quelle
Antworten:
Eine monotone 1-in-2-Klausel verlangt, dass die beiden Variablen unterschiedliche Werte haben. Auf diese Weise können Sie das Problem als Diagrammproblem modellieren, mit einem Scheitelpunkt pro Variable, der schwarz oder weiß gefärbt werden soll, und einer Kante für eine Klausel, die angibt, dass die Farben unterschiedlich sein müssen. Daher besteht die Frage darin, den Graphen durch Löschen einer minimalen Anzahl von Kanten zweiteilig zu machen. Dies ist das MaxCut- oder Edge Bipartization-Problem. Es ist NP-schwer.
Für die Kanten-Bipartisierung gibt es einen Algorithmus , der schnell ausgeführt wird, wenn nur wenige Kanten gelöscht werden müssen. Ich habe eine Implementierung für ein etwas allgemeineres Problem geschrieben, das hier beschrieben wird ( Quellcode ).
quelle
quelle