SMT解算器的限制

Question

傳統上，大多數使用計算邏輯的工作是命題性的，在這種情況下，您使用了SAT（布爾可滿足性）求解器或一階，在這種情況下，您使用了一階定理證明器。

近年來，SMT（可滿足性模數理論）求解器取得了很大進展，基本上用算術等理論增強了命題邏輯。 SRI International的John Rushby甚至稱他們爲顛覆性技術。

什麼是可以在一階邏輯中處理但仍不能由SMT處理的問題的最重要的實際例子？最特別的是，SMT在軟件驗證領域無法解決的問題是什麼？

Answer 1

SMT解算器沒有SAT解算器更強大。對於SAT中的相同問題，他們仍然會以指數時間運行或不完整。 SMT的優勢在於SMT中很多顯而易見的事情可能需要很長時間才能讓等效的座標解算器重新發現。因此，以軟件驗證爲例，如果您使用QF BV（位矢量的無量化器理論）SMT解算器，則SMT求解器將知道（a + b = b + a）一個字級別，而需要一個SAT求解器很長時間才能證明使用各個布爾值。因此，對於軟件驗證，您可以輕鬆地在軟件驗證中出現問題，這對於任何SMT或SAT解算器來說都很難。

首先，循環必須在QF BV中展開，這意味着實際上您必須限制解算器檢查的內容。如果量詞被允許，它將成爲PSPACE完成問題，而不僅僅是NP完全問題。

其次，一般認爲難度較大的問題很容易在QF BV中編碼。例如，你可以寫出如下的程序：

void run(int64_t a,int64_t b) 
{ 
    a * b == <some large semiprime>; 

    assert (false); 
} 

當然現在的SMT求解器很容易證明，斷言（假）會發生，但它必須提供一個反例，它會給你的輸入a,b。如果您將<some large number>設置爲RSA semiprime，那麼您只需反轉乘法...否則稱爲整數因子分解！因此，對於任何SMT解算器來說，這可能是困難的，並且證明軟件驗證通常是一個難題（除非P = NP，或者至少整數分解變得容易）。這樣的SMT解決方案只是通過更易於編寫和易於理解的語言進行修補而成爲SAT求解器的一部分。

解決更先進理論的SMT求解器必然不完整，或者甚至比SAT求解器慢，因爲他們試圖解決更難的問題。

參見：

• 有趣的是，Beaver SMT solver轉換QF BV至CNF和可以使用SAT解算器作爲後端。
• Klee它可以將程序編譯爲LLVM IR（中間表示），並檢查錯誤，並找到反例的斷言等。如果它發現一個錯誤，它可以給出一個反例的正確性（它會給你輸入，將重現錯誤）。