Reducir el siguiente problema a SAT

Question

Aquí está el problema.Dado $k, n, T_1, \ldots, T_m$, donde cada $T_i \subseteq \{1, \ldots, n\}$.¿Existe un subconjunto $S \subseteq \{1, \ldots, n\}$ con un tamaño como máximo $k$ tal que $S \cap T_i eq \emptyset$ para todos los $i$?Estoy intentando reducir este problema al SAT.Mi idea de solución sería tener una variable $x_i$ para cada uno de 1 a $n$.Para cada $T_i$, cree una cláusula $(x_{i_1} \vee \cdots \vee x_{i_k})$ si $T_i = \{i_1, \ldots, i_k\}$.Luego y todas estas cláusulas juntas.Pero esto claramente no es una solución completa ya que no representa la restricción de que $S$ debe tener como máximo $k$ elementos.Sé que debo crear más variables, pero simplemente no estoy seguro de cómo.Entonces tengo dos preguntas:

1. ¿Mi idea de solución va por buen camino?
2. ¿Cómo se deben crear las nuevas variables para que puedan usarse para representar la restricción de cardinalidad $k$?

Answer 1

Parece que estás tratando de calcular un transversal de hipergrafio de tamaño $ k $. Es decir, $ {t_1, dots, t_m } $ es su hipergrafio, y $ S $ es su transversal. Una traducción estándar es expresar las cláusulas como lo ha hecho, y luego traducir la restricción de longitud en una restricción de cardinalidad.

Así que use su codificación existente, es decir, $ bigwedge_ {1 le j le m} bigVee_ {i in t_j} x_i $ y luego agregue cláusulas que codifiquen $ sum_ {1 le i le n} x_i le K $.

$ sum_ {1 le i le n} x_i le k $ es una restricción de cardinalidad. Hay varias traducciones diferentes de restricción de cardinalidad al SAT.

La traducción de restricción de cardinalidad más simple pero bastante grande es solo $ bigwedge_ {x subseteq {1, dots, n }, | x | = k+1} bigVee_ {i in x} neg x_i $. De esta manera, cada disyunción representa la restricción $ neg bigwedge_ {i in x} x_i $ - para todos los subconjuntos $ x $ de $ {1, dots, n } $ de tamaño k+1. Es decir, nos aseguramos de que no haya forma de que se puedan establecer más de K variables. Tenga en cuenta que este no es un tamaño polinomial en $ k $

Algunos enlaces a documentos sobre traducciones de restricción de cardinalidad más eficiente que son de tamaño polinómico en $ k $:

• Traducir las limitaciones pseudo-booleanas al SAT - Niklas Eén y Niklas Sörensson, JSAT Vol 2 (2006), PG 1-26 (una buena encuesta).
• Codificación de CNF eficiente de restricciones de cardinalidad booleana - Olivier Bailleux y Yacine Boufkhad, Actas de principios y práctica de la programación de restricciones 2003, LNCS Vol 2833, PG 108-122 (una traducción agradable y bastante fácil de implementar).
• Hacia una codificación óptima de CNF de restricciones de cardinalidad booleana - Carsten Sinz - Actas de principios y práctica de la programación de restricciones 2005, LNCS 3709, PG 827-831.
• Hacia las codificaciones sólidas de CNF de las limitaciones de cardinalidad -Joao Marques-Silva e Inês Lynce, Actas de principios y práctica de la programación de restricciones 2007, LNCS 4741, PG 483-497.

Si realmente está interesado en resolver tales problemas, tal vez sea mejor formularlos como problemas pseudo-booleanos (ver Artículo de Wiki sobre problemas pseudo-booleanos) y use solucionadores pseudo-booleanos (ver competencia pseudo-booleana). De esa manera, las limitaciones de cardinalidad son solo limitaciones pseudo-booleanas y son parte del lenguaje; con suerte, el solucionador pseudo-booleano las maneja directamente y, por lo tanto, de manera más eficiente.

Answer 2

Si no está absolutamente establecido en el SAT normal, su idea ya es una reducción a Min-Uns (sobre fórmulas CNF positivas), que básicamente es SAT, pero donde puede establecer como máximo las variables de $ K $ a verdaderas (estrictamente es la versión de optimización donde minimizamos el número de variables verdaderas).

De manera similar, si se dirige en una dirección de complejidad parametrizada, entonces básicamente ya tiene wsat ($ gamma_ {2,1}^{+} $), donde $ gamma_ {2,1}^{+} $ es el es el es el Clase de todas las fórmulas CNF positivas (igual que antes, la notación podría ayudar a sus investigaciones). En este caso, tendría que comenzar a ver qué parametrización sería útil en su caso.

Supongo que estás buscando una reducción explícita, pero si no, siempre puedes volver a ser el Teorema de Cook-Levin.