本文是个长期的工作,是对 Dennis Yurichev的文章《SAT/SMT by example》的翻译。文本总长460页,二十余章。在翻译的过程中,我会假如我的理解和一些具体的算法。

SAT / SMT

SAT / SMT 求解器都是求解等式系统(systems of equations)的,不同的是,SMT接受不同格式的等式系统,而SAT对输入格式是有要求的,必须是CNF范式的布尔等式(boolean equations)。

2. 基本知识

2.1 one-hot encoding

在本文中,我们将经常用到 one-hot encoding这个词,来表示以下的

decimal one-hot
0 0000 0001
1 0000 0010
2 0000 0100
3 0000 1000
4 0001 0000
5 0010 0000
6 0100 0000
7 1000 0000

或者

decimal one-hot
0 1000 0000
1 0100 0000
2 0010 0000
3 0001 0000
4 0000 1000
5 0000 0100
6 0000 0010
7 0000 0001

它也有几个优点和缺点,具体可查阅:https://en.wikipedia.org/wiki/One-hot。

2.2 SMT 求解器

2.2.1 简单的等式

对于以下,
3x+2yz=13x + 2y - z = 1
$ 3x - 2y + 4z = -2 -x + ½ y = z = 0 $

我们用Z3求解器求解以下:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
from z3 import *

x = Real('x')
y = Real('y')
z = Real('z')
s = Solver()
s.add(3*x + 2*y - z == 1)
s.add(2*x - 2*y + 4*z == -2)
s.add(-x + 0.5*y - z == 0)
print(s.check())
print(s.model())
==========
output:
sat
[y = 3/2, x = 4]

求解器返回“sat” 并且给出具体的取值实例:[z = -2, y = -2, x = 1]。如果我们队等式稍加改动,求解器若求不出,会返回“unsat”。

在以上的例子中,我们用了实数类型Real,有些例子中,用整型 Int 也是可以的。并且使用的Python的接口。事实上,对于大多数的SMT求解器来说,SMT-LIB 是用来描述等式的标准语言,我们对上述的例子重新改写:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
ex1.smt

(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (=(-(+(* 3 x) (* 2 y)) z) 1))
(assert (=(+(-(* 2 x) (* 2 y)) (* 4 z)) -2))
(assert (=(-(+ (- 0 x) (* 0.5 y)) z) 0))
(check-sat)
(get-model)
----------------------
~ z3 -smt2 ex1.smt //执行命令

output:
sat
(model
(define-fun z () Real
(- 2.0))
(define-fun y () Real
(- 2.0))
(define-fun x () Real
1.0)
)

Z3不仅提供了Python接口(参考手册),也有Java,ML,C++,.net 接口

2.2.2 简单的等式2

Fig1

这个题看起来是智力测试题,利用Z3,同样可以得到问题的解。

1
2
3
4
5
6
7
8
9
10
11
12
from z3 import *

circle, square, triangle = Ints('circle square triangle')
s = Solver()
s.add(circle + circle == 10)
s.add(circle * square + square == 12)
s.add(circle * square - triangle * circle == circle)
print(s.check())
print(s.model())
-------------------
sat
[triangle = 1, square = 2, circle = 5]

2.2.3 链接SAT 和 SMT

SMT可以看走是SAT的前端,只需要将SMT表达式转换成CNF格式,就可以作为SAT的输入。一些SMT求解器用外部的SAT求解器,比如STP就用MiniSAT,一些SMT求解器内置自己的SAT求解器,Z3也具有自己的SAT求解器。

2.2.3 SMT求解器

SMT creators
Yice by Bruno Dutertre et al.
Boolector by Aina Niemetz, Mathias Preiner and Armin Biere.
Alt-Ergo used in Frama-C
MathSAT by Alberto Griggio, Alessandro Cimatti and Roberto Sebastiani
veri by David Déharbe, Pascal Fontaine, Haniel Barbosa. Lacks bitvectors.
[dReal](http://dreal.cs.cmu.edu, https://github.com/dreal) An SMT Solver for Nonlinear Theories of the Reals”

-w300

2.3 SAT 求解器

SAT 是 “Boolean satisfiability problem”的缩写。SAT问题是给定布尔表达式,寻找使得表达式值为真的解。

3-SAT 是目前公认的第一个被证明的NPC问题。由University of Toronto的Stephen A. Cook教授,在1971年发表的论文“The Complexity of Theorem-Proving Procedures”当中证明的。

2.3.1 CNF范式

一个SAT的实例是一个有n个布尔变量的布尔表达式。通常情况下,我们假设这些变量通过Conjuctive Normal Form (CNF,中文好奇葩叫做“合取范式”)的形式给出。比如以下公式,是一个合法的SAT输入公式(CNF范式):

(x1¬x2)(x2x3)(¬x1x2¬x3)(x_1 \lor \neg x_2) \land (x_2 \lor x_3) \land ( \neg x_1 \lor x_2 \lor \neg x_3)

其中,一个conjuncts被称为一个clause(比如(x1¬x2)(x_1 \lor \neg x_2), 一个clause中,一个disjunct称为literal,比如(x1¬x2)(x_1 \lor \neg x_2)中的x1x_1¬x2\neg x_2

CNF:简单的来说就是,clause内部的literals之间关系全部都是OR,clauses之间的关系全部都是AND。

2.3.2 SAT求解器

STA creators
MiniSat
PicoSat d by Armin Biere. Plingeling supports multithreading
CryptoMiniSat by Mate Soos for cryptographical problems exploration XOR,Python
MaxSAT
Open-WBO by Ruben Martins, Vasco Manquinho, Inês Lynce.