z3 guide

Z3是微软研究院开发的高性能定理证明程序。Z3有许多应用场合，如:软件/硬件验证和测试，约束求解，混合系统的分析，安全，生物(硅分析)，几何问题。 Z3发行版还包含C、C++、.Net、Java和OCaml 的api。Z3Py的源代码可以在GitHub上的Z3发行版中获得.

导入z3

!pip install "z3-solver"
from z3 import *

从一个简单例子开始

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
'''
[y = 0, x = 7]
'''

在Z3中函数Int('x')创建了一个整数变量x，solve函数求解一个约束系统。上面的例子使用了两个变量x和y以及3个约束.

公式/表达式的化简

x = Int('x')
y = Int('y')
print(simplify(x + y + 2*x + 3))
print(simplify(x < y + x + 2))
print(simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))
'''
3 + 3*x + y
Not(y <= -2)
And(x >= 2, 2*x**2 + y**2 >= 3)
'''

设置显示方法

默认情况下，Z3Py(用于web)使用数学符号显示公式和表达式。通常，∧是逻辑的和，∨是逻辑的或，等等。命令set_option(html_mode=False)使所有公式和表达式以Z3Py表示法显示。这也是Z3发行版附带的Z3Py脱机版本的默认模式

x = Int('x')
y = Int('y')
print(x**2 + y**2 >= 1)
set_option(html_mode=False)
print(x**2 + y**2 >= 1)
'''
x**2 + y**2 >= 1
x**2 + y**2 >= 1
'''
set_option(html_mode=True)
print(x**2 + y**2 >= 1)
'''
x<sup>2</sup> + y<sup>2</sup> &ge; 1
'''

将打印的结果拷贝到markdown-cell中，显示如下

x2 + y2 ≥ 1

遍历表达式

x = Int('x')
y = Int('y')
n = x + y >= 3
print("num args: ", n.num_args())
print("children: ", n.children())
print("1st child:", n.arg(0))
print("2nd child:", n.arg(1))
print("operator: ", n.decl())
print("op name:  ", n.decl().name())
'''
num args:  2
children:  [x + y, 3]
1st child: x + y
2nd child: 3
operator:  &ge;
op name:   >=
'''

求解非线性多项式约束

Z3提供了所有基本的数学运算。Z3Py使用与Python语言相同的操作符优先级。和Python一样，**是幂运算符。Z3可以求解非线性多项式约束。

x = Real('x')
y = Real('y')
solve(x**2 + 0.12 * y**2 > 3, x**3 + y < 5)
'''
[x = 1/8, y = 639/128]
'''

实数表示

上面的程序Real('x')创建了实数变量x。Z3Py可以表示任意大的整数、有理数(如上面的例子)和无理数代数数。无理数是系数为整数的多项式的根。在内部，Z3精确地表示了所有这些数字。无理数以十进制表示，以便于阅读结果。

x = Real('x')
y = Real('y')
solve(x**2 + y**2 == 3, x**3 == 2)

set_option(precision=30)
print("Solving, and displaying result with 30 decimal places")
solve(x**2 + y**2 == 3, x**3 == 2)
'''
[x = 1.2599210498?, y = -1.1885280594?]
Solving, and displaying result with 30 decimal places
[x = 1.259921049894873164767210607278?,
 y = -1.188528059421316533710369365015?]
'''

set_option用于配置Z3环境。它用于设置全局配置选项，例如如何显示结果,set_option(precision=30)设置显示结果时使用的小数位数。1.259921049894873164767210607278?中的 ? 表示截断输出。

常见错误

表达式3/2是一个Python整数，而不是Z3有理数。下面示例展示了在Z3Py中创建有理数的不同方法。程序Q(num, den)创建一个Z3有理数，其中num是分子，den是分母。RealVal(1)创建一个Z3实数表示数字1。

print(1/3)
print(RealVal(1)/3)

x = Real('x')
print(x + 1/3)
print(x + "1/3")
print(x + 0.25)
'''
0.3333333333333333
1/3
x + 3333333333333333/10000000000000000
x + 1/3
x + 1/4
'''

用十进制数表示有理数

