| 4 | 3 | 3 | 3 | |||
| 2 | 4 | |||||
| 3 | 3 | 3 | ||||
| 2 | 8 | 4 | ||||
| 1 | 3 | |||||
| 1 | 4 | 1 |
なお，以下ではパズルの盤面の一番上の行を第0行， 一番左の列を第0列として数えます．
たとえば，節点n_0_0から下への辺v_0_0および 右への辺h_0_0の宣言は以下のようになります．
(int v_0_0 -2 2) ; n_0_0からn_2_0への辺
(int h_0_0 -2 2) ; n_0_0からn_0_2への辺
他の辺を表す変数についても同様に宣言します．
たとえば，数字8の書いてあるn_4_3の節点について考えます． この節点につながる辺は， v_4_3 (下への辺), h_4_3 (右への辺), v_2_3 (上への辺), h_4_0 (左への辺)の4つです． それぞれの橋の本数は，絶対値関数absで求めることができますから， 以下のような制約条件となります．
(= (+ (abs v_4_3) (abs h_4_3) (abs v_2_3) (abs h_4_0)) 8)
他の数字についても同様に制約条件を記述します．
たとえば， v_1_1 (数字2のn_1_1の節点から下への辺)と h_2_0 (数字3のn_2_0の節点から右への辺)とは 交差してはいけません．すなわち，少なくともどちらかの値が0となります． これを制約条件として書くと以下のようになります．
(or (= v_1_1 0) (= h_2_0 0))
他の交差する可能性のある辺の組み合わせについても同様に記述します．
「ましゅパズルをSugar制約ソルバーで解く」や 「スリザーリンク・パズルをSugar制約ソルバーで解く」の 時は， つながっている部分(グラフ理論では，連結成分といいます)のそれぞれについて， 節点に番号を付けることによって始節点を決めることができました．
「橋をかけろ」の場合も同様に考えることができます．
まず，各連結成分は，辺の向きをうまく選べば， Rooted DAG (Rooted Directed Acyclic Graph)にできます． Rooted DAGとは....，ちゃんとした説明は面倒ですね...
では，こうしましょう．各橋が伸縮自在なゴムでできていると想像してください． また，どれかの数字をつまんで，紙から持ち上げることができると考えてください． 持ち上げた数字につながって，橋や他の数字も持ち上がります．
その時，持ち上げた全体がRooted DAGになっています! つまんでいる数字が根(root)の節点で， 各辺は上の数字から下の数字に向いているとすれば， 向きに沿って辺をたどっていってもループが存在しないのでacyclicですね．
各連結成分をRooted DAGにできれば， 「根の節点がちょうど1つ」という条件により，連結成分を一つにできます．
そこで，まず以下の変数を用意します．
(int z_0_0 1 17)
(int r_0_0 0 1)
さらに，
z_0_0が1に等しい時だけr_0_0が1に等しくなるという条件を
加えます．
(iff (= z_0_0 1) (= r_0_0 1))
他の節点についても同様にします．
次に，すべてのr_i_jの和が1に等しいという条件を加え， 「根の節点がちょうど1つ」すなわち「全体がつながっている」という条件を表します．
(= (+ r_0_0 r_0_2 ... r_6_5) 1)
(=> (> v_4_3 0) (< z_4_3 z_6_3))
(=> (> h_4_3 0) (< z_4_3 z_4_5))
(=> (< v_2_3 0) (< z_4_3 z_2_3))
(=> (< h_4_0 0) (< z_4_3 z_4_0))
(=> (= r_4_3 0) (or (< v_4_3 0) (< h_4_3 0) (> v_2_3 0) (> h_4_0 0)))
s SATISFIABLE a v_0_0 2 a h_0_0 2 a h_0_2 1 a v_0_4 0 a h_0_4 2 a v_0_6 1 a v_1_1 0 a h_1_1 -2 a v_1_5 -2 a v_2_0 0 a h_2_0 1 a v_2_3 2 a h_2_3 0 a v_2_6 2 a h_4_0 -2 a v_4_3 2 a h_4_3 2 a v_4_5 0 a h_5_4 -1 a h_6_1 -1 a h_6_3 1 a z_0_0 1 a r_0_0 1 a z_0_2 12 a r_0_2 0 a z_0_4 13 a r_0_4 0 a z_0_6 14 a r_0_6 0 a z_1_1 17 a r_1_1 0 a z_1_5 16 a r_1_5 0 a z_2_0 12 a r_2_0 0 a z_2_3 13 a r_2_3 0 a z_2_6 15 a r_2_6 0 a z_4_0 17 a r_4_0 0 a z_4_3 14 a r_4_3 0 a z_4_5 15 a r_4_5 0 a z_5_4 17 a r_5_4 0 a z_5_6 16 a r_5_6 0 a z_6_1 17 a r_6_1 0 a z_6_3 16 a r_6_3 0 a z_6_5 17 a r_6_5 0 aSugarの次期リリースには， 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です． 以下は，その実行例です．
$ ./hashiwokakero.pl data/hashiwokakero-0.txt >csp/hashiwokakero-0.csp
$ /usr/bin/time sugar csp/hashiwokakero-0.csp >log/hashiwokakero-0.log
0.98user 0.11system 0:00.91elapsed 119%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+176outputs (2major+9809minor)pagefaults 0swaps
$ ./hashiwokakero.pl -s log/hashiwokakero-0.log data/hashiwokakero-0.txt
; Hashiwokakero Puzzle
; # http://www.nikoli.co.jp/en/puzzles/hashiwokakero/
; size 7 7
; 4 - 3 - 3 - 3
; - 2 - - - 4 -
; 3 - - 3 - - 3
; - - - - - - -
; 2 - - 8 - 4 -
; - - - - 1 - 3
; - 1 - 4 - 1 -
4 === 3 --- 3 === 3
# 2 ========= 4 |
3 ------ 3 # 3
# # #
2 ====== 8 === 4 #
# 1 --- 3
1 --- 4 --- 1
; END
以下は，
Nikoli: 橋をかけろのおためし問題中の
おためし問題10 (32x18)をLet's Note CF-W5で解いた結果です(MiniSat2を使用)．
10秒程度で解けています．
$ ./hashiwokakero.pl data/hashiwokakero-10.txt >csp/hashiwokakero-10.csp
$ /usr/bin/time sugar csp/hashiwokakero-10.csp >log/hashiwokakero-10.log
9.38user 0.31system 0:06.98elapsed 138%CPU (0avgtext+0avgdata 0maxresident)k
21120inputs+8272outputs (103major+30910minor)pagefaults 0swaps
$ ./hashiwokakero.pl -s log/hashiwokakero-10.log data/hashiwokakero-10.txt
; Hashiwokakero Puzzle
; # http://www.nikoli.co.jp/en/puzzles/hashiwokakero/
; size 32 18
; 3 - 3 - 4 - 3 - - - 4 - 3 - - 3 - 4 - - 3 - 4 - - 1 - 3 - 3 - 2
; - 2 - 3 - 5 - - 3 - - 2 - 4 - - 1 - 2 - - 3 - 2 - - 3 - 3 - 2 -
; 2 - - - 1 - - - - - 3 - 1 - 2 - - 5 - 1 - - 1 - 1 - - 1 - - - -
; - 3 - 1 - - 2 - 3 - - 2 - 3 - - 1 - - - - 4 - 3 - 1 - - - 2 - 4
; - - - - - 2 - 3 - - 4 - - - - - - 2 - 1 - - - - - - 3 - 5 - 1 -
; 1 - 3 - 4 - 4 - - 4 - 1 - - 3 - 5 - 2 - - 5 - - 3 - - - - 1 - 4
; - 1 - - - - - - - - 2 - - 3 - - - 2 - - 1 - - 2 - 4 - - 6 - 3 -
; 4 - 5 - - 1 - 2 - 6 - - 1 - 1 - - - - 3 - 3 - - 1 - 1 - - - - 3
; - 2 - - 3 - 4 - 1 - - 3 - 4 - - 5 - - - 2 - - 5 - - - 1 - - 2 -
; 2 - 2 - - 3 - 2 - - - - 3 - - 1 - 4 - 6 - - 2 - 3 - 2 - 3 - - 4
; - 3 - - 3 - 2 - - 4 - 3 - - - - - - 1 - 1 - - - - 2 - 4 - - 2 -
; - - - 1 - 3 - - 5 - - - 5 - 3 - 4 - - 2 - - - 2 - - 3 - - 2 - 3
; 3 - 2 - - - - 2 - - 3 - - 2 - - - 1 - - - - 4 - 3 - - - - - - -
; - - - - 3 - 2 - 2 - - 3 - - 3 - 4 - 5 - 3 - - 1 - - 4 - 3 - 4 -
; 3 - - 5 - 4 - 5 - - 4 - - - - - - - - 1 - - 4 - - 2 - 3 - 1 - 3
; - - - - - - - - 1 - - 3 - 2 - - 2 - 4 - - 4 - - 4 - 3 - - - 1 -
; 3 - 2 - - 1 - 1 - - - - - - 3 - - 3 - 1 - - - - - 1 - 4 - 2 - 2
; - 2 - 3 - - 2 - 4 - 5 - - 4 - 1 - - 2 - - 3 - - 3 - 3 - 3 - 2 -
3 --- 3 === 4 === 3 --------- 4 === 3 ------ 3 === 4 ------ 3 === 4 ------ 1 3 === 3 --- 2
# 2 --- 3 === 5 ====== 3 | 2 === 4 ------ 1 | 2 ====== 3 | 2 ------ 3 | 3 === 2 |
2 | 1 | | 3 --- 1 | 2 ====== 5 --- 1 | 1 | 1 # 1 | |
3 --- 1 | | 2 === 3 | 2 --- 3 1 | 4 === 3 | 1 # | 2 === 4
| | 2 --- 3 ====== 4 | | | 2 --- 1 | | | 3 --- 5 --- 1 |
1 | 3 === 4 --- 4 ====== 4 | 1 | 3 === 5 --- 2 ------ 5 ====== 3 | # 1 --- 4
| 1 | | # 2 ------ 3 | | 2 ------ 1 | 2 --- 4 ====== 6 --- 3 #
4 --- 5 ------ 1 | 2 === 6 ------ 1 | 1 | | 3 === 3 | 1 1 | # 3
# 2 # 3 === 4 --- 1 | 3 --- 4 ====== 5 | | 2 ====== 5 | | 1 | 2 |
2 # 2 | 3 === 2 | # 3 ------ 1 # 4 === 6 ------ 2 # 3 --- 2 | 3 ====== 4
3 ------ 3 | 2 ====== 4 --- 3 # # | 1 # 1 | # | 2 === 4 ------ 2 |
1 | 3 ====== 5 --------- 5 === 3 --- 4 | | 2 | | 2 | 3 ====== 2 | 3
3 === 2 | | 2 # 3 ====== 2 | 1 | | 4 === 3 | | #
| | 3 === 2 # 2 | 3 ------ 3 --- 4 --- 5 === 3 | 1 ------ 4 --- 3 === 4 #
3 ------ 5 === 4 --- 5 ------ 4 # | | | 1 ------ 4 ====== 2 | 3 --- 1 | 3
| | | | 1 # 3 --- 2 | 2 --- 4 ====== 4 ------ 4 === 3 # 1 |
3 === 2 | 1 1 | # | 3 ====== 3 --- 1 | | 1 --- 4 --- 2 --- 2
2 === 3 2 === 4 --- 5 ====== 4 --- 1 2 ====== 3 3 === 3 --- 3 === 2
; END