Compilatori che traducono algoritmi di verifica in problemi SAT

Question

La prova che SAT è NP-completo è una prova costruttiva, quindi dovrebbe essere possibile implementarlo come programma. Qualcuno ha fatto questo?

Sto cercando un programma (un compilatore), che accetta come input un programma (che restituisce vero o falso) e restituisce una formula SAT.

Così, ad esempio, il compilatore può prendere il seguente programma (mostrato in sintassi pitonica, ma qualsiasi lingua va bene con me), come input, ed emettere una formula SAT. Alimentare la formula SAT in un solutore SAT darebbe una soluzione al parametro "certificato". In questo caso, la soluzione sarebbe [Falso, Vero, Vero, Vero, Falso], a indicare che {-3, -2, 5} è una soluzione.

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 

Ovviamente l'uscita SAT formula avrebbe altre variabili ausiliarie, quindi il compilatore dovrebbe indicare quali variabili corrispondono al certificato.

Esistono già tali compilatori? Qualcuno di loro è open source?

Answer 1

Si dovrebbe esaminare i risolutori SMT poiché sono la cosa più vicina a ciò che si desidera. Non stai scrivendo in un linguaggio completo di Turing con SMT (nessun loop), ma puoi lavorare con valori interi e variabili reali, logica booleana, funzioni, aritmetica di base e array.