MAX 1 en 2 Algoritmo SAT

8

El problema de máxima satisfacción (Max-Sat) es el problema de encontrar el número máximo de cláusulas que se pueden satisfacer en una instancia de satisfacción booleana. El problema exacto 1 en 2 Sat pregunta, dado un conjunto de cláusulas cada una con dos literales, ¿hay un conjunto de literales de tal manera que cada cláusula tenga exactamente un literal de este conjunto?

La complejidad de tomar decisiones únicas: Aproximando 1-en-k SAT por Guruswami y Trevisan ofrece un método para aproximar Max 1 en 2 sáb. Indican monótono (sin literales negados) Máx. 1 en 2 Sat "admite una aproximación electrónica en tiempo polinomial".

Me gustaría encontrar un algoritmo exacto para el problema Max monotone 1 in 2 Sat.

graph-algorithms sat max2sat Russell Easterly
fuente

1

Monotone 1-in-Ek admite una aproximación

, pero esto es interesante solo para

: para

una asignación aleatoria funciona mejor. Monotone 1-in-E2 es MaxCut y admite una aproximación de

dada por el algoritmo Goemans-Williamson.

e

$e$

k \geq 4

$k\geq 4$

k < 4

$k <4$

1.138

$1.138$

Sasho Nikolov

16

Una cláusula monótona 1 en 2 exige que las dos variables tengan valores diferentes. Por lo tanto, puede modelar el problema como un problema gráfico, con un vértice por variable que debe ser de color negro o blanco, y un borde para una cláusula que indica que los colores deben ser diferentes. Por lo tanto, la pregunta es hacer que el gráfico sea bipartito eliminando un número mínimo de aristas. Este es el problema de MaxCut o Edge Bipartization. Es NP-duro.

Para Edge Bipartization, hay un algoritmo que se ejecuta rápidamente cuando se necesitan eliminar algunos bordes. Escribí una implementación para un problema un poco más general descrito aquí ( código fuente ).

Falk Hüffner
fuente

Gracias. Hay una manera simple de transformar el problema monótono Exactamente 1 en 3 SAT en un problema de conjunto independiente ponderado máximo. Si una instancia es solucionable, el gráfico asociado puede hacerse bipartito eliminando un borde de cada cláusula. Espero que ciertas propiedades de 1 en 3 SAT hagan que MaxCut sea más fácil en este tipo de gráficos. Por ejemplo, 1 de cada 3 SAT tiene poderosas reglas de reducción .

Russell Easterly

14

$2^n$ $O(1.8^n)$

$O(n)$

Ryan Williams
fuente

Gracias. Dimitris Achlioptas ha demostrado que la cláusula de transición de fase a relación variable para 1 en 3 SAT es 1/3. Las instancias de 1 en 3 SAT solucionables tendrán gráficos asociados con relaciones de borde bajo a vértices.

Russell Easterly

@RussellEasterly No realmente, esto solo es cierto para la mayoría de las instancias solucionables.

Sasho Nikolov

MAX 1 en 2 Algoritmo SAT

Respuestas: