可滿足性模塊理論(SMT)基礎 - 01 - 自動機和斯皮爾伯格算術

前言

如果，我們只給出一個數學問題的（比如一道數獨題）約束條件，是否有程序可以自動求出一個解？
可滿足性模理論(SMT - Satisfiability Modulo Theories)已經可以實現這個需求。

因此，最近想搞明白z3的實現原理。源代碼沒有讀兩句，還是找了本教材來看。
Vijay Ganesh (PhD. Thesis 2007), Decision Procedures for Bit-Vectors, Arrays and Integers
現在的任務是：

• 看懂這本書，搞清楚求解邏輯。
• 再搞清楚，如何使用SMT來求解各種問題？

可滿足性模理論(SMT - Satisfiability Modulo Theories)

基本概念

數學上，這個問題屬於邏輯的范疇。

一階邏輯(First-Order Logic)及其語法

一階邏輯: 邏輯函數的參數可以是變量，但是不能是函數。
書中把一階邏輯看成一種數學語言。
這種語言的語法(Syntax)由字母系統(Alphabet)和構造法則(formation rules)組成。

字母系統(Alphabet)

包括邏輯符號和非邏輯符號。

1. Logical Symbols
   • Parentheses: (, )
   • Quantifier: \(\forall\)(for all), \(\exists\)(there exists)
   • Boolean Connectives: \(\lnot\)(not), \(\land\)(and), \(\lor\)(or)
   • Constant formulas: true, false
   • Equality: =
2. Non-logical Symbols
   • Variables: usually represented by letters x, y, z...
   • Function Symbols: 函數符號通常使用小寫字母來表示，f, g, h,...
     函數符號的返回類型一般不是Boolean類型。比如：f(x)可以表示為"x的父親"。
   • Relation Symbols(關系符號) or predicate symbols(謂詞符號): Each relation symbol also has an associated arity
     謂詞符號一般使用大寫字母來表示，P, Q, R, ...
     謂詞符號代表一個返回值為Boolean類型的函數。比如：P(x)可以表示"x是否是一個人"。

構造法則(Formation Rules)

包括術語(terms)和公式(formulas)。

• 術語(terms)
  包括變量(variables)和函數(functions)。
• 公式(formulas)
  包括：謂詞符號，等式(equality)，邏輯運算符號(\(\lnot, \land, \lor\)), 修飾符(quantifiers)

其它概念

• 原子公式(atomic formula)
  由謂詞符號和等式組成的公式。原子公式不包含邏輯運算符號和修飾符。
• 文字(literals)
  包括：原子公式和其否定。
• 無修飾公式(quantifier-free formulas)
  由謂詞符號、等式和邏輯運算符號組成的公式。比如： \(p(x)\)。
• 量化公式(quantified formulas)
  帶修飾符號的公式。比如： \(\forall x p(x)\)。
• 自由變量(free variable)
  比如： \(p(x)\)中的\(x\)。
• 界限變量(bound variables)
  量化公式中被限定的變化。比如： \(\forall x p(x)\)中的\(x\)。

一階邏輯的理論和模型

這里說的理論是一個需要求解的推測.

• 理論(theories)
  一個理論是一套一階命題(sentence),這些命題,在一套公理(axioms)的基礎上,是可以被推理出來的.
  我們的目的是求解出命題中變量的值,以滿足所有的命題.

• 模型(model)
  模式是一個滿足一個給定理論(所有命題)的一階結構,表示為\(dom(M)\).
  \(\phi\)是一個賦值方法,給\(\theta(\bar{x})\)的每個變量賦值一個M的元素.
  \(M \models_\rho \theta(\bar{x})\)表示\(M\)和\(\phi\)滿足(satisfy)\(\theta(\bar{x})\).

Theory -> signature(\(\Sigma\)) -> dom(m)

• 穩固性(soundness)
  論證的每一步在數學上都是正確的。如果返回值為"不可滿足(unsatisfiable)"，則確實是不可滿足。

• 完備性(completeness)
  如果返回值為“可滿足”，則確實為可滿足。並可以生成用於得出結論的所有事實。

• 在線(online)
  決策程序以一種遞增的方式接受處理新的輸入，而不需要重新處理之前已經處理過的輸入。

• 證明生成(proof-producing)
  指決策程序可以對處理過程產生一個數學證明。

• SAT(boolean satisfiability problem) - 布爾可滿足性問題
  給定一個邏輯公式，判斷是否存在解。

現有的各種方法

皮爾斯伯格算術(Presburger arithmetic)