x = Real('x')
solve(3*x*x == 2)
'''
[x = -0.816496580927726032732428024901?]
'''
set_option(rational_to_decimal=True)
solve(3*x == 1)

set_option(precision=20)
solve(3*x == 1)
set_option(rational_to_decimal=False)
solve(6*x == 37)
'''
[x = 0.3333333333?]
[x = 0.33333333333333333333?]
[x = 37/6]
'''

约束系统可能没有解。在这种情况下，我们说这个系统是不可满足的。

x = Real('x')
solve(x > 4, x < 0)
'''
no solution
'''

布尔逻辑

Z3支持布尔运算符:And,Or, Not, Implies(implication)，If (If -then-else)。 Bi-implications 用 == 表示。下面的例子展示了如何求解一个简单的布尔约束集。

p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))
'''
[q = True, p = False, r = False]
'''

Python的布尔常量True和False可用于构建Z3布尔表达式。

p = Bool('p')
q = Bool('q')
print(And(p, q, True))
print(simplify(And(p, q, True)))
print(simplify(And(p, False)))
'''
And(p, q, True)
And(p, q)
False
'''

下面的例子使用了多项式和布尔约束的组合。

p = Bool('p')
x = Real('x')
solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
'''
[x = -1.4142135623?, p = False]
'''

Solvers

Z3提供不同的求解器。在前面的示例中使用的solve命令是使用Z3求解器API实现的。该实现可以在Z3发行版中的Z3 .py文件中找到。下面的示例演示了基本的SolverAPI

x = Int('x')
y = Int('y')

s = Solver()
print(s)

s.add(x > 10, y == x + 2)
print(s)
print("Solving constraints in the solver s ...")
print(s.check())

print("Create a new scope...")
s.push()
s.add(y < 11)
print(s)
print("Solving updated set of constraints...")
print(s.check())

print("Restoring state...")
s.pop()
print(s)
print("Solving restored set of constraints...")
print(s.check())
'''
[]
[x > 10, y == x + 2]
Solving constraints in the solver s ...
sat
Create a new scope...
[x > 10, y == x + 2, y < 11]
Solving updated set of constraints...
unsat
Restoring state...
[x > 10, y == x + 2]
Solving restored set of constraints...
sat
'''

命令Solver()创建一个通用求解器。可以使用add方法添加约束。我们说约束已在求解器中断言。check()方法求解断言的约束。如果找到了一个解，那么结果就是sat(satisfiable)可满足的。如果不存在解，结果就是unsat(unsatisfiable)(不可满足)。也可以说所断言的约束系统是不可行的。最后，求解器可能无法求解约束系统而返回未知数。

在一些应用中，我们想探讨几个类似的问题，共享几个约束条件。我们可以使用push和pop命令来实现这一点。每个求解器维护一个断言栈。命令push通过保存当前堆栈大小来创建一个新的范围。命令pop将删除与匹配push之间的任何断言。check方法总是对求解器断言堆栈的内容进行操作。

下面的例子显示了一个Z3无法解决的例子。在这种情况下，求解器返回unknown。回想一下，Z3可以解非线性多项式约束，但2**x不是多项式。

x = Real('x')
s = Solver()
s.add(2**x == 3)
print(s.check())
'''
unknown
'''

下面的示例演示如何遍历在求解器中断言的约束，以及如何为check方法收集性能统计信息。

x = Real('x')
y = Real('y')
s = Solver()
s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
print("asserted constraints...")
for c in s.assertions():
    print(c)

print(s.check())
print("statistics for the last check method...")
print(s.statistics())
# Traversing statistics
for k, v in s.statistics():
    print("%s : %s" % (k, v))
    
'''
asserted constraints...
x > 1
y > 1
Or(x + y > 3, x - y < 2)
sat
statistics for the last check method...
(:arith-make-feasible 3
 :arith-max-columns   8
 :arith-max-rows      2
 :arith-upper         4
 :decisions           2
 :final-checks        1
 :max-memory          2.90
 :memory              2.59
 :mk-bool-var         6
 :num-allocs          63585276
 :num-checks          1
 :rlimit-count        2013
 :time                0.01)
mk bool var : 1
decisions : 2
final checks : 1
num checks : 1
mk bool var : 5
arith-upper : 4
arith-make-feasible : 3
arith-max-columns : 8
arith-max-rows : 2
num allocs : 63585276
rlimit count : 2013
max memory : 2.9
memory : 2.59
time : 0.006
'''

