问题标签 [constraint-satisfaction]

我是 SMT 求解的新手，我正在写信询问一些建议和指示，以了解difficult constraintSMT 求解器真正需要解决的问题，例如 Z3。

我试图调整位向量的长度，例如通过以下方式：

虽然直觉上这可能会导致相当大的搜索空间，但事实证明它Z3仍然做得很好并且可以迅速解决它。

我知道一些加密哈希函数或数学公式（例如，Collat​​z 猜想）可能会使约束求解变得非常困难。但这似乎很极端。另一方面，例如假设我有以下约束：

如何让约束求解器更难求解？有什么通用的方法吗？我的印象是，不知何故，约束变成了“非线性”，那就很难了。但我仍然不清楚它是如何工作的。

==================================

感谢您提供所有友好的注释和有见地的帖子。我非常感激！

因此，根据@usr 的建议，这里有一些试探性的测试：

我有一个任务列表，其中包含持续时间、完成利润和每周最小/最大频率（例如，每周至少阅读 X 本书 3 次）。如果某些任务的完成次数超过了最小频率，那么它们的利润将乘以某个因子（例如 1,5）。

一周中的每一天都有可用于这些任务的小时容量（例如，星期一 - 3 小时，星期二 - 5 小时等）。

我需要在几周内执行任务调度，以达到最大利润并满足所有给定的约束。

我一直在考虑使用一些启发式算法或多个背包问题的解决方案，但这里似乎没有什么真正合适的，我已经完全没有想法了。

您能否告诉我我可以在这里使用什么算法/方法，或者我可以阅读哪些资源来更好地理解问题并找到解决方案？

谢谢

我们拥有巨大的 MAX-CSP 实例，其中包含数百万个变量和约束。

对于任何 CSP 求解器，是否有任何与 Apache Spark 或类似的大数据集成？或者其他一些可用的大数据并行化方式？

如果没有，是否有可能完全并行处理 MAX-CSP？或者也许只在某些条件下使用问题的结构？

找不到任何关于此的信息...反之亦然，通过约束编程管理大数据流程等：-/

此致

亮度

我已经搜索过：

• 所有 CSP 求解器的“Spark”和“大数据”显示在http://xcsp.org/
• 《大数据约束规划》等

这是我目前正在研究的约束满足问题的一个子问题，因此，我省略了应用于变量的额外约束。

假设我们有一个包含 5 个变量的列表，并且说 vars 可以取 1 到 3 之间的值。对称性是这样定义的：假设我们要对所有变量进行 2 个完全赋值。我们还假设对于这些完整分配中的每一个，我们计算具有相同值的变量集。如果我们能找到一种方法，使第一个分配的每个集合在第二个分配中都可以有一个相等/相同的集合，那么这两个分配将是对称的。

这是一个让事情更清楚的小例子：让我们做以下两个作业：

这两个是对称的。让我们也采取以下一个：

这也与 L1 和 L2 对称。

我正在尝试修剪所有对称分配。我如何在约束中表达这一点？

到目前为止，我已经尝试使用约束来找到第一个没有赋值的变量，并且基本上用 #=/2; 锁定它的值。对于每个可能的域值，这都会发生一次。我的代码出现实例化错误，但我不确定我的努力是否真的是解决此问题的有效方法。

我读过弧一致性并不意味着可满足性。提供的示例是

对于具有多个值的域 D。

我的理解是，对于 X 的每个可能值（来自 D），都有 Y 的值（来自同一个 D），以满足上述约束。

有人可以给我一个例子吗？

我想在以下条件下每周每天将 8 个任务列表中的任务随机分配给 4 个人：

• 每个人每天正好有 2 个任务（顺序无关紧要）和
• 不能连续 2 天以上将任务分配给同一个人（一个人第二天不能获得相同的任务）并且
• 不能在同一天向人们分配相同的任务并且
• 一个人一周内不能做超过 2 次相同的任务

这是我一天的代码。但是如何为一周中的 7 天编写代码，强制执行上述条件？

我有一个整数列表

我想找到这个列表的所有排列，这样对于每个排列

1. 元素 0 到 3 加起来为 264，

2. 元素 4 到 7 加起来为 264，

3. 元素 8 到 11 加起来是 264 和

4. 元素 12 到 15 到 264。

目前我有以下策略

1. 使用 itertools.permutations 计算所有排列

2. 检查哪些排列满足我的条件

还有其他性能更好的策略吗？

我正在尝试使用 Python 线性优化库 Pulp 解决杀手数独。

https://en.wikipedia.org/wiki/Killer_sudoku

到目前为止，这是我的尝试，添加了每行必须加起来为 45 的约束。

问题是我正在努力添加一个更严格的约束，即一行中的每个值都必须不同。例如，如果一行有这些值

[1,9,1,9,1,9,1,9,5]

它会通过上面的约束，但不会是有效的数独行，因为每个值都不是唯一的。

下面是我尝试添加更严格的约束，它似乎不起作用，因为问题没有解决

我在网上看到了几个例子，通过将这个优化重新定义为二进制标志的 9x9x9 选择，而不是整数 1-9 的选择的 9x9 优化来解决这个问题。问题是，我发现在 9x9x9 的情况下很难看出如何轻松检查“笼子”的总和，而这在 9x9 的情况下非常简单。

以下是“非杀手”数独的 9x9x9 设置示例。https://github.com/coin-or/pulp/blob/master/examples/Sudoku1.py

我正在寻找（a）找到一种方法来添加这个更严格的约束，即在 9x9 设置中不能重复任何选择，或者（b）一种在 9x9x9 情况下轻松添加笼子“总和”约束的方法。如果你想测试整个笼子约束列表，这里是这个谜题中的笼子约束列表。

https://www.dailykillersudoku.com/search?dt=2020-02-15

这是解决方案https://www.dailykillersudoku.com/pdfs/19664.solution.pdf

编辑 - 如果我尝试使用二元选择更改为 9x9x9 问题，我得到的结果与我想要的笼子约束不匹配。这是一个片段。

这里是完整的例子https://gist.github.com/olicairns/d8e222526b87a62b2e175837b452c24a

前段时间我正在写一篇与 OR 相关的文章以供发表。在文章中，显示了使用 MiniZinc 解决某个优化问题的 MILP 模型。我在 10 个实例中优化了 10 个实例。

顾问对其进行了审查并提到了以下 2 条评论：

1. 在性能方面，您如何将 MiniZinc 与其他最新一代 MILP 求解器（如 CPLEX 或 Gurobi）进行比较？

我一直使用 MiniZinc，它对我来说很有效。我如何展示 MiniZinc 的多功能性？是否有参考书目或证明它的方法？

2. 由于 MiniZinc 不是最著名的 MILP 求解器之一，因此您应该避免在摘要中提及它的名称。

出于什么原因，您不建议在摘要中提及它？

什么是使用 MiniZinc 的有效理由？

我在 python 中应用 CSP 在将字典作为参数传递给 python 中的方法时遇到问题

在列表中传递字典时，它会给出错误unhashable type: 'dict'