数値式の解を探したいのですが、それで合金が使用できるかどうか疑問です。Alloyを使用して問題のような線形計画を解くことはできますか？
合金に関する限られた情報を見つけましたが、それはできると思いますが、私には同様の問題の例は見つかりませんでした。
これは確かに簡単ではないので、文章に時間と資金を投入する前に、これが実行可能かどうかを知りたいと思います。
簡略化した例：
(1) a + b = c, (2) a > b, (3) a > 0, (4) b > 0, (5) c > 0
一つの解決策は
a = 2, b = 1, c = 3
あろう合金又は優れたツール/ソリューションのユーザビリティ上の任意の洞察力を大幅に理解されるであろう。
種類：
Paul
合金は、リレーショナル制約ソルバとして特化されています。非常にシンプルな線形プログラミングが可能ですが、代わりにMiniZincのような特殊なツールを使用することをおすすめします。
ダニエル・ジャクソンは数値問題に合金を使用しないようにします。その理由は、合金がSATソルバを使用しており、使用可能な整数の範囲を厳しく制限しているため、これはうまく拡張できません。デフォルトでは、合金は整数に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でした。
合金は2010年頃に開発され、以来、SATソルバと同様に機能するSMTソルバがありますが、数値問題にも対応できます。合金は私が思うそれらのソルバを使用するように作られることができます。言語が信じられないくらいうまく働くといいですね。数字の欠如は本当にミスです。
更新はhttps://github.com/AlloyTools/models/blob/master/puzzle/einstein/einstein-wikipedia.als
で制約のパズルを追加しました