皮爾斯伯格算術公式的定義

\[f \equiv a^T \cdot x \sim c \text{, atomic formulas} \\ f ::= \lnot f_1 | f_1 \land f_2 | f_1 \lor f_2 \\ where \\ a \text{: a column vector of integer constants} \\ c \text{: an integer constants} \\ x \text{: a column vector of integer variables} \\ a^T \text{: a row vector} \\ \sim \text{: an operator from } \{=, \ne, <, \le, >, \ge\} \\ \]

解決方案(solution)的數學表達

一個_解決方案_是一個使得公式\(\phi\)為true的變量賦值w。
\(Sol(\phi)\)為公式\(\phi\)所有的解決方案。

注：\(\phi\)應該就是皮爾斯伯格算術定義的公式。
下面是解決方案\(Sol(\phi)\)的遞歸定義：

\[if \ \phi \text{ is atomic, then } Sol(\phi) = \{ w \in \mathbb{Z^n} | a^T \cdot w \sim c \} \\ if \ \phi \equiv \lnot \phi_1 \text{, then } Sol(\phi) = \mathbb{Z}^n - Sol(\phi1_1) \\ if \ \phi \equiv \phi_1 \land \phi_2 \text{, then } Sol(\phi) = Sol(\phi1_1) \cap Sol(\phi1_2) \\ if \ \phi \equiv \phi_1 \lor \phi_2 \text{, then } Sol(\phi) = Sol(\phi1_1) \cup Sol(\phi1_2) \\ where \\ \mathbb{Z} \text{: the set of integers} \\ w \text{: n-vector of integers} \\ \mathbb{Z^n} \text{: n integers} \\ \]

\(\{ a | b \}\)為滿足\(b\)條件下的\(a\)。

自動化的思路

• 確定性有限狀態自動機DFA(deterministic finite-state automaton)
  \(A_{\phi}\)
• 一個解決方案w的數學表達

