Codificación de la restricción 1 fuera de n para solucionadores SAT

Estoy usando un solucionador SAT para codificar un problema, y ​​como parte de la instancia SAT, tengo variables booleanas donde se pretende que exactamente una de estas sea verdadera y el resto debería ser falso (A veces he visto esto descrito como una codificación "única").$x_1,x_2,\dots,x_n$

Quiero codificar la restricción "exactamente uno de debe ser verdadero" en SAT. ¿Cuál es la mejor manera de codificar esta restricción, para hacer que el solucionador SAT se ejecute de la manera más eficiente posible?$x_1,\dots,x_n$

Puedo ver muchas formas de codificar esta restricción:

• Restricciones por pares. Podría agregar restricciones por pares para todo i , j para asegurar que a lo sumo un x i sea ​​verdadero, y luego agregar x 1 ∨ x 2 ∨ ⋯ ∨ x n para asegurar que al menos uno sea verdadero.$\neg x_i \lor \neg x_j$$i,j$$x_i$$x_1 \lor x_2 \lor \cdots \lor x_n$

  Esto agrega cláusulas y no variables booleanas adicionales.$\Theta(n^2)$

• Codificación binaria. Pude introducir nuevas variables booleanas i 1 , i 2 , ... , i LG n para representar (en binario) un número entero i tal que 1 ≤ i ≤ n (la adición de unas pocas restricciones booleanas para asegurar que i es en el intervalo deseado ) Luego, puedo agregar restricciones que impongan que x i es un árbol y que todas las otras x j son falsas. En otras palabras, para cada j , agregamos cláusulas que imponen que i = $\lg n$$i_1,i_2,\dots,i_{\lg n}$$i$$1 \le i \le n$$i$$x_i$$x_j$$j$ .$i=j \Leftrightarrow x_j$

  Esto agrega cláusulas y no sé cuántas variables booleanas adicionales.$\Theta(n \lg n)$

• Cuenta el número de valores verdaderos. Podría implementar un árbol de circuitos sumadores booleanos y requerir que , tratando cada x i como 0 o 1 en lugar de falso o verdadero, y use la transformación Tseitin para convertir el circuito a SAT cláusulas Un árbol de media sumadora es suficiente: restringir la salida de acarreo de cada mitad de sumadora a 0, y restringir la salida final de la mitad de sumadora final en el árbol a 1. El árbol se puede elegir para que tenga cualquier forma ( árbol binario balanceado, o no balanceado, o lo que sea).$x_1+x_2+\dots+x_n=1$$x_i$

  Esto se puede hacer en puertas y por lo tanto añade theta ( n ) cláusulas y Θ ( n ) nuevas variables booleanas.$\Theta(n)$$\Theta(n)$$\Theta(n)$

  Un caso especial de este enfoque es introducir variables booleanas , con la idea de que y yo debería contener el valor de x 1 ∨ x 2 ∨ ⋯ ∨ x i . Esta intención puede hacerse cumplir agregando las cláusulas y i ∨ ¬ x i , y i ∨ ¬ y i - 1 , y ¬ y i ∨ x i ∨ y i $y_1,\dots,y_n$$y_i$$x_1 \lor x_2 \lor \cdots \lor x_i$$y_i \lor \neg x_i$$y_i \lor \neg y_{i-1}$ (donde tratamos y 0 como sinónimo de falso) parai=1,…,n. A continuación, podemos agregar las restricciones¬ y i ∨¬ x i + 1 parai=1,2,...,n-1. Esto es básicamente equivalente a la transformación Tseitin de un árbol de medio sumador, donde el árbol tiene una forma máximamente desequilibrada.$\neg y_i \lor x_i \lor y_{i-1}$$y_0$$i=1,\dots,n$$\neg y_i \lor \neg x_{i+1}$$i=1,2,\dots,n-1$

