假设我有两个变量a和b。我想定义它们之间的以下关系/约束：
- a=1，b%12=1或b%12=0
- a=2，b%12=0
一些解决方案是
- a=1，b=1
- a=1，b=12
- a=2，b=12
我目前正在以一种简单的方式对此进行建模(并在顶部添加一个额外的条件(：
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的值，反之亦然。
根据您的评论，使用整数似乎不必要地使约束复杂化。
如果你需要坚持"；数字"；出于其他原因，我建议全局断言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(向下滚动到谈论"枚举"的部分。(
你没有告诉我们八度音阶/音符在你的系统中是如何相互约束的；但使用八度音阶并返回可能音符的常规函数应该很容易捕捉到它们。你应该发布人们可以运行的实际代码，这样他们就可以看到瓶颈是什么