一般注意事项：
给定一个值赋值(x1, x2, x3) = (v1, v2, v3)，(v1, v2, v3) 的任何排列也是问题的解决方案。在某些情况下，通过要求 ∀ i, j.((i < j) => (x_i <= x_j)) 来打破搜索空间中的对称性可能会很方便。
更容易将每个位置A_i 视为所有x_j 的编号，并赋值为i。
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]);
----------
==========