问题标签 [constraint-satisfaction]

我正在研究Java 6 ^*1)的源到源转换器。

我需要维护负面信息和正面信息，所以我必须为变压器实施小约束系统。约束系统是一种受限的CNF 公式，可以定义如下：

(v1 == c1 /\ v2 == c2 ... vn == cn) /\ ((w1,1 != d1,1 \/ w1,2 !== d1,2 ... w1,k != d1,k) /\ (w2,1 != d2,1 \/ ...) /\ ... (wm,1 != dm,1 \/ ... \/ wm,k != dm,k))

哪里vi == ci是等式约束（替换，变量赋值），

wj != dj,l是不等式约束，

vi, wj,l是变量，

ci, dj,l是常数（文字）。

常量类型是映射到整数的 Java 原始类型和引用类型。常量也是任意的类似 AST 的结构（代表部分评估的表达式，可能包含（元）变量）。

约束系统的工作原理如下：

当转换器达到条件（例如if(x == c) then b else b1）时，约束x == c被添加到then分支的约束系统中，而约束又被添加到else分支的约束系统（公式）中。x != c

因此，then分支的新公式为：（公式的x == c /\ formula正部分为等式的合取）；

else分支的新公式是：（公式的x != c \/ formula负部分是不等式析取的合取）。

编辑：约束系统的可满足性。

为了使约束系统可满足，必须可以为系统中的变量分配值以使约束得到满足。

因此，如果存在替代Theta则满足约束系统，使得对于每个方程Theta在句法上与Theta相同，同样，对于每个不等式Theta在句法上与Theta不同。 v = c vcw != d wd

不幸的是，我对约束编程很陌生，遇到了问题。

1. 在这种情况下，我并不完全清楚如何将 AST 常量映射到整数。我应该简单地使用常量数组的索引还是一些哈希函数？

2. 目前尚不清楚如何处理长类型。重写基于 int 的求解器使其基于 long 或使用浮点求解器？

3. 也不清楚如何处理组合的整数和浮点数据。我意识到直接的解决方案是使用浮点求解器来处理整数和浮点约束。这是真的吗？或者我可以分别解决约束的浮点和整数部分？

请问，有人可以帮我吗？一些方向，提示...

¹⁾目前，source=8 / target=8方案已被接受。

我正在尝试阅读约束满足问题并尝试对其进行编码以解决一些示例问题。我遇到了http://rosettacode.org/wiki/Zebra_puzzle#C.2B.2B来解决经典的斑马难题。在rosetta code website给出的C代码中，有以下功能。我只给出了几行。我不知道这两个if语句的目的是什么以及它们是如何工作的。有人可以解释一下吗？

想象一下它是公元前 3000 年，我们正在建立一些异性恋、一夫多妻制的快速约会。有n_c男有n_s女（n_s > n_c）。快速约会将分n_r轮进行。在每一轮中，每个男人都会遇到一个女人。所以n_r*n_c插槽要填补。

此外，他们都填写了石碑问卷，我们从中构建了一个评分函数 ， 它给出了在其中一个插槽u(i,j)中配对男人i和女人的效用。j

目标是最大化所有时段的得分总和，在此约束条件下，没有男人会遇到同一个女人超过一次，并且每个女人最多会遇到 ceil(n_r*n_c/n_s) 男人。（也就是说，每个女人应该与大约相同数量的男人见面。）

你能画出一个算法来解决这个问题吗？可以假设男性和女性的数量在 100 人以下，可能在 50 人以下。哦，假设我们将现代硬件带到了公元前 3000 年。

在 Minizinc 中，是否可以对域进行采样？假设我的域有很多解决方案，运行 --all-solutions 最初会返回非常相似的解决方案。

1）有没有办法对域进行采样？也许是 BFS ？目的是进行后续解决方案分析。

2) 有什么方法可以估计 CP 中的搜索域大小吗？

我的域是员工排班问题

问候，H

在将弧一致性（AC3）算法应用于一个约束满足问题中，如果一个变量的域为空，下一步是什么？

解决方案（4）。我认为（1）是正确的，因为这意味着我们找不到任何一致的分配并停止。任何人都可以描述为什么（4）是真的？

您应该何时停止扩展 CSP 规划师的视野？具体来说，是否存在约束满足问题规划器的条件，即当与搜索的弧一致性在某个范围内失败时，意味着弧一致性在所有更长的范围内也将失败。

我必须断言值 val1 >= val2。也就是说，就模型检查而言，见证人（反例）必须断言 val1 >= val2。

我可以通过以下方式在 C (cbmc) 中轻松完成：

有没有办法在 Python 中做到这一点？

更新：

导致

但如果我这样做

结果与我想要的相反（我想要 val2 >= val1）。 编辑：

根据选择的 z 和 r 的值，这将中断或通过并打印 x ， y。所以这不像 __CPROVER_assert 那样工作，它找到了一个有效/满意的见证/解释！

例如，我对相同代码的三个不同运行结果为：

有什么方法可以检查 Python 中约束的可满足性。

为什么弧一致性算法复杂度为 O(cd ³ )？

我想使用 Optaplanner 建模和解决的问题是为运动队（这里：足球）创建一个花名册。即：从所有可用的玩家中，根据几个标准选择11个。我正在使用硬/中/软分数来定义有效的解决方案，例如，指定一个守门员必须出现在名单中的硬标准。选择球员的顺序无关紧要。

我目前将此作为我的PlanningEntity：

对于我只使用的分数计算getMembers，即我不在乎玩家是否被分配到member1或member2。求解器主要使用默认配置，并配置为在 100 秒后超时，或者在 10 秒后未实现任何改进。

在一些示例数据集上玩过这个之后，我注意到求解器在大多数情况下都没有找到最佳解决方案（但至少是有效的），例如没有选择最好的守门员（这通常很容易看到，因为有可用的不多，应该选择一个）。

我怀疑这与我建模的方式有关PlanningEntity：由于所有名册成员都可以单独设置，这似乎使解决方案空间不必要地变大。如前所述，将成员分配到哪个字段并不重要。重要的是（或者更确切地说，谁）被分配，谁没有被分配。所以我基本上需要在满足一些约束和优化标准的同时选择一部分玩家。

List of RosterMember然而，简单地将s注释为@PlanningVariable似乎不起作用。我在示例中也找不到类似的情况。我想这应该是一个简单的建模示例？

到目前为止，我能想到的唯一想法是明确地对一些（硬）约束进行建模，例如将范围限制goalkeeper为恰好一个规划变量，同时将所有其他变量限制为non-goalkeeper（甚至可能更远）。根据文档（4.3.5.2.3.），应该避免这种情况。

编辑：我只有一个名册实例。我假设不同团队的花名册不相关，并计划按顺序为每个团队运行求解器。

编辑2：按照建议，我现在有了这个而不是以前的Roster：

在创建初始未解决的解决方案时，我添加了 11 个空的 RosterAssignments。但是，在创建启动解决方案后，求解器似乎无法改进任何东西：

由于棘手的约束满足问题通常被认为是 NP 完全问题，那么 NP 完全约束满足问题的 Big-O 最坏情况运行时间是多少？