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