如果,我们只给出一个数学问题的(比如一道数独题)约束条件,是否有程序可以自动求出一个解? 可满足性模理论(SMT - Satisfiability Modulo Theories)已经可以实现这个需求。
因此,最近想搞明白z3的实现原理。源代码没有读两句,还是找了本教材来看。 Vijay Ganesh (PhD. Thesis 2007), Decision Procedures for Bit-Vectors, Arrays and Integers 现在的任务是:
数学上,这个问题属于逻辑的范畴。
一阶逻辑: 逻辑函数的参数可以是变量,但是不能是函数。 书中把一阶逻辑看成一种数学语言。 这种语言的语法(Syntax)由字母系统(Alphabet)和构造法则(formation rules)组成。
包括逻辑符号和非逻辑符号。
包括术语(terms)和公式(formulas)。
这里说的理论是一个需要求解的推测.
Theory -> signature(\Sigma) -> dom(m)
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\} \\
一个_解决方案_是一个使得公式\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。
自动机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 的可能性。基本上存在于所有的整数\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_{+}
有限自动机\(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}