| 8 | 9 | ||||||||
| 4 | 2 | ||||||||
| 2 | 5 | ||||||||
| 6 | 8 | ||||||||
| 4 | 4 | ||||||||
| 6 | 7 | ||||||||
| 4 | 4 | ||||||||
| 3 | 4 | ||||||||
| 4 | 2 | ||||||||
| 6 | 8 |
なお，以下ではパズルの盤面の一番上の行を第0行， 一番左の列を第0列として数えます．
(int r_0 0 9)
(int c_0 0 9)
さらに，長方形s_0の面積は8ですから，
変数h_0とw_0の取り得る値は，1, 2, 4, 8のいずれかです
(この部分も制約条件として記述することもできるのですが，
簡単のため約数は自分で求めることにします．ちょっとずるい?)．
このドメインをhw_0で表すことにし，
それぞれの変数を以下のように宣言します．
(domain hw_0 (1 2 4 8)) ; hw_0 = { 1, 2, 4, 8 }
(int h_0 hw_0) ; h_0 ∈ hw_0
(int w_0 hw_0) ; w_0 ∈ hw_0
次に，h_0が1の時はw_0は8になるので，
以下のように取り得る値の組み合わせの条件を記述します．
(or (and (= h_0 1) (= w_0 8)) (and (= h_0 2) (= w_0 4))
(and (= h_0 4) (= w_0 2)) (and (= h_0 8) (= w_0 1)))
現状のSugarでは，変数どうしの積を利用できないので，
ちょっと面倒な記述になっています．
最後に，長方形は盤面の内部にないといけないので，以下の条件を追加します．
(<= (+ r_0 h_0) 10)
(<= (+ c_0 w_0) 10)
他の長方形についても同様に宣言します．
長方形s_kの内部は， 行がr_k以上r_k+h_k未満， 列がc_k以上c_k+w_k未満ですので， 数字の位置がその範囲に入れば良いわけです．
たとえば，2行目6列目にある数字5に対応する長方形s_5についての条件は 以下のようになります．
(and (<= r_5 2) (< 2 (+ r_5 h_5)))
(and (<= c_5 6) (< 6 (+ c_5 w_5)))
二つの長方形s_k1とs_k1 (k1 < k2)とが 重ならない条件は， 長方形s_k1のほうが 上にあるか，下にあるか，左にあるか，右にあるかのいずれかが成り立つことです．
たとえば，長方形s_0とs_1とが重ならない条件は 以下のようになります．
(or (<= (+ r_0 h_0) r_1) (<= (+ r_1 h_1) r_0)
(<= (+ c_0 w_0) c_1) (<= (+ c_1 w_1) c_0))
あるいは，重なる条件を考えて，その否定としても同じです．
(not (and (> (+ r_0 h_0) r_1) (> (+ r_1 h_1) r_0)
(> (+ c_0 w_0) c_1) (> (+ c_1 w_1) c_0)))
他のすべての組み合わせについても同様に記述します．
s SATISFIABLE a r_0 0 a c_0 3 a h_0 2 a w_0 4 a r_1 0 a c_1 7 a h_1 3 a w_1 3 a r_2 0 a c_2 0 a h_2 2 a w_2 2 a r_3 0 a c_3 2 a h_3 2 a w_3 1 a r_4 2 a c_4 0 a h_4 1 a w_4 2 a r_5 2 a c_5 2 a h_5 1 a w_5 5 a r_6 3 a c_6 1 a h_6 1 a w_6 6 a r_7 3 a c_7 7 a h_7 4 a w_7 2 a r_8 3 a c_8 0 a h_8 4 a w_8 1 a r_9 4 a c_9 1 a h_9 1 a w_9 4 a r_10 4 a c_10 5 a h_10 3 a w_10 2 a r_11 3 a c_11 9 a h_11 7 a w_11 1 a r_12 5 a c_12 1 a h_12 2 a w_12 2 a r_13 5 a c_13 3 a h_13 2 a w_13 2 a r_14 7 a c_14 2 a h_14 1 a w_14 3 a r_15 7 a c_15 5 a h_15 1 a w_15 4 a r_16 8 a c_16 6 a h_16 2 a w_16 2 a r_17 8 a c_17 8 a h_17 2 a w_17 1 a r_18 7 a c_18 0 a h_18 3 a w_18 2 a r_19 8 a c_19 2 a h_19 2 a w_19 4 aSugarの次期リリースには， 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です． 以下は，その実行例です．
$ ./shikaku.pl data/shikaku-0.txt >csp/shikaku-0.csp
$ /usr/bin/time sugar csp/shikaku-0.csp >log/shikaku-0.log
2.35user 0.09system 0:01.62elapsed 150%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+304outputs (2major+14197minor)pagefaults 0swaps
$ ./shikaku.pl -s log/shikaku-0.log data/shikaku-0.txt
; Shikaku Puzzle
; # http://www.nikoli.co.jp/en/puzzles/shikaku/
; size 10 10
; - - - - 8 - - - - 9
; - 4 2 - - - - - - -
; - 2 - - - - 5 - - -
; - - - - - - 6 8 - -
; 4 - - - 4 - - - - -
; - - - - - 6 - - - 7
; - - 4 4 - - - - - -
; - - - 3 - - - - 4 -
; - - - - - - - 4 2 -
; 6 - - - - 8 - - - -
-- -- -- -- -- -- -- -- -- --
| | | 8 | 9|
| 4| 2| | |
-- -- -- -- -- -- --
| 2| 5| |
-- -- -- -- -- -- -- -- -- --
| | 6| 8 | |
-- -- -- -- -- --
| 4| 4| | | |
-- -- -- --
| | | | 6 | | 7|
| | 4| 4 | | | |
-- -- -- -- -- -- -- -- --
| | 3 | 4| |
-- -- -- -- -- -- --
| | | 4| 2| |
| 6 | 8| | | |
-- -- -- -- -- -- -- -- -- --
; END
以下は，
Nikoli: 四角に切れのおためし問題中の
おためし問題10 (36x20)をLet's Note CF-W5で解いた結果です(MiniSat2を使用)．
10秒以内で解けています(CPU時間は約13秒)．
「四角に切れ」はSugar制約ソルバー向きの問題のようです．
$ ./shikaku.pl data/shikaku-10.txt >csp/shikaku-10.csp
$ /usr/bin/time sugar csp/shikaku-10.csp >log/shikaku-10.log
12.96user 0.34system 0:08.61elapsed 154%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+6784outputs (2major+44348minor)pagefaults 0swaps
$ ./shikaku.pl -s log/shikaku-10.log data/shikaku-10.txt
; Shikaku Puzzle
; # http://www.nikoli.co.jp/en/puzzles/shikaku/
; size 36 20
; - - 4 - - - - 6 - - - - - 12 - - - - - - - 8 - - - - - - - - 6 - - - - 6
; - 4 - - - - 5 - - - - - 4 - - - - - - 3 5 - - - - - - - - 6 - - - - 8 -
; 4 - - - 4 - - - - - 10 - - - - - - 6 8 - - - - - - 9 3 4 - - - - - 8 - -
; - - - 6 - - - - - - - 2 - - - - - - - - - - - - - - - - - - - 10 - - - -
; - - - - - - - - - 6 - - - - - 4 - - - - - 12 6 - - - - - - - 6 - - - - -
; - 8 - - 4 2 8 - 4 - - - - - 4 - - - - - - - - 4 - - - - 4 - - - - - - -
; 5 - - - - - - - - - - - - 6 - - - - - - - - - 3 - - - 8 - - - - - - - 8
; - - - - - - - - - - - - 4 - - - 8 - - - 4 - - - - - - - - - - - - - 6 -
; - - - 8 - - - - - - 8 - - - - 6 - - - 6 - - - - - 4 - - - - 6 6 6 - - -
; - - 9 - - - - 4 - - - - - 4 - - - - - - - - 2 - - - - - 8 - - - - - - -
; - - - - - - - 8 - - - - - 9 - - - - - - - - 4 - - - - - 8 - - - - 4 - -
; - - - 6 8 8 - - - - 9 - - - - - 9 - - - 9 - - - - 8 - - - - - - 8 - - -
; - 6 - - - - - - - - - - - - - 4 - - - 12 - - - 6 - - - - - - - - - - - -
; 6 - - - - - - - 6 - - - 6 - - - - - - - - - 6 - - - - - - - - - - - - 4
; - - - - - - - 4 - - - - 6 - - - - - - - - 8 - - - - - 4 - 4 6 6 - - 10 -
; - - - - - 7 - - - - - - - 12 6 - - - - - 9 - - - - - 3 - - - - - - - - -
; - - - - 4 - - - - - - - - - - - - - - - - - - - 6 - - - - - - - 4 - - -
; - - 6 - - - - - 4 6 4 - - - - - - 4 4 - - - - - - 8 - - - - - 4 - - - 3
; - 4 - - - - 6 - - - - - - - - 6 6 - - - - - - 8 - - - - - 4 - - - - 4 -
; 4 - - - - 6 - - - - - - - - 8 - - - - - - - 6 - - - - - 7 - - - - 3 - -
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| | 4 | 6 | |12 | | 8 | 6| | 6|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| 4| 5| | 4| | | 3| 5 | 6 | 8| |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| 4| | 4 | 10 | | | | 6| 8 | | 9| 3| 4| | 8 | |
-- -- -- -- -- -- -- -- --
| | | 6 | | 2| | | | | | | | | | 10 | | |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| | | | | | | 6 | | 4| | | 12| 6| | | | | 6 | | |
-- -- -- -- -- -- -- -- --
| | 8 | 4| 2| 8 | 4| | | 4 | | | | | 4 | | 4 | | | |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| 5 | | | | | 6| | | | | | 3| 8| 8|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| | | | | | | 4| | 8| | 4 | | | | | | | 6 |
-- -- -- -- -- -- -- -- -- -- -- -- -- --
| 8| | | | | 8| | 6| 6 | | | 4 | 6| 6| 6 | |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| 9| | | | 4| | | 4 | | | | 2| 8 | | | |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| | | | | 8| | | 9 | | | | 4 | | 8 | | | 4 |
-- -- -- --
| | 6| 8| 8| | | 9 | | | 9 | 9 | | 8 | | | | 8 |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| | 6 | | | | | | | | 4| 12 | 6 | | | | |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| 6| | | | | | 6| | 6 | | 6 | | | | | 4|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| | | | | 4 | | 6 | 8 | 4| 4| 6| 6 | 10| |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| | 7 | | | | 12| 6 | 9 | | 3 | | | | | |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| | | 4 | | | | | | | | | 6| | 4| | |
-- -- -- -- -- -- -- -- --
| | 6 | | | 4| 6| 4| | | 4| 4 | | | 8 | 4 | | 3|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| 4 | | 6 | | | | | 6| 6 | 8 | 4 | 4| |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
| 4 | 6| | 8 | | 6 | 7 | 3 | |
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
; END