世界一難しい数独＠Alloy(cont'd)

Alloy 数独

下記のような記事を見つけた。

  星11個の数独の問題をAlloyで

なんと以前の記事を見てdisktnkさんという方が「遅すぎる」と検証してくださったようだ。。。

Lets's Compare!

ぼくの実行結果

Executing "Run run$1 for 13"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   77305 vars. 2201 primary vars. 146903 clauses. 3635ms.
   . found. Predicate is consistent. 82243ms.

disktnkさんの実行結果

Executing "Run game"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   2725 vars. 729 primary vars. 3303 clauses. 508ms.
   . found. Predicate is consistent. 2681ms.

なんだこの複雑度の差は、、、、述語数が30～40倍くらいちがう。僕の実行環境がNetbookでバカ遅いという状況をはるかに超えている。。。たしかに余計な述語が多かったんだよな。

精進します。