將驗證算法轉換爲SAT問題的編譯器

Question

SAT是NP完全的證明是一種建設性證明，所以應該可以將其作爲程序來實現。有沒有人做過這個？

我正在尋找一個程序（一個編譯器），它將一個程序（它返回true或false）作爲輸入並輸出一個SAT公式。例如，編譯器可以將以下程序（以pythonic語法顯示，但任何語言都適合我）作爲輸入，並輸出SAT公式。將SAT公式提供給SAT求解器將給出參數「證書」的解決方案。在這種情況下，解決方案會是[假，真，真，假，假]，表明{-3，-2,5}是一個解決方案。

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 

顯然輸出SAT式將有其它輔助變量，所以編譯器將不得不以指示哪些變量對應於證書。

這樣的編譯器是否已經存在？他們中的任何一個是開源的嗎？

Answer 1

你應該看看SMT解算器，因爲它們是你想要的最接近的東西。你並沒有使用SMT（無循環）編寫Turing完整語言，但你可以使用整數和實值變量，布爾邏輯，函數，基本算術和數組。