当Z3为断言的约束集找到一个解时,check返回sat。我们说Z3满足这个约束集。我们说解是一组断言的约束的模型。模型是使每个断言的约束为真的解释。 We say the solution is a model for the set of asserted constraints. A model is an interpretation that makes each asserted constraint true.

下面的例子展示了检查模型的基本方法

x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
print(s.check())

m = s.model()
print("x = %s" % m[x])

print("traversing model...")
for d in m.decls():
    print("%s = %s" % (d.name(), m[d]))
'''
sat
x = 3/2
traversing model...
z = 0
y = 2
x = 3/2
'''

在上面的例子中，函数Reals('x y z')创建了变量x, y和z，是下面示例的简写

x = Real('x')
y = Real('y')
z = Real('z')

算数

Z3支持实数和整数变量。它们可以混合在一个问题中。像大多数编程语言一样，Z3Py会在需要时会自动强制转换。下面的例子演示了声明整数和实变量的不同方法。

x = Real('x')
y = Int('y')
a, b, c = Reals('a b c')
s, r = Ints('s r')
print(x + y + 1 + (a + s))
print(ToReal(y) + c)
'''
x + ToReal(y) + 1 + a + ToReal(s)
ToReal(y) + c
'''

Z3Py支持所有基本的算术操作。

a, b, c = Ints('a b c')
d, e = Reals('d e')
solve(a > b + 2,
      a == 2*c + 10,
      c + b <= 1000,
      d >= e)
'''
[c = 0, b = 0, e = 0, d = 0, a = 10]
'''

命令simplify对Z3表达式进行化简。

x, y = Reals('x y')
# 把表达式转换成多项式和的形式
t = simplify((x + y)**3, som=True)
print(t)
# 使用指数操作
t = simplify(t, mul_to_power=True)
print(t)
'''
x*x*x + 3*x*x*y + 3*x*y*y + y*y*y
x**3 + 3*x**2*y + 3*x*y**2 + y**3
'''

命令help_simplify()打印所有可用的 options 。Z3Py允许用户以两种方式使用option。

  • : option names，单词之间用 - 分隔
  • Z3Py也支持类似python的名称，其中不用 : ， - 被替换为 _ 。

下面的例子演示了如何使用这两种方式

x, y = Reals('x y')
# Using Z3 native option names
print(simplify(x == y + 2, ':arith-lhs', True))
# Using Z3Py option names
print(simplify(x == y + 2, arith_lhs=True))

print("\nAll available options:")
help_simplify() #内容较多，没有显示
'''
x + -1*y == 2
x + -1*y == 2

All available options:
'''

大数字

Z3Py支持任意大的数字。下面的例子演示如何使用较大的整数、有理数和无理数执行基本算术。Z3Py只支持代数无理数。代数无理数对于给出多项式约束系统的解是足够的。Z3Py将总是以十进制表示无理数，因为这样更便于阅读。内部表示可以使用方法sexpr()提取。它以s-expression(类似Lisp)表示法来显示数学公式和表达式的Z3内部表示形式。

x, y = Reals('x y')
solve(x + 10000000000000000000000 == y, y > 20000000000000000)

print(Sqrt(2) + Sqrt(3))
print(simplify(Sqrt(2) + Sqrt(3)))
print(simplify(Sqrt(2) + Sqrt(3)).sexpr())
# The sexpr() method is available for any Z3 expression
print((x + Sqrt(y) * 2).sexpr())
'''
[y = 20000000000000001, x = -9999979999999999999999]
2<sup>1/2</sup> + 3<sup>1/2</sup>
3.146264369941972342329135065715?
(root-obj (+ (^ x 4) (* (- 10) (^ x 2)) 1) 4)
(+ x (* (^ y (/ 1.0 2.0)) 2.0))
'''

