问题标签 [constraint-programming]

嗨，我需要一个非确定性约束满足问题工具，因为我需要具有相同问题输入的不同解决方案。有人知道具有这种特性的工具吗？

我只知道像 Gecode (c++)、Choco (Java) 和 Curry (Haskell) 这样的工具，我认为它们以确定性的方式工作。

请有人帮我解决这个错误谢谢，我使用 JaCoP 库，这是一个传输问题，我需要找到 OptimalSearch 它的约束编程

http://pastebin.com/ZV4j234S示例类

http://pastebin.com/at7nfAwE传输类

我有一个如图所示的网状网络。现在，我正在为这个 sat 网络中的所有边分配值。我想在我的程序中提出，我的分配中没有闭环。例如，左上角最正方形的约束可以写成 -

E0 = 0 or E3 = 0 or E4 = 0 or E7 = 0，因此任何一个链接都必须处于非活动状态才能不形成循环。然而，在这种网络中，存在许多可能的环路。

例如由边缘形成的循环 - E0, E3, E7, E11, E15, E12, E5, E1。

现在我的问题是我必须描述这个网络中可能发生的每个可能的循环组合。我试图在一个可能的公式中编写约束，但是我无法成功。

如果有可能的方法来编码这种情况，任何人都可以抛出任何指针吗？仅供参考，我正在使用 Z3 Sat Solver。

对于我的计算机科学研究课程，我必须提出一组约束和分数定义，才能找到用于频繁项集挖掘的平铺。包含数据的矩阵由 1 和 0 组成。

我的任务是提出一组用于平铺的约束（具有固定数量的平铺），以及需要最大化的得分函数。由于我开始制定允许重叠图块的解决方案，因此我试图找到一个得分函数来计算所有图块的总“面积”。请记住，必须针对每个可能的解决方案评估得分函数，因此我不能简单地查看整个矩阵（包含大约 100k 个元素）并查看它是否是图块的一部分。但是，我只考虑了 2 个图块之间的重叠，并得出以下结论：

TotalArea = Sum_a_in_Tiles(Area(a)) - Sum_a/b_in_tiles(Overlap(a,b))

愚蠢的我，我没有考虑3个瓷砖之间可能的重叠。我的问题如下：是否可以为 n 个图块提出一个通用的得分函数，只考虑每个图块的面积和 2 个（或更多）图块之间的每个重叠面积，如果是这样，我将如何编程？

我可以提供一些代码，但又必须用一种叫做 Comet 的晦涩语言进行编程 :(

有哪些已知算法（或查找算法的资源）可以在约束满足问题中找到最大化分配变量数量的分配（如果不存在令人满意的分配）？

因此？

我的问题发生的用例上下文

我定义了一个三角形的 3 个随机项。Microsoft Z3 应输出：

• 约束是否满足或是否有无效的输入值？
• 所有其他三角形项目的模型，其中所有变量都分配给具体值。

为了约束我需要assert三角形等式的项目 - 我想从勾股定理（(h_c² + p² = b²) ^ (h_c² + q² = a²)）开始。

问题

我知道 Microsoft Z3 解决非线性算术问题的能力有限。但即使是一些手动计算器也能够解决这样一个非常简化的版本：

问题

• 如果给出两个值，有没有办法让 Microsoft Z3 解决勾股定理？
• 或者：是否有另一个定理证明器能够处理这些非线性算术的情况？

感谢您对此的帮助 - 如果有任何不清楚的地方，请发表评论。

我需要在 Java 或 .NET 中对约束满足 (CSP) 问题进行建模。该问题需要表示变量的层次结构。所以树的每个节点都是一个变量。

例如，如果变量 C1 是另一个变量 C2 的子变量，并且如果 C1 为真，那么 C2 应该为真，因为它是他的父变量。同时，如果一个分支中的一个变量节点为真，这意味着其他分支中的所有变量都是假的，因为在层次结构中只能选择一个分支。

我如何将其表示为 CSP 问题，我可以在 Java 或 .NET 中使用哪个工具？

我必须对其进行编辑以提供更多详细信息，因为还有更多：

在我的问题中，有 2 个部分：在第 1 部分中，有一个最大化函数 q1*x1+q2*x2+q3*x3.. 其中 qi 是系数（实数），xi 是变量（可以是 0或 1) 我必须选择一些最大化此功能的 xi。换句话说，节点只能是 0 或 1，我必须通过从层次结构中选择一个节点来最大化这个功能。

同样，这些 xi 变量是树的节点，所以当我选择一些 xi 时，它们必须来自树的同一分支，并且一次只能选择 1 个分支。因此我需要表示这些分层约束（第二部分）。最好的办法是将所有内容都表示为 lp 问题，但我不知道如何表示具有线性规划约束的树。

我不知道我是否可以同时使用最大化问题（第一部分）并施加 CSP 约束（而不是使用 LP 约束）。

我想问一下，如何将以下 Z3 约束转换为 Z3py（Python API）。

在下面的工作示例中，我试图检索匹配的模型，在这种情况下有两个令人满意的模型：

和

问题是重复匹配的模型，直到运行求解器超时。如何在不重复的情况下检索满意的模型。

非常感谢，

我无法让 z3 与 Python 一起工作。我正在运行 Windows 7 64 位。我已经下载了 64 位 Python 3.3.0 和 64 位 z3 4.3.0。我已经更新了我的 PATH 和 PYTHONPATH 以包含 z3 \bin 目录。但是，当我尝试在 python 中使用 z3 时，出现以下错误：

from z3 import * Traceback（最近一次调用最后一次）：文件“”，第 1 行，在 ImportError 中：'z3' 中的坏幻数：b'\x03\xf3\r\n'

有谁知道出了什么问题以及如何解决？

谢谢