Considere el siguiente problema: dada una fórmula CNF y una asignación que satisface esta fórmula, ¿hay otra asignación satisfactoria para esta fórmula? ¿Cuál es la complejidad de este problema? (Seguramente está en NP, pero ¿también es NP-hard?) ¿Qué sucede si no se le asigna la tarea y solo...
Quiero hacer un primer solucionador SAT. Conozco la competencia SAT y la conferencia SAT, y hay tantos documentos sobre este tema. Soy un abridor, un abrumador abrumador. ¿Dónde debería comenzar? Finalmente quiero impulsar el estado del arte. Quiero un consejo experto sobre cómo comenzar, para no...
¿Qué se sabe sobre la complejidad de encontrar circuitos mínimos que computan SAT hasta una longitud nnn ? Más formalmente: ¿cuál es la complejidad de una función que, dado como entrada, genera un circuito mínimo tal que para cualquier fórmula φ con , ?1n1n1^{n}CCCφφ\varphi|φ|≤n|φ|≤n|\varphi|...
No entiendo por qué casi todos los solucionadores de SAT usan CNF en lugar de DNF. Me parece que resolver SAT es más fácil usando DNF. Después de todo, solo tiene que explorar el conjunto de implicantes y verificar si uno de ellos no contiene tanto una variable como su negación. Para CNF, no existe...
Siguiendo con una pregunta anterior , ¿Cuáles son los mejores límites inferiores del espacio actual para SAT? Con un límite inferior de espacio, me refiero al número de celdas de cintas de trabajo utilizadas por una máquina de Turing que utiliza un alfabeto binario de cintas de trabajo. Un...
Deje que las variables sean . La distancia entre dos variables se define como. La distancia entre dos literales es la distancia entre las dos variables correspondientes. d ( x a , x b ) = | a - b |x1,x2,x3...xnx1,x2,x3...xnx_1 , x_2 , x_3 ... x_nd(xa,xb)=|a−b|d(xa,xb)=|a−b|d(x_a , x_b) =...
¿Alguien podría señalar uno o más sitios web donde sea posible descargar una implementación funcional de un solucionador #SAT? Estoy interesado en aquellos que devuelven el recuento exacto de la solución, no una
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...
El problema de decisión CNF-SAT se puede describir de la siguiente manera: Entrada: Una fórmula booleana en forma conjuntiva normal.ϕϕ\phi Pregunta: ¿Existe una asignación variable que satisfaga ?ϕϕ\phi Estoy considerando varios enfoques diferentes para resolver CNF-SAT con una máquina de Turing...
¿Se ha trabajado en cómo la complejidad de las instancias aleatorias de # 2-SAT varía con la densidad de la cláusula? Es decir: ¿cómo varía la dificultad de contar soluciones satisfactorias para una instancia de 2-SAT generada aleatoriamente , a medida que varía la densidad de la cláusula? En...
El problema Max-Sat le pide que encuentre una asignación de una fórmula CNF que satisfaga tantas cláusulas como sea posible. Para el problema SAT más simple, existen muchos casos especiales conocidos que pueden resolverse en tiempo polinómico, por ejemplo, podemos resolver 2-SAT en tiempo...
Aquí el objetivo es reducir un problema SAT arbitrario a 3-SAT en tiempo polinómico usando el menor número de cláusulas y variables. Mi pregunta está motivada por la curiosidad. Menos formalmente, me gustaría saber: "¿Cuál es la reducción 'más natural' de SAT a 3-SAT?" Ahora la reducción que...
Sea una fórmula CNF satisfactoria con n variables y m cláusulas. Sea S F 1 el espacio de solución de F 1 .F1F1F_1nortennmetrommSF1SF1S_{F_1}F1F1F_1 Considere el problema de determinar, dado , otra Fórmula CNF F 2 con el mismo conjunto de variables que F 1 , con S F 2 = S F 1 (el mismo espacio de...
¿Hay algún algoritmo para la resolución SAT que no esté basado en DPLL? ¿O todos los algoritmos utilizados por los solucionadores SAT están basados en
El problema de la satisfacción es, por supuesto, un problema fundamental en la CS teórica. Estaba jugando con una versión del problema con infinitas variables. \newcommand{\sat}{\mathrm{sat}} \newcommand{\unsat}{\mathrm{unsat}} Configuración básica. Sea un conjunto de variables no vacío y...
Version corta. La prueba original de que # 2-SAT es # P- completo muestra, de hecho, que esas instancias de # 2-SAT son monótonas (no implican negaciones de ninguna variable) y bipartitas (el gráfico formado por las cláusulas sobre el variables es un gráfico bipartito) son #P -duro. Por lo tanto,...
Dado , ¿cuántos DNF con variables y cláusulas son tautología? (¿o cuántos CNF son insatisfactorios?)k n m km , n , kmetro,norte,km, n,
En el pasado, implementé modelos de coordinación utilizando SAT y satisfacción de restricciones regulares como el caballo de batalla principal en sus motores. Continuando en esta línea de trabajo, me gustaría hacer que los modelos sean más interactivos, y la mejor manera que veo de hacerlo es abrir...
Es bien sabido que las fórmulas aleatorias -CNF sobre n variables con c n cláusulas son insatisfactorias (es decir, son contradicciones) con alta probabilidad, para una constante c suficientemente grande . Por lo tanto, las fórmulas aleatorias de k -CNF (para c lo suficientemente grande)...
Esta pregunta probablemente esté en el límite entre el tema y fuera del tema, sin embargo, he visto preguntas similares aquí, por lo tanto, lo haré. Estoy implementando un solucionador Unique -SAT, cuya entrada es una fórmula -CNF que tiene como máximo asignación satisfactoria. Para probar su...