机器运算

现代cpu和主流编程语言在固定大小的位向量上使用算术。Z3Py也可以使用位向量上的机器运算。它实现了无符号和有符号双补码算术的精确语义。
下面的例子演示了如何创建位向量变量和常量。函数BitVec('x',16)在Z3中创建了一个名为x的16位位向量变量。为了方便起见，在Z3Py中可以使用整数常量来创建位向量表达式。函数BitVecVal(10,32)创建一个32位的位向量，其值为10。

x = BitVec('x', 16)
y = BitVec('y', 16)
print(x + 2)
# 内部表示
print((x + 2).sexpr())

# -1和65535在16bit的时候相等
print(simplify(x + y - 1))

# 创建位向量常量
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print(simplify(a == b))

a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
# -1和65535在32bit的时候不相等
print(simplify(a == b))
'''
x + 2
(bvadd x #x0002)
65535 + x + y
True
False
'''

与编程语言相反，例如在C, C++，C#，Java中，有符号和无符号的位向量作为数字没有区别。相反，Z3提供了特殊的有符号版本的算术操作，其中位向量是有符号还是无符号处理是不同的。在Z3Py中，操作符<，<=，>，>=，/，%和>>对应有符号的版本。对应的无符号操作符是:ULT、ULE、UGT、UGE、UDiv、URem和LShR(logical shift right)。

#创建32bit的位向量
x, y = BitVecs('x y', 32)

solve(x + y == 2, x > 0, y > 0)
'''
[y = 1, x = 1]
'''
solve(x & y == ~y)

solve(x < 0)

# 使用无符号小于
solve(ULT(x, 0))
'''
[y = 4294967295, x = 0]
[x = 4294967295]
no solution
'''

x, y = BitVecs('x y', 32)

solve(x >> 2 == 3)
solve(x << 2 == 3)
solve(x << 2 == 24)
'''
[x = 12]
no solution
[x = 6]
'''

函数

在编程语言中，函数有副作用，可以抛出异常，或者永远不会返回，而Z3中的函数没有副作用，而且是完备的。也就是说，它定义在所有输入值上，包括像除法这样的函数。Z3是基于一阶逻辑的。

给定一个约束条件，例如x+y > 3,我们已经说过x和y是变量。在许多教科书中，x和y被称为未解释常数。也就是说，它们允许任何与约束x+y > 3一致的解释.

更准确地说，纯一阶逻辑中的函数符号和常数符号是未解释的或自由的，这意味着没有附加任何先验解释。这与属于理论特征的函数相反，例如算术函数 +有一个固定的标准解释(它加两个数)。未解释的函数和常量是最灵活的;它们允许任何与函数或常数约束一致的解释。

为了说明未解释的函数和常量，让我们来看看未解释的整数常量(也就是变量)x,y。最后，让f是一个未解释的函数，它接受一个整型参数(也就是sort)并得到一个整数值。这个例子说明了如何强制解释 f 对 x 应用两次会得到x，但 f 对 x 应用一次会不同于x。

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
solve(f(f(x)) == x, f(x) == y, x != y)
'''
[x = 0, y = 1, f = [1 -> 0, else -> 1]]
'''

f的解(解释)应该是f(0) = 1 f(1) = 0，f(a)=1(a≠0，a≠1)

在Z3中，我们也可以对约束系统的模型表达式求值。下面的示例演示如何使用evaluate方法。

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
print(s.check())
m = s.model()
print("f(f(x)) =", m.evaluate(f(f(x))))
print("f(x)    =", m.evaluate(f(x)))
'''
sat
f(f(x)) = 0
f(x)    = 1
'''

可满足性和有效性

validity:逻辑公式总是为真

satisfiable:逻辑公式有时候为真，有时候为假

unsatisfiable:逻辑公式永远为假

下面的例子证明了德摩根定律。下面的示例重新定义了Z3Py函数，它接收一个公式作为参数。这个函数创建一个Solver，添加/断言公式的否定，并检查否定是否不可满足。这个函数的实现是Z3Py命令prove的一个简单版本。

