模数约束传播答案

【问题标题】：Constraint propagation with modulo模数约束传播
【发布时间】：2021-07-10 05:11:08
【问题描述】：

假设我有两个变量 a 和 b。我想在它们之间定义以下关系/约束：

一些解决方案是

我目前正在以一种简单的方式对此进行建模（并在顶部添加一个额外的条件）：

rhs = Or(
  And(a == 1, Or(b % 12 == 1, b % 12 == 0)),
  And(a == 2, Or(b % 12 == 0))
)
lhs = And(b > 10)
solver.add(Implies(lhs, rhs))

但是，随着我增加变量和约束的数量，这会变得非常慢。

有没有更好的建模方法？也许是一个功能？但我希望允许搜索“双向”运行，即给定 b 的值，我们应该能够识别 a 的值，反之亦然。

【问题讨论】：

除法和模数对于 SMT 求解器来说总是很困难。可能有更好的编码，但如果不看到更多细节就很难说。如果您清楚自己要在高层次上解决什么问题，则堆栈溢出效果最好，因此此处需要更多详细信息以获得更好的答案。另外，请注意 XY 问题：en.wikipedia.org/wiki/XY_problem.
感谢您的回复。我本质上是在尝试使用 Z3 作为约束求解器。这个特殊的问题是一个音乐 CSP，所以 a 是一个和弦，b 是一个音符，它们相互约束。模数归一化八度音阶，例如对于某些和弦，我们可以有音符 i 或 i+12（一个八度音程）或 i+24 等。我还尝试用所有可能音符的析取替换模数，但这并没有更快。

标签： z3 z3py

【解决方案1】：

根据您的评论，使用整数似乎不必要地使您的约束复杂化。

如果您出于其他原因需要坚持使用“数字”，那么我建议全局断言 0 <= b 和 b < 12（代表所有 12 个音符），这可以帮助求解器减少搜索空间。然而，除法/模数对于 SMT 求解器来说总是很困难，但也许您根本不需要它们：事实上，我建议首先不要使用数字来表示音符。而是使用枚举：

Note, (A, B, C) = EnumSort('Note', ('A', 'B', 'C'))

（我只写了上面的前三个，剩下的9个你可以添加。）

这非常清楚地向求解器传达了您正在处理的不同项目的有限集合。您还应该考虑将八度音程表示为某种枚举类型，或者至少将其限制在某个小范围内，涵盖我假设您感兴趣的前 6-7 个八度音程。

您可以在此处阅读有关 z3 中枚举的更多信息：https://ericpony.github.io/z3py-tutorial/advanced-examples.htm（向下滚动到讨论“枚举”的部分。）

您还没有告诉我们八度音阶/音符在您的系统中是如何相互约束的；但是使用八度音阶并返回可能的音符的常规函数应该很容易捕获它们。您应该发布人们可以运行的实际代码，以便他们了解瓶颈是什么。

【讨论】：