Compiladores que traducen algoritmos de verificación en problemas SAT

Question

La prueba de que SAT es NP-completa es una prueba constructiva, por lo que debería ser posible implementarla como un programa. ¿Alguien ha hecho esto?

Estoy buscando un programa (un compilador), que toma como entrada un programa (que devuelve verdadero o falso) y emite una fórmula SAT.

Por lo tanto, por ejemplo, el compilador podría tomar el siguiente programa (mostrar en sintaxis pitonica, pero cualquier lenguaje está bien para mí), como entrada, y generar una fórmula SAT. Al alimentar la fórmula SAT con un solucionador de SAT se daría una solución al parámetro "certificado". En este caso, la solución sería [False, True, True, True, False], lo que indica que {-3, -2, 5} es una solución.

def verify(certificate): 
    problem = [-7, -3, -2, 5, 8] 
    sum = 0 
    for (x, b) in zip(problem, certificate): 
    if b: 
     sum += x 
    return sum == 0 

Obviamente la salida fórmula SAT tendría otras variables auxiliares, por lo que el compilador tendría que indicar que las variables se corresponden con el certificado.

¿Ya existen estos compiladores? ¿Alguno de ellos es de código abierto?

Answer 1

Debe considerar los solucionadores de SMT, ya que son lo más parecido a lo que desea. No está escribiendo en un lenguaje completo de Turing con SMT (sin bucles), pero puede trabajar con variables enteras y con valores reales, lógica booleana, funciones, aritmética básica y matrices.