p, q = Bools('p q')
demorgan = And(p, q) == Not(Or(Not(p), Not(q)))
print(demorgan)

def prove(f):
    s = Solver()
    s.add(Not(f))
    if s.check() == unsat:
        print("proved")
    else:
        print("failed to prove")

print("Proving demorgan...")
prove(demorgan)
'''
And(p, q) == Not(Or(Not(p), Not(q)))
Proving demorgan...
proved
'''

列表推导

Python支持列表推导式。列表推导式提供了一种简洁的创建列表的方式。它们可以在Z3Py中创建Z3表达式和问题。下面的例子演示了如何在Z3Py中使用Python列表推导式。

# 创建列表 [1, ..., 5] 
print([ x + 1 for x in range(5) ])

# 创建两个包含5个整数变量的列表
X = [ Int('x%s' % i) for i in range(5) ]
Y = [ Int('y%s' % i) for i in range(5) ]
print(X)

# 创建一个包含 X[i]+Y[i] 的列表
X_plus_Y = [ X[i] + Y[i] for i in range(5) ]
print(X_plus_Y)

# 创建一个包含 X[i] > Y[i]的列表
X_gt_Y = [ X[i] > Y[i] for i in range(5) ]
print(X_gt_Y)

print(And(X_gt_Y))

#创建一个3*3的整数变量的矩阵
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(3) ]
      for i in range(3) ]
pp(X)
'''
[1, 2, 3, 4, 5]
[x0, x1, x2, x3, x4]
[x0 + y0, x1 + y1, x2 + y2, x3 + y3, x4 + y4]
[x0 > y0, x1 > y1, x2 > y2, x3 > y3, x4 > y4]
And(x0 > y0, x1 > y1, x2 > y2, x3 > y3, x4 > y4)
[[x_1_1, x_1_2, x_1_3],
 [x_2_1, x_2_2, x_2_3],
 [x_3_1, x_3_2, x_3_3]]
'''

pp命令类似于print，但它使用Z3Py格式化器来格式化列表和元组，而不是Python的格式化器。
Z3Py还提供了创建布尔值、整数和实变量的向量的函数。这些函数是使用列表推导式实现的。

X = IntVector('x', 5)
Y = RealVector('y', 5)
P = BoolVector('p', 5)
print(X)
print(Y)
print(P)
print([ y**2 for y in Y ])
print(Sum([ y**2 for y in Y ]))
'''
[x__0, x__1, x__2, x__3, x__4]
[y__0, y__1, y__2, y__3, y__4]
[p__0, p__1, p__2, p__3, p__4]
[y__0**2, y__1**2, y__2**2, y__3**2, y__4**2]
y__0**2 + y__1**2 + y__2**2 + y__3**2 + y__4**2
'''

应用

运动学方程

在高中，学生学习运动学方程。这些方程描述了位移(d)、时间(t)、加速度(a)、初速度(v_i)和最终速度(v_f)之间的数学关系。在Z3Py表示法中，我们可以把这些方程写成:

a, t ,v_i, v_f = Reals('a t v__i v__f') #missing in HTML?
d == v_i * t + (a*t**2)/2,
v_f == v_i + a*t

vf =vi+a*t

v_f

vf

问题1

小明正以30.0米/秒的速度接近红绿灯。红灯变成黄色，小明踩下刹车，刹了下来。如果小明的加速度为-8.00 m/s2，则确定汽车在打滑过程中的位移。

d, a, t, v_i, v_f = Reals('d a t v__i v__f')

equations = [
   d == v_i * t + (a*t**2)/2,
   v_f == v_i + a*t,
]
print("Kinematic equations:")
print(equations)

# Given v_i, v_f and a, find d
problem = [
    v_i == 30,
    v_f == 0,
    a   == -8
]
print("Problem:")
print(problem)

print("Solution:")
solve(equations + problem)
'''
Kinematic equations:
[d == v__i*t + (a*t**2)/2, v__f == v__i + a*t]
Problem:
[v__i == 30, v__f == 0, a == -8]
Solution:
[a = -8, v__f = 0, v__i = 30, t = 15/4, d = 225/4]
'''

问题2