• Red de mariposas. I podría construir una red mariposa en bits de, limitar el n de entrada bits para ser 000 ⋯ 01 , restringir el n salida de bits a ser x 1 x 2 ⋯ x n , y tratar a cada puerta de mariposa 2 bits como una puerta independiente que intercambia o no intercambia su entrada con la decisión de qué hacer basándose en una nueva variable booleana nueva que se deja sin restricciones. Entonces, puedo aplicar la transformación Tseitin para convertir el circuito a cláusulas SAT.$n$$n$$000\cdots 01$$n$$x_1 x_2 \cdots x_n$

  Esto requiere puertas y por lo tanto añade Θ ( n lg n ) cláusulas y Θ ( n lg n ) nuevas variables booleanas.$\Theta(n \lg n)$$\Theta(n \lg n)$$\Theta(n \lg n)$

¿Hay algún otro método que haya pasado por alto? ¿Cuál debo usar? ¿Alguien ha probado esto o los ha probado experimentalmente, o alguien tiene alguna experiencia con alguno de estos? ¿Es el número de cláusulas y / o el número de nuevas variables booleanas una buena métrica sustituta para estimar el impacto de esto en el rendimiento del solucionador SAT, o si no, qué métrica usaría?

Acabo de notar que esta respuesta tiene algunas referencias sobre el cumplimiento de las restricciones de cardinalidad para SAT, es decir, el cumplimiento de la restricción de que exactamente de las n variables son verdaderas. Entonces, mi pregunta se reduce a un caso especial donde k = 1 . Tal vez la literatura sobre restricciones de cardinalidad ayudará a arrojar luz sobre mi pregunta.$k$$n$$k=1$

Para el caso especial de k de n variables verdaderas donde k = 1, existe una codificación de variable comandante como se describe en Codificación eficiente de CNF para seleccionar 1 a N objetos por Klieber y Kwon. Simplificado: Divida las variables en pequeños grupos y agregue cláusulas que hagan que el estado de una variable comandante implique que un grupo de variables es falso o todo es falso. Luego aplique recursivamente el mismo algoritmo a las variables del comandante. Al final del proceso, exija que se cumpla exactamente una de las variables finales del comandante. El resultado es O (n) nuevas cláusulas y O (n) nuevas variables.

Dada la ubicuidad de dos literales vistos en solucionadores basados ​​en DPLL, creo que el crecimiento de la cláusula O (n) es una ventaja decisiva sobre los esquemas de codificación que agregarían más cláusulas.

Un artículo de Magnus Björk describe dos técnicas que vale la pena probar.

Para 1-de- , uno puede usar tanto la codificación one-hot como la codificación binaria simultáneamente. Por lo tanto, tenemos x 1 , ... , x n como codificación de un solo hot, e y 1 , ... , y b como codificación binaria, donde b = lg n . Podemos codificar la restricción "al menos uno" fácilmente, en una sola cláusula: ( x 1 ∨ ⋯ ∨ x n ) . También podemos forzar que las dos codificaciones sean consistentes con 2 lg $n$$x_1,\dots,x_n$$y_1,\dots,y_b$$b = \lg n$$(x_1 \lor \dots \lor x_n)$$2 \lg n$cláusulas: simplemente agregamos o x $x_i \implies \neg y_j$ , según si elbit número j de la codificación binaria de i es 0 o 1. Finalmente, la restricción "a lo sumo" sigue automáticamente. Esto también permite que el resto de la instancia SAT use la codificación que sea más conveniente.$x_i \implies y_j$$j$$i$

Para -out-of- n , se puede aplicar una red de clasificación a la entrada x 1 , ... , x n para obtener la salida ordenada y 1 , ... , y n , y luego agregar una cláusula que requiera que y k sea ​​verdadero y y k + 1 es falso. Existen varias redes de clasificación simples que solo necesitan unidades de comparación O ( n lg 2 n ) . Por lo tanto, obtenemos una codificación que usa O ( n lg $k$$n$$x_1,\dots,x_n$$y_1,\dots,y_n$$y_k$$y_{k+1}$$O(n \lg^2 n)$$O(n \lg^2 n)$

El papel es

Magnus Björk. Técnicas de codificación SAT exitosas . 25 de julio de 2009.

$n$$k$$n$

Alan M. Frisch, Paul A. Giannaros. Codificaciones SAT de la restricción a lo sumo k: algunas viejas, algunas nuevas, algunas rápidas, algunas lentas . ModRef 2010.