代码之家 › 专栏 › 技术社区 › Paul

我可以用Alloy来解决线性规划之类的问题吗?

equation-solving alloy

0

Paul · 技术社区 · 7 年前

我想找到一组数值方程的解,我想知道合金是否可以用来解决这个问题。

我发现关于合金的信息有限,似乎(至少对我来说)可以做到这一点,但我没有发现类似问题的例子。

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

简化示例:

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

一种解决方案是

a = 2, b = 1, c = 3

如对合金或更好工具/解决方案的可用性有任何见解,将不胜感激。

谨致问候,

保罗。

2 回复 | 直到 7 年前

1

Peter Kriens 7 年前

丹尼尔·杰克逊不鼓励在数值问题上使用合金。原因是Alloy使用SAT解算器,但由于它严重限制了可用整数的范围,因此无法很好地进行缩放。默认情况下,Alloy使用4位表示整数:-8。。7.(这可以通过run命令进行放大,但当然会减慢找到答案的速度。)不使用数字的心态也影响了语法,数字没有很好的运算符。一、 e.加法为5。加上【6】。

也就是说,您的问题如下所示:

pred f[a,b,c : Int] {
    a.plus[b] = c 
    a > b
    a > 0
    b > 0
    c > 0 
}

run f for 4 int

答案可以在evaluator或文本视图中找到。我得到的第一个答案是 a=4, b=1, c=5 .

Alloy是在2010年左右开发的,从那时起,SMT解算器的工作方式与SAT解算器类似,但也可以处理数值问题。我认为可以用这些溶剂制造合金。这会很好,因为语言非常好用,缺少数字是一个真正的失误。

使现代化 添加了一个约束难题 https://github.com/AlloyTools/models/blob/master/puzzle/einstein/einstein-wikipedia.als

2

0

Hovercouch 7 年前

Alloy专门用作关系约束解算器。虽然它可以做非常简单的线性规划,但您可能希望看到一个专门的工具,如 MiniZinc 相反