小明在等红灯。当最终变绿时，小明从静止开始加速，速度为6.00 m/s2，持续时间为4.10秒。确定小明在这段时间的位移。

d, a, t, v_i, v_f = Reals('d a t v__i v__f')

equations = [
   d == v_i * t + (a*t**2)/2,
   v_f == v_i + a*t,
]

# Given v_i, t and a, find d
problem = [
    v_i == 0,
    t   == 4.10,
    a   == 6
]

solve(equations + problem)

# Display rationals in decimal notation
set_option(rational_to_decimal=True)

solve(equations + problem)
'''
[a = 6, t = 41/10, v__i = 0, v__f = 123/5, d = 5043/100]
[a = 6, t = 4.1, v__i = 0, v__f = 24.6, d = 50.43]
'''

比特陷阱

经常在C程序(包括Z3)中测试一个机器整数是否为2的幂。我们可以用Z3来证明。当且仅当x是2的幂时，x != 0 && !(x & (x - 1))为真

x      = BitVec('x', 32)
powers = [ 2**i for i in range(32) ]
fast   = And(x != 0, x & (x - 1) == 0)
slow   = Or([ x == p for p in powers ])
print(fast)
prove(fast == slow)

print("trying to prove buggy version...")
fast   = x & (x - 1) == 0
prove(fast == slow)
'''
And(x != 0, x & x - 1 == 0)
proved
trying to prove buggy version...
failed to prove
'''

测试两个机器整数是否有相反的符号。

x      = BitVec('x', 32)
y      = BitVec('y', 32)

# Claim: (x ^ y) < 0 iff x and y have opposite signs
trick  = (x ^ y) < 0

# Naive way to check if x and y have opposite signs
opposite = Or(And(x < 0, y >= 0),
              And(x >= 0, y < 0))

prove(trick == opposite)
'''
proved
'''

谜题

考虑一下下面的难题。花100美元买100只动物。狗要15美元，猫要1美元，老鼠每只25美分。你必须至少买一种。每种你应该买多少?

# Create 3 integer variables
dog, cat, mouse = Ints('dog cat mouse')
solve(dog >= 1,   # at least one dog
      cat >= 1,   # at least one cat
      mouse >= 1, # at least one mouse
      # we want to buy 100 animals
      dog + cat + mouse == 100,
      # We have 100 dollars (10000 cents):
      #   dogs cost 15 dollars (1500 cents), 
      #   cats cost 1 dollar (100 cents), and 
      #   mice cost 25 cents 
      1500 * dog + 100 * cat + 25 * mouse == 10000)
'''
[cat = 41, mouse = 56, dog = 3]
'''

数独

数独是一种非常流行的益智游戏。目标是在方框中插入数字，只满足一个条件:每一行、每一列和3x3的方框必须恰好包含1到9的数字一次。
在这里插入图片描述
下面的例子对Z3中的数独问题进行了编码。不同的数独实例可以通过修改矩阵实例来解决。这个例子大量使用了Python编程语言中的列表推导式。


 # 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
             for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
             for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
                        for i in range(3) for j in range(3) ])
             for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
                  True,
                  X[i][j] == instance[i][j])
               for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
          for i in range(9) ]
    print_matrix(r)
else:
    print("failed to solve")
    

# Let us remove 9 from the first row and see if there is more than one solution

instance = ((0,0,0,0,0,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
                  True,
                  X[i][j] == instance[i][j])
               for i in range(9) for j in range(9) ]    
    
def n_solutions(n):
    s = Solver()
    s.add(sudoku_c + instance_c)
    i = 0
    while s.check() == sat and i < n:
        m = s.model()
        print([[ m.evaluate(X[i][j]) for j in range(9)] for i in range(9)])
        fml = And([X[i][j] == m.evaluate(X[i][j]) for i in range(9) for j in range(9)])
        s.add(Not(fml))
        i += 1
        
