四角に切れパズルをSugar制約ソルバーで解く


はじめに

Nikoliによる 四角に切れ(Shikaku)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます.

例題

Nikoliによる 四角に切れの例題 です.
例題
      8      9
 4 2          
 2       5    
         68   
4     4       
       6     7
   44         
    3       4 
          4 2 
6      8      

四角に切れのルール

Nikoliによる四角に切れのルールは以下の通りです.
(Rule 1)
盤面を長方形(正方形)に分割します.
(Rule 2)
数字は,1マスの面積を1とした,長方形の面積です. 4と書いてあるマスを含む長方形は,1x4,2x2,4x1のどれかになります.
(Rule 3)
切るのは点線の上で,どの長方形にも数字が1つずつ入ります.
四角に切れを 制約充足問題(CSP, Constraint Satisfaction Problem)として表すための 方法について考えていきます.

なお,以下ではパズルの盤面の一番上の行を第0行, 一番左の列を第0列として数えます.

Rule 1とRule 2

(Rule 1)
盤面を長方形(正方形)に分割します.
(Rule 2)
数字は,1マスの面積を1とした,長方形の面積です. 4と書いてあるマスを含む長方形は,1x4,2x2,4x1のどれかになります.
「分割」というRuleは後回しにし,他のRuleについて,次のようにします. たとえば,長方形s_0について, 変数r_0c_0の宣言は以下のようになります.
    (int r_0 0 9)
    (int c_0 0 9)
さらに,長方形s_0の面積は8ですから, 変数h_0w_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)
他の長方形についても同様に宣言します.

Rule 3

(Rule 3)
切るのは点線の上で,どの長方形にも数字が1つずつ入ります.
各数字が,対応する長方形の内部にあるという条件を記述します. 後述の長方形が互いに重ならないという条件を追加すれば, どの長方形にも数字が1つずつ入ることになります.

長方形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)))

Rule 1 再び

(Rule 1)
盤面を長方形(正方形)に分割します.
ここでは,長方形が互いに重ならないという条件を記述します.

二つの長方形s_k1s_k1 (k1 < k2)とが 重ならない条件は, 長方形s_k1のほうが 上にあるか,下にあるか,左にあるか,右にあるかのいずれかが成り立つことです.

たとえば,長方形s_0s_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)))
他のすべての組み合わせについても同様に記述します.

実行結果

すべての制約を記述したファイルを作成し, Sugarで実行すると以下のような結果が得られます.
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
a
Sugarの次期リリースには, 問題ファイルを読み込んで 制約条件を記述した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

「パズルをSugar制約ソルバーで解く」に戻る


Naoyuki Tamura
( Last modified: Fri Jul 11 13:09:33 2008 JST ,   ?????  Since June 4, 2008 )