标签: constraint-programming

我有一个非常简单的方程，我希望能够在序言中解决：

A = B + C

我希望能够编写一个表达这种关系的谓词，它可以处理任何一个未被实例化的参数。无需推广到更复杂的关系或方程。

myEquation(A, B, C) :-
...something...

我可以使用以下语义调用：

myEquation(A,1,2).
>    A = 3.
myEquation(3,B,2).
>    B = 1.
myEquation(3,1,C).
>    C = 2.

有任何想法吗？使用算术运算符会产生很多“参数未充分实例化”的错误。看起来求解任意方程组超出了大多数 prolog 实现的范围，但我希望这个极其简单的方程易于处理。

该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 的解决方案，我也会收到错误 …

我正在重新使用 Google 的 OR 工具并尝试（相对）简单的优化。我正在使用 CP SAT 求解器，但我可能在这里遗漏了一些基本内容。我有一些变量 x、y 和一些常量 c。如果 y 小于 c，我希望 x 等于 1，否则等于 0。

from ortools.sat.python import cp_model

solver = cp_model.CpSolver()
model = cp_model.CpModel()
c = 50
x = model.NewBoolVar(name='x')
y = model.NewIntVar(name='y', lb=0, ub=2**10)

model.Add(x == (y < c))

model.Maximize(x+y)

status = solver.Solve(model)

我收到一条错误消息

TypeError: bad operand type for unary -: 'BoundedLinearExpression'

看来我在这里滥用 OR 工具语法来限制我的约束。我很难理解在线 OR 工具的文档，而且我似乎忘记的东西比我想象的要多得多。

我需要找到所有 16 位数字 ( x, y, z) 的三元组（实际上只有在不同三元组中与相同位置的位完美匹配的位），这样

y | x = 0x49ab
(y >> 2) ^ x = 0x530b
(z >> 1) & y = 0x0883
(x << 2) | z = 0x1787

直接使用 8700K 的策略需要大约 2 天，这太多了（即使我会使用我可以访问的所有 PC（R5-3600、i3-2100、i7-8700K、R5-4500U、3xRPi4、RPi0/W）这将花费太多时间）。

如果位移位不在等式中，那么这样做将是微不足道的，但是使用位移位很难做同样的事情（甚至可能是不可能的）。

所以我想出了一个非常有趣的解决方案：将方程解析为关于数字位的语句（类似于“x XOR 的第 3 位 XOR y 的第 1 位等于 1”），并且所有这些语句都用 Prolog 语言之类的语言编写（或只是解释他们使用真值表操作）执行所有明确的位将被发现。这个解决方案也很困难：我不知道如何编写这样的解析器，也没有 Prolog 的经验。(*)

所以问题是：这样做的最佳方法是什么？如果是 (*) 那么怎么做呢？

编辑：为了更容易在此处编码数字的二进制模式：

0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111

在阅读约束逻辑编程时,我不禁注意到与SQL编程的明显关系.SQL是否是"约束逻辑编程"的一个例子？

我想知道如何解决一个未知的基本线性方程.

我尝试通过字符串拆分来实现它以获得解决方程所需的一切,但我确信有更好的方法.

solve(5 + X = 10).
X = 5.
solve(5+8 = Ans).
Ans = 13.

这是我想要解决的问题.我想用solve/1.

先感谢您.

I am currently evaluating googles or-tools and just noticed that it's not really a solver on its own but mainly an interface to other solvers. What I'd like to know is which solvers this framework uses for constraint and routing problems.

I have already looked thoroughly through https://developers.google.com/optimization/, but only found that

• for linear optimization Google's "in-house, open-source GLOP" is used
• for network flow optimization an own solver seems to be used ("OR-Tools provides several solvers for network flow …

我正在使用ORTOOLS库来解决 VRP 问题。我给它一个初始可行的解决方案来解决我的问题，满足我的问题的所有约束，但不是最优的。然后 ORTOOLS 执行 GUIDED_LOCAL_SEARCH 启发式，不断扰乱我的解决方案的一部分（有时可能使其不可行），直到它有望达到比我的初始解决方案更好的解决方案。

为什么要使用约束规划求解器？我的理解是，经典的约束规划从一个不可行（可能为空）的解决方案开始，传播约束以缩小我的变量的域，直到达到静止状态，然后做出决定。然后它再次迭代，直到解决问题或在到达死胡同时回溯（想想数独）。

在进行小扰动时，这些能力（传播、回溯）以什么方式需要？

我目前正在研究 MiniZinc，并且我一直在使用 MiniZinc 中集成的两个求解器运行我的模型：Gecode 和 Chuffed。我一直在 IDE 中运行它，但我知道它也可以在 bash 中运行（使用minizinc命令）。

但我想测试我的模型如何使用 Google 的 CP 求解器，称为 OR-Tools。但我真的不知道怎么做。我在 Ubuntu 18.04 中安装了 MiniZinc snap，但我可以下载 MiniZinc 的新目录并在本地运行它，并在那里配置求解器（而不是在 snap 安装中，因为 snap 目录无法修改）。

我需要一种方法来安装 OR-Tools 并使其至少在终端中工作（但从 IDE 运行它会很完美）。