可满足性模块理论(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)
包括逻辑符号和非逻辑符号。
- Logical Symbols
- Parentheses: (, )
- Quantifier: (forall)(for all), (exists)(there exists)
- Boolean Connectives: (lnot)(not), (land)(and), (lor)(or)
- Constant formulas: true, false
- Equality: =
- 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是否是一个人"。
包括术语(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)是一个赋值方法,给( heta(ar{x}))的每个变量赋值一个M的元素.
(M models_
ho heta(ar{x}))表示(M)和(phi)满足(satisfy)( heta(ar{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 ext{, atomic formulas} \
f ::= lnot f_1 | f_1 land f_2 | f_1 lor f_2 \
where \
a ext{: a column vector of integer constants} \
c ext{: an integer constants} \
x ext{: a column vector of integer variables} \
a^T ext{: a row vector} \
sim ext{: an operator from } {=,
e, <, le, >, ge} \
]
解决方案(solution)的数学表达
一个_解决方案_是一个使得公式(phi)为true的变量赋值w。
(Sol(phi))为公式(phi)所有的解决方案。
注：(phi)应该就是皮尔斯伯格算术定义的公式。
下面是解决方案(Sol(phi))的递归定义：
[if phi ext{ is atomic, then } Sol(phi) = { w in mathbb{Z^n} | a^T cdot w sim c } \
if phi equiv lnot phi_1 ext{, then } Sol(phi) = mathbb{Z}^n - Sol(phi1_1) \
if phi equiv phi_1 land phi_2 ext{, then } Sol(phi) = Sol(phi1_1) cap Sol(phi1_2) \
if phi equiv phi_1 lor phi_2 ext{, then } Sol(phi) = Sol(phi1_1) cup Sol(phi1_2) \
where \
mathbb{Z} ext{: the set of integers} \
w ext{: n-vector of integers} \
mathbb{Z^n} ext{: n integers} \
]
({ a | b })为满足(b)条件下的(a)。
自动化的思路
- 确定性有限状态自动机DFA(deterministic finite-state automaton)
(A_{phi})
- 一个解决方案w的数学表达
[w =
egin{Bmatrix}
w_1 \
cdots \
w_n
end{Bmatrix} \
=
egin{Bmatrix}
b_{10} & cdots & b_{1m} \
cdots & cdots & cdots \
b_{n0} & cdots & b_{nm} \
end{Bmatrix} ext{, binary matrix} \
=
egin{Bmatrix}
b_{10} cdots b_{1m} \
cdots \
b_{n0} cdots b_{nm} \
end{Bmatrix} ext{, a vector binary strings} \
=
egin{Bmatrix}
b_{0} & cdots & b_{m} \
end{Bmatrix} ext{, a vector of languages} \
where \
w_x = egin{Bmatrix}
b_{x0} & cdots & b_{xi} \
end{Bmatrix} ext{, 2's complement form, } b_{x0} ext{: sign bit} \
b_{xy} in mathbb{B} \
mathbb{B} = {0, 1 } \
b_x =
egin{Bmatrix}
b_{1x} \
cdots \
b_{nx} \
end{Bmatrix} , b_x ext{ is denoted as a letter}\
]
-
2补数(2's complement)
一种使用2进制表示有符号数的方法。
第一位为符号位，
如果是0，则记做0;
如果为1，则记做(-2^{n-1} ext{, 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} } ext{ is the set of states, } mathbb{Z} ext{ is the set of integers and } s_{initial}
otin mathbb{Z} \
s_{initial} ext{ is the start state} \
mathbb{B}^n ext{ is the alphabet, which is the set of n-bit vectors, } mathbb{B} = {0, 1} \
ext{The transition function } delta : S imes mathbb{B}^n o S ext{ 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} ext{ is a non-initial state} \
S_{acc} ext{: the set of accepting states}:
S_{acc} = { l in mathbb{Z} | l sim c } cup
egin{cases}
{ s_{initial} } & if a^T cdot 0 sim c \
emptyset & otherwise
end{cases}
]
[l_{initial} = -a^T cdot b_0 ext{, since } b_0 ext{ are sign bits} \
l_{x+1} = a^T cdot
egin{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
Vert_{-} = sum_{{i | a_i < 0}} vert a_i vert \
lVert a^T
Vert_{+} = sum_{{i | a_i > 0}} vert a_i vert
]
推论：
[-a^T cdot b = lVert a^T
Vert_{-} - lVert a^T
Vert_{+} leq lVert a^T
Vert_{-} \
a^T cdot b = lVert a^T
Vert_{+} - lVert a^T
Vert_{-} leq lVert a^T
Vert_{+}
]
引理1：给定一个原子的皮尔斯伯格算术公式(a^T cdot x sim c), a对应的自动机(A_f)，a当前这个自动机的状态(l in mathbb{Z})，有下面断言：
- 如果(l > lVert a^T
Vert_{-}), 则下一个状态(l')，有(l' > l)。
- 如果(l < lVert a^T
Vert_{+}), 则下一个状态(l')，有(l' < l)。
根据引理，自动机的状态的可能性为：
[S = [min(-lVert a^T
Vert_{+}, c), max(lVert a^T
Vert_{-}, 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
Vert_{+}, c), max(lVert a^T
Vert_{-}, c)] cup { s_{initial}, s_{-infty}, s_{+infty} } \
s_{initial}
otin mathbb{Z} \
s_{initial} ext{ is the start state} \
mathbb{B}^n ext{ is the alphabet, which is the set of n-bit vectors, } mathbb{B} = {0, 1} \
ext{The transition function } delta : S imes mathbb{B}^n o S ext{ 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) =
egin{cases}
s_{+infty} & if 2l + a^T cdot b > max(lVert a^T
Vert_{-}, c) \
s_{-infty} & if 2l + a^T cdot b > max(-lVert a^T
Vert_{+}, c) \
2l + a^T cdot b & otherwise \
end{cases} \
S_{acc} ext{: the set of accepting states}: \
S_{acc} = { l in mathbb{Z} | l sim c } \
quad cup \
egin{cases}
{ s_{initial} } & if a^T cdot 0 sim c \
s_{+infty} & if sim in { >, geq,
eq } \
s_{-infty} & if sim in { <, leq,
eq } \
emptyset & otherwise
end{cases}
]
References