\[w = \begin{Bmatrix} w_1 \\ \cdots \\ w_n \end{Bmatrix} \\ = \begin{Bmatrix} b_{10} & \cdots & b_{1m} \\ \cdots & \cdots & \cdots \\ b_{n0} & \cdots & b_{nm} \\ \end{Bmatrix} \text{, binary matrix} \\ = \begin{Bmatrix} b_{10} \cdots b_{1m} \\ \cdots \\ b_{n0} \cdots b_{nm} \\ \end{Bmatrix} \text{, a vector binary strings} \\ = \begin{Bmatrix} b_{0} & \cdots & b_{m} \\ \end{Bmatrix} \text{, a vector of languages} \\ where \\ w_x = \begin{Bmatrix} b_{x0} & \cdots & b_{xi} \\ \end{Bmatrix} \text{, 2's complement form, } b_{x0} \text{: sign bit} \\ b_{xy} \in \mathbb{B} \\ \mathbb{B} = \{0, 1 \} \\ b_x = \begin{Bmatrix} b_{1x} \\ \cdots \\ b_{nx} \\ \end{Bmatrix} , \ b_x \text{ is denoted as a letter}\\ \]

• 2補數(2's complement)
  一種使用2進制表示有符號數的方法。
  第一位為符號位，
  如果是0，則記做0;
  如果為1，則記做\(-2^{n-1} \text{, n is the size of the number}\)。
  例如： 0010為2; 1010為-6。

• 語言\(L_f\)
  是公式f的所有解決方案形成的所有字符串的集合。

自動機的正式描述

自動機\(A_f\)可以理解為一個類的實例，
屬性：
formula
state
方法：
read(),
transition(),
satisfied()
output()
無限自動機\(A_f\)的數學描述：

\[A_f = (S, \mathbb{B}^n, \delta, s_{initial}, S_{acc}) \\ where \\ S = \mathbb{Z} \cup \{ s_{initial} \} \text{ is the set of states, } \mathbb{Z} \text{ is the set of integers and } s_{initial} \notin \mathbb{Z} \\ s_{initial} \text{ is the start state} \\ \mathbb{B}^n \text{ is the alphabet, which is the set of n-bit vectors, } \mathbb{B} = \{0, 1\} \\ \text{The transition function } \delta : S \times \mathbb{B}^n \to S \text{ is defined as follows:} \\ \quad \delta(s_{initial}, b) = -a^T \cdot b \\ \quad \delta(l, b) = 2l + a^T \cdot b \\ \quad where \ l \in \mathbb{Z} \text{ is a non-initial state} \\ S_{acc} \text{: the set of accepting states}: S_{acc} = \{ l \in \mathbb{Z} | l \sim c \} \cup \begin{cases} \{ s_{initial} \} & if \ a^T \cdot 0 \sim c \\ \emptyset & otherwise \end{cases} \]

• 自動機的狀態
  \(l\)是自動機\(A_f\)的狀態。

\[l_{initial} = -a^T \cdot b_0 \text{, since } b_0 \text{ are sign bits} \\ l_{x+1} = a^T \cdot \begin{Bmatrix} b_{10} & \cdots & b_{1x+1} \\ \cdots & \cdots & \cdots \\ b_{n0} & \cdots & b_{nx+1} \\ \end{Bmatrix} \\ \ \ = 2l_x + a^T \cdot b_{x+1} \]

• 自動機的接受條件
  \(l \sim c\)

• 自動機的結果
  當滿足接受條件時，\(b\)的值。

為什么是無限的？

這里說的無限是指狀態\(l\)的可能性。基本上存在於所有的整數\(\mathbb{Z}\)中了。

轉變為有限自動機，需要的過程。

2個定義: 對系數\(a^T = (a_1, \cdots, a_n)\)：

\[\lVert a^T \rVert_{-} = \sum_{\{i | a_i < 0\}} \vert a_i \vert \\ \lVert a^T \rVert_{+} = \sum_{\{i | a_i > 0\}} \vert a_i \vert \]

推論：

\[-a^T \cdot b = \lVert a^T \rVert_{-} - \lVert a^T \rVert_{+} \leq \lVert a^T \rVert_{-} \\ a^T \cdot b = \lVert a^T \rVert_{+} - \lVert a^T \rVert_{-} \leq \lVert a^T \rVert_{+} \]

引理1：給定一個原子的皮爾斯伯格算術公式\(a^T \cdot x \sim c\), a對應的自動機\(A_f\)，a當前這個自動機的狀態\(l \in \mathbb{Z}\)，有下面斷言：

1. 如果\(l > \lVert a^T \rVert_{-}\), 則下一個狀態\(l'\)，有\(l' > l\)。
2. 如果\(l < \lVert a^T \rVert_{+}\), 則下一個狀態\(l'\)，有\(l' < l\)。

根據引理，自動機的狀態的可能性為：

\[S = [\min(-\lVert a^T \rVert_{+}, c), max(\lVert a^T \rVert_{-}, c)] \cup \{ s_{initial}, s_{-\infty}, s_{+\infty} \} \]

這就可以變成有限自動機。

有限自動機的正式描述

有限自動機\(A_f\)的數學描述：

\[A_f = (S, \mathbb{B}^n, \delta, s_{initial}, S_{acc}) \\ where \\ S = [\min(-\lVert a^T \rVert_{+}, c), max(\lVert a^T \rVert_{-}, c)] \cup \{ s_{initial}, s_{-\infty}, s_{+\infty} \} \\ s_{initial} \notin \mathbb{Z} \\ s_{initial} \text{ is the start state} \\ \mathbb{B}^n \text{ is the alphabet, which is the set of n-bit vectors, } \mathbb{B} = \{0, 1\} \\ \text{The transition function } \delta : S \times \mathbb{B}^n \to S \text{ is defined as follows:} \\ \quad \delta(s_{initial}, b) = -a^T \cdot b \\ \quad \delta(s_{+\infty}, b) = s_{+\infty} \\ \quad \delta(s_{-\infty}, b) = s_{-\infty} \\ \quad \delta(l, b) = \begin{cases} s_{+\infty} & if \ 2l + a^T \cdot b > max(\lVert a^T \rVert_{-}, c) \\ s_{-\infty} & if \ 2l + a^T \cdot b > max(-\lVert a^T \rVert_{+}, c) \\ 2l + a^T \cdot b & otherwise \\ \end{cases} \\ S_{acc} \text{: the set of accepting states}: \\ S_{acc} = \{ l \in \mathbb{Z} | l \sim c \} \\ \quad \cup \\ \begin{cases} \{ s_{initial} \} & if \ a^T \cdot 0 \sim c \\ s_{+\infty} & if \ \sim \in \{ >, \geq, \neq \} \\ s_{-\infty} & if \ \sim \in \{ <, \leq, \neq \} \\ \emptyset & otherwise \end{cases} \]

References

• Vijay Ganesh (PhD. Thesis 2007), Decision Procedures for Bit-Vectors, Arrays and Integers
• Satisfiability Modulo Theories
• First-order logic