Una fórmula 3-CNF que requiere un ancho de resolución

13

Recordemos que la anchura de una resolución refutación de una fórmula CNF es el número máximo de literales en cualquier cláusula que ocurre en . Para cada , hay fórmulas insatisfactorias en 3-CNF st cada refutación de resolución de requiere un ancho de al menos .F R w F F wRFRwFFw

Necesito un ejemplo concreto de una fórmula insatisfactoria en 3-CNF (tan pequeña y simple como sea posible) que no tiene una resolución de refutación de ancho 4.

Jan Johannsen
fuente
¿Necesita exactamente el ancho 5 o al menos el ancho 5? En el último caso, supongo que pocas cláusulas aleatorias en un puñado de variables funcionarán. Sin embargo, no es muy agradable ni muy pequeño.
MassimoLauria
1
creo que una computadora / búsqueda empírica relativamente directa podría encontrar esto o descartarlo. También creo que hay algo más general / interesante teoría inexplorada al acecho aquí. ver también en pruebas de resolución, ¿son posibles todos los DAG? , buscando volver a abrir los votos si está de acuerdo =) pregunta relacionada: para las fórmulas metro×norte -SAT, ¿qué DAG de resolución de dimensión (s) son posibles?
vzn
Jan, creo que Jacob debería poder responder esto fácilmente. Por cierto, ¿le gustaría generalizar un poco la pregunta y preguntar sobre un método para obtener 3-CNF de ancho de resolución dado?
Kaveh
Massimo, necesito un ejemplo concreto que pueda escribir y explicar en una pizarra más o menos. Entonces las cláusulas aleatorias no servirán.
Jan Johannsen
1
Ahora estoy en la zona horaria equivocada para poder pensar correctamente, pero ¿tal vez sería útil una fórmula de Tseitin sobre un gráfico realmente pequeño (donde podría verificar la expansión a mano)? Pero realmente necesitas un 3-CNF, ¿verdad? Para un 4-CNF, quizás jugaría con una cuadrícula rectangular de dimensiones adecuadas y vería qué sucede. Solo algunos pensamientos a medio cocer ...
Jakob Nordstrom

Respuestas:

14

El siguiente ejemplo proviene del documento que ofrece una caracterización combinatoria del ancho de resolución por Atserias y Dalmau ( Journal , ECCC , copia del autor ).

El teorema 2 del artículo establece que, dada una fórmula CNF , las refutaciones de resolución de ancho como máximo k para F son equivalentes a las estrategias ganadoras para Spoiler en el juego existencial ( k + 1 ) de guijarros. Recordemos que el juego de guijarros existencial se juega entre dos jugadores compiten entre sí, llamados alerón y la duplicadora, y las posiciones del juego son las cesiones parciales de tamaño de dominio a lo sumo k + 1 a las variables de F . En el juego de guijarros ( k + 1 ) , a partir de la asignación vacía, Spoiler quiere falsificar una cláusula de FFkF(k+1)k+1F(k+1)Fmientras recuerda a lo sumo valores booleanos a la vez, y Duplicator quiere evitar que Spoiler lo haga.k+1

El ejemplo se basa en (la negación de) el principio del casillero.

Por cada y j { 1 , ... , n } , sea p i , j una variable proposicional que significa que la paloma i se sienta en el hoyo j . Por cada i { 1 , ... , n + 1 } y j { 0 , ... , n } , dejemosyo{1,...,norte+1}j{1,...,norte}pagyo,jyojyo{1,...,norte+1}j{0 0,...,norte} sea ​​una nueva variable proposicional. La siguientefórmula 3 -CNF E P i expresa que la paloma i se encuentra en algún agujero: E P i¬ y i , 0n j = 1 ( y i , j - 1p i , j¬ y i , j ) y i , n .yyo,j3miPAGyoyo

miPAGyo¬yyo,0 0j=1norte(yyo,j-1pagyo,j¬yyo,j)yyo,norte.
Finalmente, la fórmula -CNF E P H P n + 1 n que expresa la negación del principio del casillero es la conjunción de todas las E P i y todas las cláusulas H i , j k¬ p i , k¬ p j , k para i , j { 1 , ... , n + 1 } , i j y3miPAGHPAGnortenorte+1miPAGyoHkyo,j¬pagyo,k¬pagj,kyo,j{1,...,norte+1},yoj .k{1,...,norte}

El Lema 6 del documento ofrece una prueba bastante corta e intuitiva de que Spoiler no puede ganar el juego de pebbles en E P H P n + 1 n , por lo tanto, E P H P n + 1 n no tiene refutación de resolución de ancho como máximo n - 1 .nortemiPAGHPAGnortenorte+1miPAGHPAGnortenorte+1norte-1

El artículo tiene otro ejemplo en el Lema 9, basado en el principio de orden lineal denso.

Ω(norte(k-3)/ /12)k+1

siuman
fuente
2
miPAGHPAG5 56 6