n_solutions(10)
'''
[[7, 1, 5, 8, 9, 4, 6, 3, 2],
 [2, 3, 4, 5, 1, 6, 8, 9, 7],
 [6, 8, 9, 7, 2, 3, 1, 4, 5],
 [4, 9, 3, 6, 5, 7, 2, 1, 8],
 [8, 6, 7, 2, 3, 1, 9, 5, 4],
 [1, 5, 2, 4, 8, 9, 7, 6, 3],
 [3, 7, 6, 1, 4, 8, 5, 2, 9],
 [9, 2, 8, 3, 6, 5, 4, 7, 1],
 [5, 4, 1, 9, 7, 2, 3, 8, 6]]
[[5, 1, 6, 7, 8, 4, 9, 3, 2], [2, 3, 4, 5, 1, 9, 6, 8, 7], [7, 8, 9, 6, 2, 3, 1, 4, 5], [3, 9, 7, 4, 5, 6, 2, 1, 8], [4, 6, 8, 2, 9, 1, 7, 5, 3], [1, 5, 2, 8, 3, 7, 4, 9, 6], [6, 7, 3, 1, 4, 8, 5, 2, 9], [9, 2, 1, 3, 6, 5, 8, 7, 4], [8, 4, 5, 9, 7, 2, 3, 6, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 8, 6, 7], [5, 8, 9, 6, 3, 7, 1, 4, 2], [4, 9, 7, 3, 5, 6, 2, 1, 8], [8, 6, 3, 2, 9, 1, 7, 5, 4], [1, 5, 2, 7, 4, 8, 3, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 4, 7, 3], [3, 4, 5, 9, 7, 2, 6, 8, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 8, 6, 7], [5, 8, 9, 6, 3, 7, 1, 4, 2], [4, 9, 3, 7, 5, 6, 2, 1, 8], [8, 6, 7, 2, 9, 1, 3, 5, 4], [1, 5, 2, 3, 4, 8, 7, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 4, 7, 3], [3, 4, 5, 9, 7, 2, 6, 8, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 8, 6, 7], [5, 8, 9, 6, 3, 7, 1, 4, 2], [4, 9, 3, 7, 5, 6, 2, 1, 8], [8, 6, 7, 2, 9, 1, 4, 5, 3], [1, 5, 2, 3, 4, 8, 7, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 3, 7, 4], [3, 4, 5, 9, 7, 2, 6, 8, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 6, 8, 7], [5, 8, 9, 6, 3, 7, 1, 4, 2], [4, 9, 3, 7, 5, 6, 2, 1, 8], [8, 6, 7, 2, 9, 1, 4, 5, 3], [1, 5, 2, 3, 4, 8, 7, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 3, 7, 4], [3, 4, 5, 9, 7, 2, 8, 6, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 6, 8, 7], [5, 8, 9, 6, 3, 7, 1, 4, 2], [4, 9, 3, 7, 5, 6, 2, 1, 8], [8, 6, 7, 2, 9, 1, 3, 5, 4], [1, 5, 2, 3, 4, 8, 7, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 4, 7, 3], [3, 4, 5, 9, 7, 2, 8, 6, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 6, 8, 7], [5, 8, 9, 6, 3, 7, 1, 4, 2], [4, 9, 7, 3, 5, 6, 2, 1, 8], [8, 6, 3, 2, 9, 1, 7, 5, 4], [1, 5, 2, 7, 4, 8, 3, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 4, 7, 3], [3, 4, 5, 9, 7, 2, 8, 6, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 6, 8, 7], [5, 8, 9, 7, 3, 6, 1, 4, 2], [4, 9, 3, 6, 5, 7, 2, 1, 8], [8, 6, 7, 2, 9, 1, 3, 5, 4], [1, 5, 2, 3, 4, 8, 7, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 4, 7, 3], [3, 4, 5, 9, 7, 2, 8, 6, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 6, 8, 7], [5, 8, 9, 7, 3, 6, 1, 4, 2], [4, 9, 3, 6, 5, 7, 2, 1, 8], [8, 6, 7, 2, 9, 1, 4, 5, 3], [1, 5, 2, 3, 4, 8, 7, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 3, 7, 4], [3, 4, 5, 9, 7, 2, 8, 6, 1]]
[[7, 1, 6, 8, 2, 4, 9, 3, 5], [2, 3, 4, 5, 1, 9, 8, 6, 7], [5, 8, 9, 7, 3, 6, 1, 4, 2], [4, 9, 3, 6, 5, 7, 2, 1, 8], [8, 6, 7, 2, 9, 1, 4, 5, 3], [1, 5, 2, 3, 4, 8, 7, 9, 6], [6, 7, 1, 4, 8, 3, 5, 2, 9], [9, 2, 8, 1, 6, 5, 3, 7, 4], [3, 4, 5, 9, 7, 2, 6, 8, 1]]

'''

