我想为一组数值方程找到一个解，我想知道合金是否可以用来解决这个问题。
我发现关于合金的有限信息似乎表明（至少对我而言）可以做到，但我没有发现类似问题的示例。
这当然不容易，所以在投入时间和金钱于文学之前，我想知道这是否可行。
简化示例：
(1) a + b = c, (2) a > b, (3) a > 0, (4) b > 0, (5) c > 0
一个解决方案是
a = 2, b = 1, c = 3
我们将不胜感激有关 Alloy 的可用性或更好的工具/解决方案的任何见解。
亲切的问候，
保罗。
【问题讨论】：
Daniel Jackson 不鼓励使用 Alloy 解决数字问题。原因是 Alloy 使用了 SAT 求解器，并且它不能很好地扩展，因为它严重限制了可用整数的范围。默认情况下，Alloy 使用 4 位表示整数：-8..7。 （这可以用 run 命令扩大，但当然会减慢寻找答案的速度。）不使用数字的心态也影响了语法，没有好的数字运算符。 IE。加法是 5.plus[6]。
也就是说，您的问题看起来像：
pred f[a,b,c : Int] {
a.plus[b] = c
a > b
a > 0
b > 0
c > 0
}
run f for 4 int
答案可以在评估器或文本视图中找到。我得到的第一个答案是a=4, b=1, c=5。
Alloy 是在 2010 年左右开发的，从那时起就出现了与 SAT 求解器类似的 SMT 求解器，但也可以处理数值问题。我认为合金可以使用那些求解器。会很好，因为该语言非常好用，缺少数字是一个真正的失误。
更新在https://github.com/AlloyTools/models/blob/master/puzzle/einstein/einstein-wikipedia.als添加了一个约束拼图
【讨论】：
Alloy 专门用作关系约束求解器。虽然它可以进行非常简单的线性编程，但您可能需要查看像 MiniZinc 这样的专用工具。
【讨论】：