3cnf - Class Scheduling to Boolean satisfiability
3cnf sat (1)
Voy a tratar de formalizar primero el problema y luego intentar reducirlo al SAT.
Defina el problema de programación de clases como:
Input = { S1,S2,....,Sn | Si = {(x_i1, y_i1), (x_i2, y_i2) , ... , (x_ik, y_ik) | 0 <= x_ij < y_ij <= M } }
Informalmente: la entrada es un conjunto de clases, cada clase es un conjunto de intervalos (abiertos) en la forma (x, y)
(M es una constante que describe el "final de la semana")
Salida: verdadero si y solo si existe algún conjunto:
R = { (x_1j1, y_1j1) , ..., (x_njn, y_njn) | for each a,b: (x_aja,y_aja) INTERSECTION (x_bjb,y_bjb) = {} }
Informalmente: es verdadero si y solo si hay alguna asignación de intervalos de modo que la intersección entre cada par de intervalos esté vacía.
Reducción al SAT:
Defina una variable booleana para cada intervalo, V_ij
Basado en él, defina la fórmula:
F1 = (V_11 OR V_12 OR ... OR V_1(k_1)) AND .... AND (V_n1 OR V_n2 OR ... OR V_n(k_n))
Informalmente, F1 se satisface si y solo si al menos uno de los intervalos de cada clase está "satisfecho"
Definir Smaller(x,y) = true si y solo if x <= y 1
Lo usaremos para asegurarnos de que los intervalos no se superpongan.
Tenga en cuenta que si queremos asegurarnos de que (x1, y1) y (x2, y2) no se superpongan, necesitamos:
x1 <= y1 <= x2 <= y2 OR x2 <= y2 <= x1 <= y1
Como la entrada garantiza x1<=y1, x2<=y2 , se reduce a:
y1<= x2 OR y2 <= x1
Y usando nuestras cláusulas más pequeñas y booleanas:
Smaller(y1,x2) OR Smaller(y2,x1)
Ahora, vamos a definir nuevas cláusulas para manejarlo:
Para cada par de clases a, b e intervalos c, d en ellas (c en a, d en b)
G_{c,d} = (Not(V_ac) OR Not(V_bd) OR Smaller(y_ac,x_bd) OR Smaller(y_bd,x_ac))
De manera informal, si uno de los intervalos byd no se usa, la cláusula queda satisfecha y terminamos. De lo contrario, se utilizan ambos, y debemos asegurarnos de que no haya superposición entre los dos intervalos.
Esto garantiza que si ambos c, d son "elegidos", no se superponen, y esto es cierto para cada par de intervalos.
Ahora, forma nuestra fórmula final:
F = F1 AND {G_{c,d} | for each c,d}
Esta fórmula nos asegura:
- Para cada clase, se elige al menos un intervalo
- Para cada dos intervalos c, d - si se eligen c y d, no se superponen.
Nota pequeña: esta fórmula permite elegir más de 1 intervalo de cada clase, pero si hay una solución con algunos t> 1 intervalos, puede eliminar fácilmente t-1 de ellos sin cambiar la corrección de la solución.
Al final, los intervalos elegidos son las variables booleanas V_ij que definimos.
Ejemplo:
Alebgra = {(1,3),(3,5),(4,6)} Calculus = {(1,4),(2,5)}
Definir F:
F1 = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2)
Definir G''s:
G{A1,C1} = Not(V1,1) OR Not(V2,1) OR 4 <= 1 OR 3 <= 1 //clause for A(1,3) C(1,4)
= Not(V1,1) OR Not(V2,1) OR false =
= Not(V1,1) OR Not(V2,1)
G{A1,C2} = Not(V1,1) OR Not(V2,2) OR 3 <= 2 OR 5 <= 1 // clause for A(1,3) C(2,5)
= Not(V1,1) OR Not(V2,2) OR false =
= Not(V1,1) OR Not(V2,2)
G{A2,C1} = Not(V1,2) OR Not(V2,1) OR 5 <= 1 OR 4 <= 3 //clause for A(3,5) C(1,4)
= Not(V1,2) OR Not(V2,1) OR false =
= Not(V1,2) OR Not(V2,1)
G{A2,C2} = Not(V1,2) OR Not(V2,2) OR 5 <= 2 OR 5 <= 3 // clause for A(3,5) C(2,5)
= Not(V1,2) OR Not(V2,2) OR false =
= Not(V1,2) OR Not(V2,2)
G{A3,C1} = Not(V1,3) OR Not(V2,1) OR 4 <= 4 OR 6 <= 1 //clause for A(4,6) C(1,4)
= Not(V1,3) OR Not(V2,1) OR true=
= true
G{A3,C2} = Not(V1,3) OR Not(V2,2) OR 6 <= 2 OR 5 <= 4 // clause for A(4,6) C(2,5)
= Not(V1,3) OR Not(V2,2) OR false =
= Not(V1,3) OR Not(V2,2)
Ahora podemos mostrar nuestra fórmula final:
F = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2)
AND Not(V1,1) OR Not(V2,1) AND Not(V1,1) OR Not(V2,2)
AND Not(V1,2) OR Not(V2,1) AND Not(V1,2) OR Not(V2,2)
AND true AND Not(V1,3) OR Not(V2,2)
Lo anterior está satisfecho solo cuando:
V1,1 = false
V1,2 = false
V1,3 = true
V2,1 = true
V2,2 = false
Y eso representa el horario: Algebra = (4,6); Cálculo = (1,4), según lo deseado.
(1) se puede calcular como una constante a la fórmula con bastante facilidad, hay un número polinomial de tales constantes.
Tengo un problema teórico / práctico y no tengo ni idea por el momento de cómo administrar, Aquí está:
Creo un solucionador de SAT capaz de encontrar un modelo cuando existe uno y probar la contradicción cuando no es el caso de los problemas de CNF en C usando algoritmos de genética.
Un problema SAT se ve básicamente como este tipo de problema: Mi objetivo es usar este solucionador para encontrar soluciones en muchos problemas diferentes de NP-complete . Básicamente, traduzco diferentes problemas en SAT, resuelvo SAT con mi solucionador y luego transformo la solución en una solución aceptable para el problema original.
Ya tengo éxito para el N * N Sudoku y también los problemas de N-queens, pero este es mi nuevo objetivo: reducir el problema de programación de clases al SAT pero no tengo idea de cómo formalizar un problema de programación de clases para transformarlo fácilmente en SAT después.
El objetivo es, obviamente, en pocos meses, generar una imagen de un horario como este:
Encontré este código fuente que puede resolver la programación de clases pero desafortunadamente sin ninguna reducción al SAT: /
También encontré algunos artículos sobre Planificación en general ( http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf, por ejemplo).
Pero el lenguaje de definición de dominio de planificación utilizado en este artículo me parece demasiado general como para representar un problema de programación de clase. : /
¿Alguien tiene una idea sobre cómo formalizar eficientemente una programación de clases para reducirla al SAT y después, transformar la solución SAT (si existe ^^) en un horario de clase?
Estoy básicamente abierto a cualquier sugerencia, por ahora no tengo idea de cómo representar, cómo reducir el problema, cómo transformar la solución SAT en un horario ...
Pregunta de seguimiento : Programación de clase a satisfacibilidad booleana [Reducción de tiempo polinómico] parte 2