Python 中的 Z3 计数器变量数组
Array of Z3 Counter variables in Python
我想创建一个 Z3 数组 (A)，其元素是 Z3 Int 变量，并且每个元素都有一个固定的范围。另外，我想 初始化 这些元素的值为 0。
现在假设有一个简单的函数 x1 + x2 + x3 = 6，其中 0 <= x1, x2, x3 <= 4，其中 x1, x2, x3 是 Z3 Int 变量。
接下来，我想将A的x1、x2、x3索引位置的值（x1、x2、x3的值由Z3决定）增加1。
例如：
我的问题是如何用尽可能低的值初始化 Z3 变量并将其用作计数器变量？
注意：最大。和分钟。 x1、x2 和 x3 的可能值始终分别是 A 的最低和最高索引。
一般注意事项：
给定赋值(x1, x2, x3) = (v1, v2, v3)，(v1, v2, v3)的任意排列也是问题的解。在某些情况下，在搜索 space 中 打破对称性 可能很方便，例如 ∀ i, j.((i < j) => (x_i <= x_j)).
将每个位置 A_i 视为分配了值 [=21] 的所有 x_j 的 编号 会容易得多=].
Python + z3:
from z3 import *
def model_to_str(m):
fmt = "\t A:= {}; x := {};"
A_tuple = tuple([m.eval(el) for el in A_list])
x_tuple = tuple([m.eval(el) for el in x_list])
return fmt.format(A_tuple, x_tuple)
###########
# PROBLEM #
###########
s = Solver()
# declarations
A_length = 5
A_list = [Int('A_{0}'.format(idx)) for idx in range(0, A_length)]
x_list = [Int('x_{0}'.format(idx)) for idx in range(0, 3)]
# A's constraints
for i, A_i in enumerate(A_list):
s.add(A_i == Sum([If(x_j == i, 1, 0) for x_j in x_list]))
s.add(A_i <= 2)
# x's constraints
s.add(6 == Sum(x_list))
for x_i in x_list:
s.add(0 <= x_i)
s.add(x_i < A_length)
# Symmetry-breaking constraints:
# (remove symmetry solutions)
#s.add(x_list[0] <= x_list[1])
#s.add(x_list[0] <= x_list[2])
#s.add(x_list[1] <= x_list[2])
# Get one solution:
if s.check() == sat:
print("Random Solution:")
print(model_to_str(s.model()))
# Get all solutions:
s.push()
print("\nEnumerate All Solutions:")
while s.check() == sat:
m = s.model()
print(model_to_str(m))
s.add(Or([x_j != m.eval(x_j) for x_j in x_list]))
s.pop()
# Enumerate all possible assignments
print("\nTry All Possible Assignments:")
for x_0_val in range(0, A_length):
for x_1_val in range(0, A_length):
for x_2_val in range(0, A_length):
values = (x_0_val, x_1_val, x_2_val)
s.push()
s.add([x_j == x_j_val for x_j, x_j_val in zip(x_list, values)])
if s.check() == sat:
print(model_to_str(s.model()))
else:
print("\t\tx := {} is unsat!".format(values))
s.pop()
输出：
Random Solution:
A:= (1, 0, 1, 0, 1); x := (4, 0, 2);
Enumerate All Solutions:
A:= (1, 0, 1, 0, 1); x := (2, 0, 4);
A:= (1, 0, 1, 0, 1); x := (2, 4, 0);
A:= (0, 1, 1, 1, 0); x := (2, 1, 3);
A:= (0, 1, 1, 1, 0); x := (2, 3, 1);
A:= (1, 0, 0, 2, 0); x := (3, 3, 0);
A:= (1, 0, 1, 0, 1); x := (4, 0, 2);
A:= (0, 2, 0, 0, 1); x := (4, 1, 1);
A:= (1, 0, 1, 0, 1); x := (4, 2, 0);
A:= (0, 1, 1, 1, 0); x := (3, 2, 1);
A:= (1, 0, 1, 0, 1); x := (0, 2, 4);
A:= (0, 1, 1, 1, 0); x := (1, 2, 3);
A:= (1, 0, 1, 0, 1); x := (0, 4, 2);
A:= (0, 1, 1, 1, 0); x := (1, 3, 2);
A:= (0, 2, 0, 0, 1); x := (1, 4, 1);
A:= (1, 0, 0, 2, 0); x := (0, 3, 3);
A:= (0, 2, 0, 0, 1); x := (1, 1, 4);
A:= (1, 0, 0, 2, 0); x := (3, 0, 3);
A:= (0, 1, 1, 1, 0); x := (3, 1, 2);
Try All Possible Assignments:
x := (0, 0, 0) is unsat!
x := (0, 0, 1) is unsat!
x := (0, 0, 2) is unsat!
x := (0, 0, 3) is unsat!
x := (0, 0, 4) is unsat!
x := (0, 1, 0) is unsat!
x := (0, 1, 1) is unsat!
x := (0, 1, 2) is unsat!
x := (0, 1, 3) is unsat!
x := (0, 1, 4) is unsat!
x := (0, 2, 0) is unsat!
x := (0, 2, 1) is unsat!
x := (0, 2, 2) is unsat!
x := (0, 2, 3) is unsat!
A:= (1, 0, 1, 0, 1); x := (0, 2, 4);
x := (0, 3, 0) is unsat!
x := (0, 3, 1) is unsat!
x := (0, 3, 2) is unsat!
A:= (1, 0, 0, 2, 0); x := (0, 3, 3);
x := (0, 3, 4) is unsat!
x := (0, 4, 0) is unsat!
x := (0, 4, 1) is unsat!
A:= (1, 0, 1, 0, 1); x := (0, 4, 2);
x := (0, 4, 3) is unsat!
x := (0, 4, 4) is unsat!
x := (1, 0, 0) is unsat!
x := (1, 0, 1) is unsat!
x := (1, 0, 2) is unsat!
x := (1, 0, 3) is unsat!
x := (1, 0, 4) is unsat!
x := (1, 1, 0) is unsat!
x := (1, 1, 1) is unsat!
x := (1, 1, 2) is unsat!
x := (1, 1, 3) is unsat!
A:= (0, 2, 0, 0, 1); x := (1, 1, 4);
x := (1, 2, 0) is unsat!
x := (1, 2, 1) is unsat!
x := (1, 2, 2) is unsat!
A:= (0, 1, 1, 1, 0); x := (1, 2, 3);
x := (1, 2, 4) is unsat!
x := (1, 3, 0) is unsat!
x := (1, 3, 1) is unsat!
A:= (0, 1, 1, 1, 0); x := (1, 3, 2);
x := (1, 3, 3) is unsat!
x := (1, 3, 4) is unsat!
x := (1, 4, 0) is unsat!
A:= (0, 2, 0, 0, 1); x := (1, 4, 1);
x := (1, 4, 2) is unsat!
x := (1, 4, 3) is unsat!
x := (1, 4, 4) is unsat!
x := (2, 0, 0) is unsat!
x := (2, 0, 1) is unsat!
x := (2, 0, 2) is unsat!
x := (2, 0, 3) is unsat!
A:= (1, 0, 1, 0, 1); x := (2, 0, 4);
x := (2, 1, 0) is unsat!
x := (2, 1, 1) is unsat!
x := (2, 1, 2) is unsat!
A:= (0, 1, 1, 1, 0); x := (2, 1, 3);
x := (2, 1, 4) is unsat!
x := (2, 2, 0) is unsat!
x := (2, 2, 1) is unsat!
x := (2, 2, 2) is unsat!
x := (2, 2, 3) is unsat!
x := (2, 2, 4) is unsat!
x := (2, 3, 0) is unsat!
A:= (0, 1, 1, 1, 0); x := (2, 3, 1);
x := (2, 3, 2) is unsat!
x := (2, 3, 3) is unsat!
x := (2, 3, 4) is unsat!
A:= (1, 0, 1, 0, 1); x := (2, 4, 0);
x := (2, 4, 1) is unsat!
x := (2, 4, 2) is unsat!
x := (2, 4, 3) is unsat!
x := (2, 4, 4) is unsat!
x := (3, 0, 0) is unsat!
x := (3, 0, 1) is unsat!
x := (3, 0, 2) is unsat!
A:= (1, 0, 0, 2, 0); x := (3, 0, 3);
x := (3, 0, 4) is unsat!
x := (3, 1, 0) is unsat!
x := (3, 1, 1) is unsat!
A:= (0, 1, 1, 1, 0); x := (3, 1, 2);
x := (3, 1, 3) is unsat!
x := (3, 1, 4) is unsat!
x := (3, 2, 0) is unsat!
A:= (0, 1, 1, 1, 0); x := (3, 2, 1);
x := (3, 2, 2) is unsat!
x := (3, 2, 3) is unsat!
x := (3, 2, 4) is unsat!
A:= (1, 0, 0, 2, 0); x := (3, 3, 0);
x := (3, 3, 1) is unsat!
x := (3, 3, 2) is unsat!
x := (3, 3, 3) is unsat!
x := (3, 3, 4) is unsat!
x := (3, 4, 0) is unsat!
x := (3, 4, 1) is unsat!
x := (3, 4, 2) is unsat!
x := (3, 4, 3) is unsat!
x := (3, 4, 4) is unsat!
x := (4, 0, 0) is unsat!
x := (4, 0, 1) is unsat!
A:= (1, 0, 1, 0, 1); x := (4, 0, 2);
x := (4, 0, 3) is unsat!
x := (4, 0, 4) is unsat!
x := (4, 1, 0) is unsat!
A:= (0, 2, 0, 0, 1); x := (4, 1, 1);
x := (4, 1, 2) is unsat!
x := (4, 1, 3) is unsat!
x := (4, 1, 4) is unsat!
A:= (1, 0, 1, 0, 1); x := (4, 2, 0);
x := (4, 2, 1) is unsat!
x := (4, 2, 2) is unsat!
x := (4, 2, 3) is unsat!
x := (4, 2, 4) is unsat!
x := (4, 3, 0) is unsat!
x := (4, 3, 1) is unsat!
x := (4, 3, 2) is unsat!
x := (4, 3, 3) is unsat!
x := (4, 3, 4) is unsat!
x := (4, 4, 0) is unsat!
x := (4, 4, 1) is unsat!
x := (4, 4, 2) is unsat!
x := (4, 4, 3) is unsat!
x := (4, 4, 4) is unsat!
MiniZinc + z3:
我也想分享这种方法，因为在 MiniZinc 中我只花了 5 分钟 就解决了这个问题，比z3py.
[注意： 对于此任务，我使用 fzn2omt project 中的 fzn2z3.py 脚本。]
文件counter.mzn：（一般问题结构）
include "globals.mzn";
% PARAMETERS
set of int: DOMAIN_A;
set of int: INDEX_SET_A;
set of int: DOMAIN_X = INDEX_SET_A;
set of int: INDEX_SET_X;
% VARIABLES
array [INDEX_SET_A] of var DOMAIN_A: A;
array [INDEX_SET_X] of var DOMAIN_X: x;
% CONSTRAINTS
constraint sum(x) == 6;
constraint forall(i in INDEX_SET_A) (
A[i] = sum(j in INDEX_SET_X)(x[j] == i)
);
% SYMMETRY BREAKING CONTRAINT
constraint increasing(x);
solve satisfy;
(注意:我在这个问题上启用了对称性破坏约束只是为了减少解决方案的数量打印在下面。）
文件counter.dzn：（实例特定数据）
DOMAIN_A = 0..2;
INDEX_SET_A = 0..4;
INDEX_SET_X = 1..3;
找到一个解决方案 z3:
~$ mzn2fzn counter.mzn counter.dzn
~$ fzn2z3.py counter.fzn
x = array1d(1..3, [1, 1, 4]);
A = array1d(0..4, [0, 2, 0, 0, 1]);
----------
找到所有可能的解决方案（仅限 optimathsat）：
~$ mzn2fzn counter.mzn counter.dzn
~$ fzn2optimathsat.py --all-solutions counter.fzn
% allsat model
x = array1d(1..3, [1, 1, 4]);
A = array1d(0..4, [0, 2, 0, 0, 1]);
----------
% allsat model
x = array1d(1..3, [0, 2, 4]);
A = array1d(0..4, [1, 0, 1, 0, 1]);
----------
% allsat model
x = array1d(1..3, [0, 3, 3]);
A = array1d(0..4, [1, 0, 0, 2, 0]);
----------
% allsat model
x = array1d(1..3, [1, 2, 3]);
A = array1d(0..4, [0, 1, 1, 1, 0]);
----------
==========
我想创建一个 Z3 数组 (A)，其元素是 Z3 Int 变量，并且每个元素都有一个固定的范围。另外，我想 初始化 这些元素的值为 0。 现在假设有一个简单的函数 x1 + x2 + x3 = 6，其中 0 <= x1, x2, x3 <= 4，其中 x1, x2, x3 是 Z3 Int 变量。 接下来，我想将A的x1、x2、x3索引位置的值（x1、x2、x3的值由Z3决定）增加1。
例如：
我的问题是如何用尽可能低的值初始化 Z3 变量并将其用作计数器变量？
注意：最大。和分钟。 x1、x2 和 x3 的可能值始终分别是 A 的最低和最高索引。
一般注意事项：
给定赋值
(x1, x2, x3) = (v1, v2, v3)，(v1, v2, v3)的任意排列也是问题的解。在某些情况下，在搜索 space 中 打破对称性 可能很方便，例如∀ i, j.((i < j) => (x_i <= x_j)).将每个位置
A_i视为分配了值 [=21] 的所有x_j的 编号 会容易得多=].
Python + z3:
from z3 import *
def model_to_str(m):
fmt = "\t A:= {}; x := {};"
A_tuple = tuple([m.eval(el) for el in A_list])
x_tuple = tuple([m.eval(el) for el in x_list])
return fmt.format(A_tuple, x_tuple)
###########
# PROBLEM #
###########
s = Solver()
# declarations
A_length = 5
A_list = [Int('A_{0}'.format(idx)) for idx in range(0, A_length)]
x_list = [Int('x_{0}'.format(idx)) for idx in range(0, 3)]
# A's constraints
for i, A_i in enumerate(A_list):
s.add(A_i == Sum([If(x_j == i, 1, 0) for x_j in x_list]))
s.add(A_i <= 2)
# x's constraints
s.add(6 == Sum(x_list))
for x_i in x_list:
s.add(0 <= x_i)
s.add(x_i < A_length)
# Symmetry-breaking constraints:
# (remove symmetry solutions)
#s.add(x_list[0] <= x_list[1])
#s.add(x_list[0] <= x_list[2])
#s.add(x_list[1] <= x_list[2])
# Get one solution:
if s.check() == sat:
print("Random Solution:")
print(model_to_str(s.model()))
# Get all solutions:
s.push()
print("\nEnumerate All Solutions:")
while s.check() == sat:
m = s.model()
print(model_to_str(m))
s.add(Or([x_j != m.eval(x_j) for x_j in x_list]))
s.pop()
# Enumerate all possible assignments
print("\nTry All Possible Assignments:")
for x_0_val in range(0, A_length):
for x_1_val in range(0, A_length):
for x_2_val in range(0, A_length):
values = (x_0_val, x_1_val, x_2_val)
s.push()
s.add([x_j == x_j_val for x_j, x_j_val in zip(x_list, values)])
if s.check() == sat:
print(model_to_str(s.model()))
else:
print("\t\tx := {} is unsat!".format(values))
s.pop()
输出：
Random Solution:
A:= (1, 0, 1, 0, 1); x := (4, 0, 2);
Enumerate All Solutions:
A:= (1, 0, 1, 0, 1); x := (2, 0, 4);
A:= (1, 0, 1, 0, 1); x := (2, 4, 0);
A:= (0, 1, 1, 1, 0); x := (2, 1, 3);
A:= (0, 1, 1, 1, 0); x := (2, 3, 1);
A:= (1, 0, 0, 2, 0); x := (3, 3, 0);
A:= (1, 0, 1, 0, 1); x := (4, 0, 2);
A:= (0, 2, 0, 0, 1); x := (4, 1, 1);
A:= (1, 0, 1, 0, 1); x := (4, 2, 0);
A:= (0, 1, 1, 1, 0); x := (3, 2, 1);
A:= (1, 0, 1, 0, 1); x := (0, 2, 4);
A:= (0, 1, 1, 1, 0); x := (1, 2, 3);
A:= (1, 0, 1, 0, 1); x := (0, 4, 2);
A:= (0, 1, 1, 1, 0); x := (1, 3, 2);
A:= (0, 2, 0, 0, 1); x := (1, 4, 1);
A:= (1, 0, 0, 2, 0); x := (0, 3, 3);
A:= (0, 2, 0, 0, 1); x := (1, 1, 4);
A:= (1, 0, 0, 2, 0); x := (3, 0, 3);
A:= (0, 1, 1, 1, 0); x := (3, 1, 2);
Try All Possible Assignments:
x := (0, 0, 0) is unsat!
x := (0, 0, 1) is unsat!
x := (0, 0, 2) is unsat!
x := (0, 0, 3) is unsat!
x := (0, 0, 4) is unsat!
x := (0, 1, 0) is unsat!
x := (0, 1, 1) is unsat!
x := (0, 1, 2) is unsat!
x := (0, 1, 3) is unsat!
x := (0, 1, 4) is unsat!
x := (0, 2, 0) is unsat!
x := (0, 2, 1) is unsat!
x := (0, 2, 2) is unsat!
x := (0, 2, 3) is unsat!
A:= (1, 0, 1, 0, 1); x := (0, 2, 4);
x := (0, 3, 0) is unsat!
x := (0, 3, 1) is unsat!
x := (0, 3, 2) is unsat!
A:= (1, 0, 0, 2, 0); x := (0, 3, 3);
x := (0, 3, 4) is unsat!
x := (0, 4, 0) is unsat!
x := (0, 4, 1) is unsat!
A:= (1, 0, 1, 0, 1); x := (0, 4, 2);
x := (0, 4, 3) is unsat!
x := (0, 4, 4) is unsat!
x := (1, 0, 0) is unsat!
x := (1, 0, 1) is unsat!
x := (1, 0, 2) is unsat!
x := (1, 0, 3) is unsat!
x := (1, 0, 4) is unsat!
x := (1, 1, 0) is unsat!
x := (1, 1, 1) is unsat!
x := (1, 1, 2) is unsat!
x := (1, 1, 3) is unsat!
A:= (0, 2, 0, 0, 1); x := (1, 1, 4);
x := (1, 2, 0) is unsat!
x := (1, 2, 1) is unsat!
x := (1, 2, 2) is unsat!
A:= (0, 1, 1, 1, 0); x := (1, 2, 3);
x := (1, 2, 4) is unsat!
x := (1, 3, 0) is unsat!
x := (1, 3, 1) is unsat!
A:= (0, 1, 1, 1, 0); x := (1, 3, 2);
x := (1, 3, 3) is unsat!
x := (1, 3, 4) is unsat!
x := (1, 4, 0) is unsat!
A:= (0, 2, 0, 0, 1); x := (1, 4, 1);
x := (1, 4, 2) is unsat!
x := (1, 4, 3) is unsat!
x := (1, 4, 4) is unsat!
x := (2, 0, 0) is unsat!
x := (2, 0, 1) is unsat!
x := (2, 0, 2) is unsat!
x := (2, 0, 3) is unsat!
A:= (1, 0, 1, 0, 1); x := (2, 0, 4);
x := (2, 1, 0) is unsat!
x := (2, 1, 1) is unsat!
x := (2, 1, 2) is unsat!
A:= (0, 1, 1, 1, 0); x := (2, 1, 3);
x := (2, 1, 4) is unsat!
x := (2, 2, 0) is unsat!
x := (2, 2, 1) is unsat!
x := (2, 2, 2) is unsat!
x := (2, 2, 3) is unsat!
x := (2, 2, 4) is unsat!
x := (2, 3, 0) is unsat!
A:= (0, 1, 1, 1, 0); x := (2, 3, 1);
x := (2, 3, 2) is unsat!
x := (2, 3, 3) is unsat!
x := (2, 3, 4) is unsat!
A:= (1, 0, 1, 0, 1); x := (2, 4, 0);
x := (2, 4, 1) is unsat!
x := (2, 4, 2) is unsat!
x := (2, 4, 3) is unsat!
x := (2, 4, 4) is unsat!
x := (3, 0, 0) is unsat!
x := (3, 0, 1) is unsat!
x := (3, 0, 2) is unsat!
A:= (1, 0, 0, 2, 0); x := (3, 0, 3);
x := (3, 0, 4) is unsat!
x := (3, 1, 0) is unsat!
x := (3, 1, 1) is unsat!
A:= (0, 1, 1, 1, 0); x := (3, 1, 2);
x := (3, 1, 3) is unsat!
x := (3, 1, 4) is unsat!
x := (3, 2, 0) is unsat!
A:= (0, 1, 1, 1, 0); x := (3, 2, 1);
x := (3, 2, 2) is unsat!
x := (3, 2, 3) is unsat!
x := (3, 2, 4) is unsat!
A:= (1, 0, 0, 2, 0); x := (3, 3, 0);
x := (3, 3, 1) is unsat!
x := (3, 3, 2) is unsat!
x := (3, 3, 3) is unsat!
x := (3, 3, 4) is unsat!
x := (3, 4, 0) is unsat!
x := (3, 4, 1) is unsat!
x := (3, 4, 2) is unsat!
x := (3, 4, 3) is unsat!
x := (3, 4, 4) is unsat!
x := (4, 0, 0) is unsat!
x := (4, 0, 1) is unsat!
A:= (1, 0, 1, 0, 1); x := (4, 0, 2);
x := (4, 0, 3) is unsat!
x := (4, 0, 4) is unsat!
x := (4, 1, 0) is unsat!
A:= (0, 2, 0, 0, 1); x := (4, 1, 1);
x := (4, 1, 2) is unsat!
x := (4, 1, 3) is unsat!
x := (4, 1, 4) is unsat!
A:= (1, 0, 1, 0, 1); x := (4, 2, 0);
x := (4, 2, 1) is unsat!
x := (4, 2, 2) is unsat!
x := (4, 2, 3) is unsat!
x := (4, 2, 4) is unsat!
x := (4, 3, 0) is unsat!
x := (4, 3, 1) is unsat!
x := (4, 3, 2) is unsat!
x := (4, 3, 3) is unsat!
x := (4, 3, 4) is unsat!
x := (4, 4, 0) is unsat!
x := (4, 4, 1) is unsat!
x := (4, 4, 2) is unsat!
x := (4, 4, 3) is unsat!
x := (4, 4, 4) is unsat!
MiniZinc + z3:
我也想分享这种方法，因为在 MiniZinc 中我只花了 5 分钟 就解决了这个问题，比z3py.
[注意： 对于此任务，我使用 fzn2omt project 中的 fzn2z3.py 脚本。]
文件counter.mzn：（一般问题结构）
include "globals.mzn";
% PARAMETERS
set of int: DOMAIN_A;
set of int: INDEX_SET_A;
set of int: DOMAIN_X = INDEX_SET_A;
set of int: INDEX_SET_X;
% VARIABLES
array [INDEX_SET_A] of var DOMAIN_A: A;
array [INDEX_SET_X] of var DOMAIN_X: x;
% CONSTRAINTS
constraint sum(x) == 6;
constraint forall(i in INDEX_SET_A) (
A[i] = sum(j in INDEX_SET_X)(x[j] == i)
);
% SYMMETRY BREAKING CONTRAINT
constraint increasing(x);
solve satisfy;
(注意:我在这个问题上启用了对称性破坏约束只是为了减少解决方案的数量打印在下面。）
文件counter.dzn：（实例特定数据）
DOMAIN_A = 0..2;
INDEX_SET_A = 0..4;
INDEX_SET_X = 1..3;
找到一个解决方案 z3:
~$ mzn2fzn counter.mzn counter.dzn
~$ fzn2z3.py counter.fzn
x = array1d(1..3, [1, 1, 4]);
A = array1d(0..4, [0, 2, 0, 0, 1]);
----------
找到所有可能的解决方案（仅限 optimathsat）：
~$ mzn2fzn counter.mzn counter.dzn
~$ fzn2optimathsat.py --all-solutions counter.fzn
% allsat model
x = array1d(1..3, [1, 1, 4]);
A = array1d(0..4, [0, 2, 0, 0, 1]);
----------
% allsat model
x = array1d(1..3, [0, 2, 4]);
A = array1d(0..4, [1, 0, 1, 0, 1]);
----------
% allsat model
x = array1d(1..3, [0, 3, 3]);
A = array1d(0..4, [1, 0, 0, 2, 0]);
----------
% allsat model
x = array1d(1..3, [1, 2, 3]);
A = array1d(0..4, [0, 1, 1, 1, 0]);
----------
==========