为了解决一组布尔方程,我正在使用以下输入试验Constraint-Programming Solver MiniZinc:
% Solve system of Brent's equations modulo 2
% Matrix dimensions
int: aRows = 3;
int: aCols = 3;
int: bCols = 3;
int: noOfProducts = 23;
% Dependent parameters
int: bRows = aCols;
int: cRows = aRows;
int: cCols = bCols;
set of int: products = 1..noOfProducts;
% Corefficients are stored in arrays
array[1..aRows, 1..aCols, products] of var bool: A;
array[1..bRows, 1..bCols, products] of var bool: B;
array[1..cRows, 1..cCols, products] of var …我有一个问题，可以归结为找到一种将三角矩阵映射到跳过对角线的向量的方法。
基本上我需要使用 Gecode 库来翻译这个 C++ 代码
// implied constraints
for (int k=0, i=0; i<n-1; i++)
for (int j=i+1; j<n; j++, k++)
rel(*this, d[k], IRT_GQ, (j-i)*(j-i+1)/2);
进入这个 MiniZinc（功能）代码
constraint
forall ( i in 1..m-1 , j in i+1..m )
( (differences[?]) >= (floor(int2float(( j-i )*( j-i+1 )) / int2float(2)) ));
我需要找出differences[?].
MiniZinc 是一种函数/数学语言，没有合适的 for 循环。所以我必须映射那些接触上三角矩阵的所有单元格的索引 i 和 j，跳过其对角线，将这些单元格从 0 编号到任意值。
如果这是一个普通的三角矩阵（它不是），解决这样会做
index = x + (y+1)*y/2
我正在处理的矩阵是一个n*n方阵，索引从 0 到 n-1，但最好为n*m矩阵提供更通用的解决方案。
这是完整的 Minizinc 代码 …
锌规格是这样说的：
如果不存在输出项，则实现应以可读格式打印所有全局变量及其值。
然而，这似乎不适用于 minizinc 版本 1.6.0：
G12 MiniZinc 评估驱动程序，版本 1.6.0
我尝试过默认命令 (minizinc) 和 mzn-gecode。
我真的很想避免在输出表达式中重复所有变量名称。我真正想要的是让所有决策变量以某种结构化格式（例如 YAML）输出，但我会选择某种方法来避免这种重复。
澄清一下：我的模型与 CSP 的典型示例不匹配，例如没有大数组或矩阵。它只是一组相当大（相对而言）的单独决策变量。
编辑：创建了错误。
EDIT2：bug 现已在 minizinc 2.0 git 存储库中修复，因此它符合规范。
我试图做出约束，以检查图中是否存在从顶点A到顶点B的路径。我已经做了一个约束，返回了路径本身，但是我还需要一个函数，该函数返回一个布尔值，指示路径是否存在。
我已经花了很多时间，但是我的尝试都没有成功...
有谁知道我该怎么办？
这是我制作的返回路径本身的函数，其中graph是一个邻接矩阵，source和target是顶点A和B：
function array [int] of var int: path(array[int,int] of int: graph, int: source, int: target)::promise_total =
let {
set of int: V = index_set_1of2(graph);
int: order = card(V);
set of int: indexes = 1..order;
array[indexes] of var (V union {-1}): path_array;
var indexes: path_nodes_count; % the 'size' of the path
constraint assert(index_set_1of2(graph) = index_set_2of2(graph), "The adjacency matrix is not square", true); …我正在尝试编写一个与 执行相同操作的谓词circuit，但忽略数组中的零，并且我不断收到以下错误：
MiniZinc: type error: initialisation value for 'x_without_0' has invalid type-inst: expected 'array[int] of int', actual 'array[int] of var opt int'
在代码中：
% [0,5,2,0,7,0,3,0] -> true
% [0,5,2,0,4,0,3,0] -> false (no circuit)
% [0,5,2,0,3,0,8,7] -> false (two circuits)
predicate circuit_ignoring_0(array[int] of var int: x) =
let {
array[int] of int: x_without_0 = [x[i] | i in 1..length(x) where x[i] != 0],
int: lbx = min(x_without_0),
int: ubx = max(x_without_0),
int: len = length(x_without_0),
array[1..len] of var lbx..ubx: …假设我要计算 {1,2,..100} 的 80 个元素子集的数量，使得它们的总和为 3690。
我有以下模型：
array[1..100] of var 0..1: b;
constraint (sum (i in 1..100) (i*b[i])) == 3690;
constraint (sum (i in 1..100) (b[i])) == 80;
solve satisfy;
为了计算解决方案的总数，我运行
$ ./minizinc --all-solutions ~/Documents/code/xmas.mzn > sol.out
$ wc -l sol.out
本质上，我正在打印所有的解决方案并计算它们。有没有一个更简单的 minizinc 语句来代替solve satisfy它让我计算解决方案而不是找到它们？
该MiniZinc约束求解器允许表达基数约束很容易使用内置的sum()功能：
% This predicate is true, iff 2 of the array
% elements are true
predicate exactly_two_sum(array[int] of var bool: x) =
(sum(x) == 2);
满足基数约束，当且仅当布尔变量数组中的真实元素的数量符合指定。布尔值自动映射到整数值0并1计算总和。
我将自己的基数约束谓词实现为一组计数器切片：
% This predicate is true, iff 2 of the array
% elements are true
predicate exactly_two_serial(array[int] of var bool: x) =
let
{
int: lb = min(index_set(x));
int: ub = max(index_set(x));
int: len = length(x);
}
in
if len < 2 then
false …我有兴趣计算一个问题的解决方案数量（不列举解决方案）。为此，我有使用CNF文件的工具。我想转换Minizinc文件（mzn 或 Flatzinc fzn 格式）并将其转换为 CNF。
我了解到Picat能够在加载约束后“转储”CNF 文件。此外，Picat 有一个聪明的模块来解释基本的 Flatzinc 文件。我修改了模块fzn_picat_sat.pi以“转储”CNF 文件。所以，我所做的是使用 mzn2fzn 将 Minizinc 文件转换为 Flatzinc，然后尝试使用我的（稍微）修改过的 fzn_picat_sat.pi版本将其转换为 CNF 。
我想要什么：我希望 Picat 加载 Flatzinc 文件并转储适当的 CNF 文件。如果原来的问题有X个解，我期望对应的CNF有X个解。
会发生什么：我尝试过的大多数 Flatzinc 文件都运行良好。但有些似乎会产生不需要的结果。例如，下面的 mzn转换为这个 Flatzinc 文件。该文件只有 211 个解决方案，但Picat转储的CNF 文件有超过 130k 个解决方案。许多 SAT 求解器可以显示 CNF 文件有超过 211 个解（例如带有选项的cryptominisat--maxsol）。奇怪的是，当我要求 Picat 解决 Flatzinc 文件而不转换为 CNF 时，Picat 确实只找到了 211 个解决方案。问题似乎出在翻译的某个地方。最后，即使 CNF 文件有很多使用 Picat 的解决方案，我也会收到错误 …
我是约束规划和 Minizinc 的新手。我一直在寻找解决这个并不困难的任务的方法，但我什么也没找到。
我想计算数组中出现的不同元素的数量：这是我的数组的声明：
array[1..n,1..n] of var 1..n: countLeft;
我尝试这样做：
constraint
forall(j in 1..n) (
length(array2set([countLeft[i,j]|i in 1..stopCountLeft[j]]) )==left_vision[j]
);
但显然我的数组类型为： array[int]of var opt int 并且不被函数 array2set 接受。
有任何想法吗？
我目前正在研究 MiniZinc，并且我一直在使用 MiniZinc 中集成的两个求解器运行我的模型：Gecode 和 Chuffed。我一直在 IDE 中运行它，但我知道它也可以在 bash 中运行（使用minizinc命令）。
但我想测试我的模型如何使用 Google 的 CP 求解器，称为 OR-Tools。但我真的不知道怎么做。我在 Ubuntu 18.04 中安装了 MiniZinc snap，但我可以下载 MiniZinc 的新目录并在本地运行它，并在那里配置求解器（而不是在 snap 安装中，因为 snap 目录无法修改）。
我需要一种方法来安装 OR-Tools 并使其至少在终端中工作（但从 IDE 运行它会很完美）。
installation solver constraint-programming minizinc or-tools