Fórmulas mínimas insatisfactorias de 3-CNF

Actualmente estoy interesado en obtener (o construir) y estudiar fórmulas 3-CNF que son insatisfactorias y de tamaño mínimo. Es decir, deben consistir en la menor cantidad posible de cláusulas (m = 8 preferiblemente) y la menor cantidad posible de variables distintas (n = 4 o más), de modo que eliminar al menos una cláusula haga que la fórmula sea satisfactoria.

Más formalmente, cualquier fórmula F de 3-CNF elegible debe cumplir las siguientes condiciones:

F es insatisfactorio
F tiene una cantidad mínima (4+) de variables distintas (o su negación)
F tiene una cantidad mínima de cláusulas (8+)
cada subconjunto apropiado de F es satisfactoria (permitiendo la eliminación de cualquier cláusula o cláusulas arbitrarias).
F no tiene 2 cláusulas que sean reducibles a una cláusula 2-CNF, por ejemplo, (i, j, k) & (i, j, ~k)NO está permitido (se reducen a (i,j))

Por ejemplo, con n = 4, existen muchas fórmulas mínimas de 8 cláusulas 3-CNF que son insatisfactorias. Por un lado, al mirar el 4 hipercubo e intentar cubrirlo con bordes (2 caras), se puede construir la siguiente fórmula insatisfactoria:

1. (~A,  B,  D)
2. (~B,  C,  D)
3. ( A, ~C   D)
4. ( A, ~B, ~D)
5. ( B, ~C, ~D)
6. (~A,  C, ~D)
7. ( A,  B,  C)
8. (~A, ~B, ~C)

Esto califica como una fórmula mínimamente insatisfactoria de 3-CNF porque:

Es insatisfactorio:
- Las cláusulas 1-3 son equivalentes a: D or A=B=C
- Las cláusulas 4-6 son equivalentes a: ~D or A=B=C
- Implican A=B=C, pero según las cláusulas 7 y 8, esto es una contradicción.
Solo hay 4 variables distintas.
Solo hay 8 cláusulas.
Eliminar cualquier cláusula la hace satisfactoria.
No hay 2 cláusulas 'reducibles' a una cláusula 2-CNF.

Entonces, creo que mis preguntas generales aquí son, en orden de importancia para mí:

