SAT&SMT

前言

本文性質：個人學習筆記

SAT(SATISFIABILITY/布爾可滿足性問題)，SMT(Satisfiability Modulo Theories/可滿足性模理論)

根據哥德爾不完備定理/停機問題/萊斯定理，我們可以知道在有限時間内是無法得到精确的分析結果。我們可以嘗試使用抽象和搜尋來得到近似或者精确的結果。這其中的關鍵技術就是限制求解。

限制求解

給定一組限制，求：

• 這組限制是否可滿足
• （可選）如果可滿足，給出一組指派
• （可選）如果不可滿足，給出一個較小的沖突集

總的來說是不可判定的問題，但存在很多可判定的子問題，如：

• a > 10
• b < 100 || b > 200

• a+b=30

  可滿足：a=15, b=15

SAT

SAT問題就是子句集上的限制求解問題，給定一組子句，尋找一個布爾指派，使得所有子句為真。

子句clause：文字的析取（disjunction） 如𝑥 ∨ ¬y

布爾指派：從變量到布爾值上的映射

SAT問題通常是通過合取範式定義的，任何命題邏輯公式可以表達為合取範式，即SAT問題可以求解任何命題邏輯公式。

SAT的基本求解方法：

• 窮舉法
• 基于指派推導和沖突檢測的SAT求解——DPLL
• 沖突導向的子句學習CDCL（Conflict-Driven Clause Learning）

SMT

SAT問題回答某個命題邏輯公式的可滿足性，如：𝐴 ∧ 𝐵 ∨ ¬𝐶。但實際中的公式卻往往是這樣的：𝑎 + 𝑏 < 𝑐 ∧ 𝑓 𝑏 > 𝑐 ∨ 𝑐 > 0

如何判斷這樣公式的可滿足性？

從邏輯學角度來看，𝑎 + 𝑏 < 𝑐或者𝑓 (𝑏) > 𝑐都是邏輯系統中不包含的符号，需要知道他們的意思。

理論(Theory)：

• 理論用于對這類符号賦予含義

• 理論包含一組公理和這組公理能推導出的結論

可滿足性模理論Satisfiability Modulo Theories：給定一組理論，根據給定背景邏輯，求在該組理論解釋下公式的可滿足性

• SAT solver：解著名的NP完全問題
• Linear solvers：求線性方程組
• Array solvers: 求解包含數組的限制
• String solver：求解字元串限制

SMT：綜合以上各類限制求解工具。

參考

本文僅為個人了解，如有錯誤，歡迎指正。參考資料如下：

維基百科關于SMT的解釋

北大熊英飛老師軟體分析課件——SAT

北大熊英飛老師軟體分析課件——SMT

想更全面深入的了解可以閱讀書籍《Decision Procedures: An Algorithmic Point of View》或《Handbook of satisfiality》。先留個坑在這裡，待我讀完其中一本以後，再來給本文做點修改和補充。