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 w
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.
cc.complexity-theory
lo.logic
sat
proof-complexity
Jan Johannsen
fuente
fuente
Respuestas:
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 FF k F (k+1) k+1 F (k+1) F mientras 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.
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 .norte miPAGHPAGn + 1norte miPAGHPAGn + 1norte n - 1
El artículo tiene otro ejemplo en el Lema 9, basado en el principio de orden lineal denso.
fuente