问题标签 [constraint-satisfaction]

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

我正在尝试解决无法始终验证约束满足的问题。我可以找到很多关于灵活约束满足的论文，但这并不是我想要的。这是一个例子：

查理正在谈论两个喜欢奶酪的朋友。他最有可能在谈论谁？

我目前将此视为约束满足问题：

是否有处理此类 CSP 的现有方法？

CSP 甚至是解决问题的正确方法吗？

问题陈述：

给定四个单词，将它们放在正方形的 amxn 网格中，使网格的面积尽可能小。

单词必须在网格内从左到右，从上到下运行。字母可以重叠，但不能形成额外的单词。所有的词都必须在一个巨大的链条中相互连接。

可以用 4 个单词“一、二、三和四”组成的示例网格。请注意，最后一个网格是最优化的。

我正在尝试学习 python，我认为这将是一个很好的应用程序。

任何想法如何构建我的数据和算法来解决这样的问题？我不是在寻找一个直截了当的答案，而是一些提示，例如：

使用这个库，或者这个类，或者这个数据结构。或者像这样遍历可用空间。

我正在尝试在 Scheme 中实现回溯搜索。到目前为止，我有以下内容：

我的函数 assignment-complete 和 select-u 通过了单元测试。参数赋值是一个带有 (make-hash) 的哈希表，所以应该没问题。

我相信我遇到的问题与在循环结束时返回 false 有关，如果没有递归返回非 false 值（这应该是有效的赋值）。是否有等效于显式返回语句的方案？

I would like to use the Google or-tools Java api and I can't make disjunction of constraints. I try to implement like this: (A==1 OR B==1) AND ((C==1 OR D==1))... How can I do that?

And the other question is how can I implement the makeSumLessOrEqual(IntVar[] VARS, IntVar limit) because there is only makeSumLessOrEqual(IntVar[] VARS, int limit) function.

Thank you for your help!

我有一个（可满足的）（线性）整数可满足性问题。除其他外，该问题包含一堆布尔值变量，称它们为 x ₁ ...x _n，其中一个约束是 sum(x ₁ ...x _n ) = C。我希望确定哪个这些变量中的一些是固定的，并且所述变量的固定值（如：在所有可能的解决方案中，这些变量中的哪些取特定值（0 或 1，因为它们又是布尔值））。

我有一个可行的解决方案，只是很慢（委婉地说）：

1. _{添加 x 1} == 0的约束
2. 检查问题是否可以解决
3. 删除在步骤 1 中添加的约束。
4. _{添加 x 1} == 1的约束
5. 检查问题是否可以解决
6. 移除第 4 步中添加的约束
7. 断言至少 2 和 5 之一成功。
8. 如果两者都成功，则变量不固定。否则，该变量将固定为问题仍然可以满足的任何约束。
9. _{对 x 2} ...x _n重复 1...8

这样做的问题是它很慢。特别是，它需要解决问题 O(n)，或者更确切地说是 2*n 次。（我传递了以前的解决方案来热启动求解器，但只是启动求解器几乎需要所有时间。）

有没有更快的方法？特别是，需要更少调用求解器的次数？

我正在考虑的事情，不幸的是不能按原样工作，是将它变成一个 ILP 问题并解决它两次，一次以最大化 sum(x 1 ...x n) 为目标，一次以最大化 sum(x ₁ ...x _n ) 为目标最小化相同，并检查哪些变量发生变化。不幸的是，这通常不起作用。对于（反）示例：布尔变量x和y，其中x+y=1。即使两个变量都不是固定的，最大化和最小化也可以产生相同的结果。

我找到了一种使用此链接中描述的方式查找所有解决方案的方法。

这工作正常，但速度很慢。因为它从一开始就重新计算约束，所以 i_e 没有利用以前的计算。

现在，我在这个 链接中看到，有一种更有效的方法可以使用 MiniSat 作为库来查找所有解决方案。但是那里没有描述方法。

您能否为我指出正确的文档以有效地找到所有 SAT 解决方案？

谢谢。

Gecode 使用Spaces 来表示正在进行的约束满足问题：每次到达决策点时，Space都会复制 。

我想对这些正在进行的空间进行分析。有没有办法获得在某个注册的变量、约束、...的列表Space？API 文档似乎没有提供这样的方法。

任何人都可以向我解释 AC-1、AC-2 和 AC-3 算法吗？我必须理解它们并用代码实现它们。但首先，我想很好地理解它们，但它们太难被我理解了。请问有什么帮助吗？顺便说一句，我对回溯不太熟悉，我尝试阅读和观看有关它的视频，但还是一样！谢谢，

我有成对的套装，例如

...并且我想根据已知良好数据自动训练算法，以了解如何将集合成员链接为

...最多为任一集合的每个元素匹配一次。这些集合不必具有相同的大小并且不能保证它们的重叠 - 可能没有匹配，可能所有匹配，可能混合匹配和不匹配。但在许多情况下，预计会有人类可识别的匹配，计算机应该对其进行近似。

到目前为止尝试过

H(a, b, w1, w2, w3)<a1, a2, a3>对来自A和<b1, b2, b3>来自B的一对元组进行评分，f1(a1, b1) * w1 + f2(a2, b2) * w2 + f3(a3, b3) * w3其中f1、f2和f3是手工制作的w1，w2、 和w3是参数化权重。我按分数对所有对进行排序A × B，并取两个成员都没有被更高分数对表示的对。我使用粗略的爬山来训练权重，以便生成的对映射为训练数据的预期。完美的加权配置具有一个阈值，该阈值将正确的t配对分数与不正确的配对分数划定S_ab。对于我大约 800 的训练数据，该算法通常会在数百或数千次迭代后找到完美的配置(A, B)设置总计 2500 对 8-uples（而不是图示的 3-uples）。我还没有给它一个验证数据集来找出这种方法过度拟合的严重程度。

我对问题的集合方面的硬编码处理不满意。我只能想象用于评分对的机器学习技术，但随后的映射是手工制作的，可能不如将集合映射作为一个整体考虑的理想解决方案那么聪明。因为机器学习部分没有考虑整个集合，所以在我看来，它似乎错过了一些可以用来做出更好决策的信息。

我认为我上面的插图可以重构为首先将所有对评分A × B为S_ab = < f1(a1, b1), f2(a2, b2), ..., fn(an, bn) >（对于 n 元组），然后使用[n, ?, 1]神经网络对每个 S_ab 的匹配和非匹配进行训练。这考虑了一对并输出匹配/不匹配，并且不考虑整个集合。

我的理解是神经网络不处理可变大小的输入，尽管也许我可以选择一个上限||A||并||B||找到一些中性编码来填充未使用的节点。并且输出可以是沿着轴索引A沿着侧面和B沿着底部的元素的匹配矩阵，比如说。但是，网络仍然会对元素的顺序敏感，不是吗？

所以 ...

有没有一种机器学习技术可以以这种方式可靠地将集合映射到集合？它以明显的方式与记录链接有关。这是一个约束满足问题，因为每个元素最多可以匹配一次。如果可以将人工对结果的校正作为反馈纳入改进的未来结果，那将是理想的。如果您有办法，请为我​​拼写出来，因为我不精通机器学习概念。