我可以使用Alloy来解决线性编程问题吗？

Question

我想找到一套数值方程的解决方案，我想知道是否可以使用Alloy。

我发现有限的合金信息似乎（至少对我来说）可以做到，但我没有发现类似问题的例子。

这当然不容易，所以在投入时间和文学资金之前，我想知道这是否可行。

简化示例：

(1) a + b = c, (2) a > b, (3) a > 0, (4) b > 0,  (5) c > 0 

一个解决方案是

a = 2, b = 1, c = 3

任何关于Alloy或更好的工具/解决方案的可用性的见解将不胜感激。

亲切的问候，

保罗。

Answer 1

Alloy专门用作关系约束求解器。虽然它可以进行非常简单的线性编程，但您可能需要查看像MiniZinc这样的专用工具。

Answer 2

Daniel Jackson不鼓励使用Alloy来解决数字问题。原因是Alloy使用SAT求解器，因为它严重限制了可用整数的范围，所以它不能很好地扩展。默认情况下，Alloy使用4位作为整数：-8..7。 （这可以使用run命令放大，但当然会减慢找到答案。）不使用数字的思维方式也会影响语法，没有好的数字运算符。即另外是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年左右开发的，从那时起，SMT求解器的工作方式类似于SAT求解器，但也可以处理数值问题。可以使用合金来使用我认为的那些求解器。会很好，因为语言非常好用，缺少数字是一个真正的错过。

更新在https://github.com/AlloyTools/models/blob/master/puzzle/einstein/einstein-wikipedia.als添加了约束谜题