八皇后问题

8个皇后谜题是将8个皇后放在一个8x8的棋盘上，这样就不会有两个皇后互相攻击。因此，一个解决方案要求没有两个皇后共享同一行、列或对角线。
在这里插入图片描述

# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Queens = [ Int('Q_%i' % (i + 1)) for i in range(8) ]

# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Queens[i], Queens[i] <= 8) for i in range(8) ]

# At most one queen per column
col_c = [ Distinct(Queens) ]

# Diagonal constraint
diag_c = [ If(i == j,
              True,
              And(Queens[i] - Queens[j] != i - j, Queens[i] - Queens[j] != j - i))
           for i in range(8) for j in range(i) ]

solve(val_c + col_c + diag_c)
'''
[Q_5 = 6,
 Q_8 = 5,
 Q_3 = 7,
 Q_2 = 2,
 Q_6 = 8,
 Q_4 = 3,
 Q_7 = 1,
 Q_1 = 4]
'''

程序安装

安装问题包括确定是否可以在系统中安装一组新的包。这个应用程序是基于文章 OPIUM: Optimal Package Install/Uninstall Manager. 。许多包依赖于其他包来提供某些功能。每个发行版都包含一个元数据文件，它解释了发行版每个包的需求。元数据包含名称、版本等细节。更重要的是，它包含了依赖和冲突条款，规定了哪些包应该在系统上。依情况而定的条款规定了还必须附加哪些包。冲突条款规定其他包不得出现。

使用Z3可以很容易地解决安装问题。其思想是为每个包定义一个布尔变量。如果包必须在系统中，则此变量为true。如果包a依赖于包b、包c和包z，

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

#DependsOn(a, [b, c, z])
#DependsOn is a simple Python function that creates Z3 constraints that capture the depends clause semantics.

def DependsOn(pack, deps):
   return And([ Implies(pack, dep) for dep in deps ])

#Thus, DependsOn(a, [b, c, z]) generates the constraint
# And(Implies(a, b), Implies(a, c), Implies(a, z))

print(DependsOn(a, [b, c, z]))

#That is, if users install package a, they must also install packages b, c and z.

#If package d conflicts with package e, we write Conflict(d, e). Conflict is also a simple Python function.

def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))

# Conflict(d, e) generates the constraint Or(Not(d), Not(e)). 
# With these two functions, we can easily encode the example 
# in the Opium article (Section 2) in Z3Py as:

def DependsOn(pack, deps):
    return And([ Implies(pack, dep) for dep in deps ])

def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))


solve(DependsOn(a, [b, c, z]),
      DependsOn(b, [d]),
      DependsOn(c, [Or(d, e), Or(f, g)]),
      Conflict(d, e),
      a, z)
def install_check(*problem):
    s = Solver()
    s.add(*problem)
    if s.check() == sat:
        m = s.model()
        r = []
        for x in m:
            if is_true(m[x]):
                # x is a Z3 declaration
                # x() returns the Z3 expression
                # x.name() returns a string
                r.append(x())
        print(r)
    else:
        print("invalid installation profile")

print("Check 1")
install_check(DependsOn(a, [b, c, z]),
              DependsOn(b, [d]),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z)

print("Check 2")
install_check(DependsOn(a, [b, c, z]),
              #DependsOn(b, d),
              DependsOn(b, [d]),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z, g)
'''
And(Implies(a, b), Implies(a, c), Implies(a, z))
[f = False,
 b = True,
 a = True,
 d = True,
 g = True,
 z = True,
 c = True,
 e = False]
 Check 1
[f, b, a, d, z, c]
Check 2
invalid installation profile
'''