Alloyガール 迷宮編 1の補遺
集合のサイズの制約 vs スコープ指定
僕: 昨日迷路を生成するために書いたモデル、迷路のサイズを指定するために Col と Row のサイズを指定する制約を書いたんだけど…
(...snip...)
// 迷路のサイズ
fun height : Int {
10
}
fun width: Int {
10
}
(...snip...)
run {
#Col = width[]
#Row = height[]
} for 10僕: よく考えてみたら run に与えるスコープの指定でシグネチャのアトムの数が指定できるからこういうふうに書くこともできるんだね
run {} for exactly 10 Row, exactly 10 ColAlloy: 指定がないシグネチャのスコープは 3になるから、サイズに応じた指定が必要。それと exactly 10 Row は Row の atom がちょうど 10個という意味。exactly がないと10個以下という意味になるのでサイズを指定したい時には exactly が必要ね
僕: この2つの書きかたを比べると、スコープで指定するほうが高速に終わるみたいだ。
(Row, Col のサイズ制約版) Executing "Run run$1 for 10" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 136722 vars. 10220 primary vars. 244255 clauses. 12438ms. Instance found. Predicate is consistent. 330ms.
(スコープによる指定版) Executing "Run run$1 for exactly 10 Row, exactly 10 Col" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 136722 vars. 10220 primary vars. 244255 clauses. 12479ms. Instance found. Predicate is consistent. 105ms.
僕: 多分 136722 vars... の行が SAT に変換しているところで、その次が SAT ソルバで制約を充足するインスタンスを探すのにかかった時間だと思うけど、SATへの変換は変数の数は変わってないようだし時間もあまり変化ないね。一方ソルバが解く時間はスコープを使って指定するほうが短いみたいだ
Alloy: 集合のサイズの制約を使うほうでは #Col < width や #Row < height になるような場合も検査した上で棄却するけど、スコープでの指定ではそもそも検査対象にならないから、というところかな
僕: そういうことかなぁ。まあこの例では SAT への変換が時間がかかっているので全体としての影響はあまりないんだけどね
Alloy: これは1つめのインスタンスをみつけるまでの時間だけだから、たくさんのインスタンスの結果を列挙するような場合には次第に影響が大きくなってくるでしょうね
僕: なるほど、じゃあスコープで指定する方法に変えよう
