Doğrulama algoritmalarını SAT sorunlarına çeviren derleyiciler

Question

SAT'ın NP-tamamlandığının kanıtı yapıcı bir kanıttır, bu yüzden bunu bir program olarak uygulamak mümkün olmalıdır. Bunu yapan var mı?

Bir program (girdi doğru ya da yanlış) giriş olarak alan ve SAT formülünü gönderen bir program (derleyici) arıyorum. Örneğin, derleyici aşağıdaki gibi bir program alabilir (pythonic sözdiziminde gösterme, ancak herhangi bir dilde benimle iyidir), girdi olarak ve bir SAT formülünü verebilir. SAT formülünü SAT çözücüye beslemek, "sertifika" parametresine bir çözüm getirecektir. Bu durumda çözüm, {-3, -2, 5} 'in bir çözüm olduğunu belirten [Yanlış, Doğru, Doğru, Doğru, Yanlış] olur. derleyici belgesi tekabül eden değişkenleri belirtmek gerekir, böylece

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 

Açıkçası çıkış SAT formülü, diğer yardımcı değişkenlere sahiptir.

Bu tür derleyiciler zaten var mı? Açık kaynaklardan biri var mı?

Answer 1

SMT çözücülere bakmalısın, çünkü istediklerinize en yakın şey onlar. SMT'lerle (döngü yok) bir Turing tam dilinde yazmıyorsunuz, ancak tamsayı ve gerçek değerli değişkenler, Boole mantığı, fonksiyonlar, temel aritmetik ve dizilerle çalışabilirsiniz.