¿Cuáles son algunas otras fórmulas mínimas pequeñas que cumplen con las condiciones anteriores? (es decir, por ejemplo, 4,5,6 variables y 8,9,10 cláusulas)
¿Existe algún tipo de base de datos o "atlas" de tales fórmulas mínimas?
¿Qué algoritmos no aleatorios existen para construirlos directamente, si los hay?
¿Cuáles son algunas ideas sobre las características de estas fórmulas? ¿Se pueden contar o estimar, dadas n (# variables) ym (# cláusulas)?

Gracias de antemano por sus respuestas. Agradezco cualquier respuesta o comentario.

cc.complexity-theory sat MAF
fuente

Cada cláusula 3-CNF no permite 1/8 de las posibles soluciones. Claramente, siempre necesita al menos 8 cláusulas, o más, si los conjuntos de soluciones no permitidas se superponen. Dado que su condición 5 prohíbe conjuntos no superpuestos de soluciones no permitidas para n = 3, necesita más de 8 cláusulas para este caso: tenga en cuenta que su ejemplo no obedece a la condición 5.

András Salamon

Sí, tienes razón en todos los puntos, András. 8 cláusulas son un mínimo requerido para una fórmula 3-CNF insatisfactoria, por lo que la condición 5 puede ser demasiado restrictiva para mis propósitos al encontrar / construir fórmulas calificativas. Me doy cuenta de que para n = 3, la condición 5 debe violarse necesariamente, pero se incluyó solo con fines ilustrativos. Estoy estrictamente interesado en calificar fórmulas de tamaño n = 4 + (es decir, 4 o más variables, pero no demasiadas más). Quizás rascaré la condición 5.

MAF

Creo que su "ejemplo" con n = 3 es confuso más que ilustrativo, porque (como señaló András en su comentario) no es realmente un ejemplo de lo que está preguntando en esta pregunta. El ejemplo con n = 4 es perfectamente fino e ilustrativo. ¿Por qué no eliminas el ejemplo con n = 3?

Tsuyoshi Ito

Buen punto, Tsuyoshi. Hecho.

MAF

@MAF: la eliminación de la condición 5 da como resultado un ejemplo trivial: comience con la instancia no satisfactoria que contiene las cláusulas y , luego reemplace cada cláusula con dos cláusulas y para una variable nueva , y continúe hasta que todas las cláusulas tengan 3 literales. Esto produce una fórmula de 7 variables insatisfactorias con 8 cláusulas. Esto es solo dividir el espacio de la solución en 8 piezas disjuntas, que generalmente no es un código interesante.

{x}

$\{x\}$

{x^{'}}

$\{x'\}$

C

$C$

C \cup {v}

$C \cup \{v\}$

C \cup {v^{'}}

$C \cup \{v'\}$

v

$v$

András Salamon

Respuestas:

Tome la fórmula en su ejemplo, elimine la cláusula y agregue las siguientes cláusulas: $\lnot A \lor \lnot B \lor \lnot C$ $2$

$\lnot A \lor \lnot B \lor \lnot E$
$\lnot B \lor \lnot C \lor E$

Obtendrá una fórmula mínima insatisfactoria con , obedeciendo la condición 5. $n=5$ $m=9$

En general, puede elegir aleatoriamente una cláusula y dividirla en cláusulas: $l_1 \lor l_2 \lor l_3$ $2$

$l_1 \lor l_2 \lor v$
$l_2 \lor l_3 \lor \lnot v$

donde es una nueva variable. Cada vez que lo hace, tanto como se incrementan en . La repetición de este proceso le permite "estirar" el núcleo inicial insatisfactorio y obtener fórmulas mínimas insatisfactorias (obedeciendo la condición 5) cuya tiende a medida que crece (lo cual es bastante raro, como fórmulas con son satisfactorios con alta probabilidad). $v$ $n$ $m$ $1$ $r=\frac{m}{n}$ $1$ $n$ $r=1$

Giorgio Camerani
fuente

Gracias por la respuesta, Walter. El procedimiento que describe es realmente muy útil para generar fórmulas mín. Un poco más grandes aún más pequeñas de estructura 'similar', es decir, una vez que tiene un conjunto central que considera que tiene propiedades interesantes.

MAF

@MAF: De nada. Gracias por publicar una pregunta tan interesante.

Giorgio Camerani

Creo que la condición número 5 no se cumple realmente en su ejemplo y no se puede mantener nunca.
Que las siguientes cláusulas sean equivalentes:

( p, q) = (~A,B,D)(A,~B,~D)

Lo que nos permitirá asignar las cláusulas de A, B, C y D a las nuevas variables p, q, r y s como la siguiente tabla de verdad:

A B C D | p q r s
-----------------
0 0 0 0 | 0 1 0 0
0 0 0 1 | 0 1 0 1
0 0 1 0 | 0 1 1 0
0 0 1 1 | 0 1 1 1
-----------------
0 1 0 0 | 1 0 0 0
0 1 0 1 | 0 0 0 0
0 1 1 0 | 1 0 0 1
0 1 1 1 | 0 0 0 1
-----------------
1 0 0 0 | 0 0 1 0
1 0 0 1 | 1 0 1 0
1 0 1 0 | 0 0 1 1
1 0 1 1 | 1 0 1 1
-----------------
1 1 0 0 | 1 1 0 0
1 1 0 1 | 1 1 0 1
1 1 1 0 | 1 1 1 0
1 1 1 1 | 1 1 1 1
-----------------

Y ahora podemos expresar las cláusulas de A, B, C y D en términos de p, q, r y s:

1. (~A,  B,  D) = ( p, q,~r, s)( p, q,~r,~s)
2. (~B,  C,  D) = (~p, q, r, s)(~p,~q, r, s)
3. ( A, ~C   D) = ( p,~q,~r, s)(~p, q, r,~s)
4. ( A, ~B, ~D) = ( p, q, r, s)( p, q, r,~s)
5. ( B, ~C, ~D) = ( p,~q,~r,~s)(~p, q,~r,~s)
6. (~A,  C, ~D) = (~p, q,~r, s)(~p,~q, r,~s)
7. ( A,  B,  C) = ( p,~q, r, s)( p,~q, r,~s)
8. (~A, ~B, ~C) = (~p,~q,~r, s)(~p,~q,~r,~s)

Dado que todas las cláusulas se muestran y se asocian con las cláusulas A, B, C y D. Entonces podemos afirmar que las cláusulas p, q, r y s pueden reducirse a:

( p, q, r)
( p, q,~r)
( p,~q, r)
( p,~q,~r)
(~p, q, r)
(~p, q,~r)
(~p,~q, r)
(~p,~q,~r)

Lo que obviamente viola la condición número 5.

Lo que quiero señalar es que incluso el ejemplo no muestra explícitamente que hay 2 cláusulas que pueden reducirse a 2-CNF, pero implícitamente es has (por ejemplo, (~ A, B, D) y (A, ~ B, ~ D)), es posible que no pueda expresar el 2-CNF con las variables dadas, pero cuando introduzca una asignación diferente para el problema podrá expresarlas.

Khazam Alhamdan
fuente