塗り分けパズルをHaskellとSATソルバーで解く

久々にHaskell触ったので軽いネタを書いておく。

年始に某パズルを解いて応募すると抽選で箱根の温泉旅行が当たる、というものがあった。
多角形のマスが一杯あって隣接するマスが同じ色にならないように塗り分けると解けるというタイプのパズルだ。
で、紙に印刷して色々試せば解けそうだったのだが、面倒だったのでSATソルバーで解けるんじゃないかと試してみた。
最初Rubyで使えるライブラリを探したのだが、2.3.0では動かなかったのでHaskellで探すことにした。
Haskellで探したのは、なんか一杯ありそうだと思ったから。予想通りやたら一杯ライブラリがあったw

ちなみにSATソルバーってのは充足可能性問題を解くためのアルゴリズムで、なんか色々論文があるらしいが細かいことは良く分かりませんw
とりあえず数独が解けるんなら、こういうパズルも解けるはずである。
で、結果試してみたら、あっさり解けたのでSATソルバー凄いなーと思った。
ちなみに温泉旅行は外れた。 orz

めっちゃ久々に書いたので、すげー雑な上にこういう使い方で良いのか良く分からんが、とにかく解けたのでコードを貼ってみる。

```haskell
{-# LANGUAGE ScopedTypeVariables #-}

import Prelude hiding ( not )
import Control.Monad

import Satchmo.Binary.Op.Fixed 
import qualified Satchmo.Binary.Op.Flexible 
import Satchmo.SAT.Mini
import Satchmo.Boolean hiding ( equals )
import Satchmo.Code
import qualified Satchmo.Integer as SI

import System.Environment

main :: IO ()
main = do
    [ n ] <- getArgs
    (res :: Maybe [ Integer ]) <- solve $ do
        zero <- Satchmo.Binary.Op.Flexible.constant 0
        five <- Satchmo.Binary.Op.Flexible.constant 5

        ho1 <- number 3
        shi1 <- number 3
        ko <- number 3
        se <- number 3
        ta <- number 3
        e1 <- number 3
        ka1 <- number 3
        e2 <- number 3
        ri <- number 3
        i1 <- number 3
        a <- number 3
        ka2 <- number 3
        de <- number 3
        i2 <- number 3
        ru <- number 3
        ha <- number 3
        ba <- number 3
        ni <- number 3
        ki <- number 3
        re <- number 3
        xtsu <- number 3
        ma <- number 3
        ji <- number 3
        ho2 <- number 3
        shi2 <- number 3
        ku <- number 3
        to <- number 3

        let args = [
                   ho1,
                   shi1,
                   ko,
                   se,
                   ta,
                   e1,
                   ka1,
                   e2,
                   ri,
                   i1,
                   a,
                   ka2,
                   de,
                   i2,
                   ru,
                   ha,
                   ba,
                   ni,
                   ki,
                   re,
                   xtsu,
                   ma,
                   ji,
                   ho2,
                   shi2,
                   ku,
                   to
                   ]

        let cs1 = concatMap (\n -> [gt n zero, lt n five]) args
        monadic assertAnd cs1

        monadic assertAnd [
          notGreen ho1,
          notGreen shi1, notBlue shi1,
          notGreen ko,
          notRed se,
          notRed ta,
          notBlue e1,
          notGreen ka1, notBlue ka1,
          notGreen e2, notRed e2,
          notBlue ri,
          notRed i1,
          notBlue a,
          notRed ka2, notGreen ka2,
          notBlue de, notGreen de, notRed de,
          notRed ru,
          notGreen ha,
          notGreen ba, notRed ba,
          notGreen ni,
          notGreen ki, notRed ki,
          notGreen re,
          notGreen xtsu, notRed xtsu,
          notGreen ho2, notRed ho2,
          notYello ku,
          notGreen to, notYello to
                          ]

        monadic assertAnd [
          notEqual ho1 ko,
          notEqual ho1 e1,
          notEqual ho1 ka1,
          notEqual ko shi1,
          notEqual ko ka1,
          notEqual shi1 se,
          notEqual shi1 ka1,
          notEqual shi1 e2,
          notEqual se ta,
          notEqual se e2,
          notEqual e1 ka1,
          notEqual e1 ri,
          notEqual e1 a,
          notEqual ka1 ri,
          notEqual e2 i1,
          notEqual ta i1,
          notEqual i1 ru,
          notEqual ri a,
          notEqual a de,
          notEqual a ha,
          notEqual de ha,
          notEqual de ba,
          notEqual de e2,
          notEqual ka2 ru,
          notEqual ka2 ba,
          notEqual ka2 i2,
          notEqual i2 ru,
          notEqual i2 ni,
          notEqual ni re,
          notEqual ni ka2,
          notEqual ni shi2,
          notEqual re xtsu,
          notEqual xtsu ki,
          notEqual xtsu re,
          notEqual ki ha,
          notEqual ki a,
          notEqual xtsu ho2,
          notEqual re ho2,
          notEqual re shi2,
          notEqual ni ma,
          notEqual ni ji,
          notEqual ma ji,
          notEqual ji i2,
          notEqual ho2 shi2,
          notEqual ho2 to,
          notEqual ji to,
          notEqual ji ku,
          notEqual ku ru,
          notEqual ku i2,
          notEqual ho2 re,
          notEqual ho2 ji,
          notEqual ma shi2,
          notEqual ma ho2,
          notEqual ku to
                          ]

        return $ decode [
                        ho1,
                        shi1,
                        ko,
                        se,
                        ta,
                        e1,
                        ka1,
                        e2,
                        ri,
                        i1,
                        a,
                        ka2,
                        de,
                        i2,
                        ru,
                        ha,
                        ba,
                        ni,
                        ki,
                        re,
                        xtsu,
                        ma,
                        ji,
                        ho2,
                        shi2,
                        ku,
                        to
                        ]
    print res

blue :: SAT Number
blue = Satchmo.Binary.Op.Flexible.constant 1
yellow :: SAT Number
yellow = Satchmo.Binary.Op.Flexible.constant 2
green :: SAT Number
green = Satchmo.Binary.Op.Flexible.constant 3
red :: SAT Number
red = Satchmo.Binary.Op.Flexible.constant 4

notBlue :: Number -> SAT Boolean
notBlue f = do
    b <- blue
    e <- equals f b
    return $ not e

notYello :: Number -> SAT Boolean
notYello f = do
    b <- yellow
    e <- equals f b
    return $ not e

notGreen :: Number -> SAT Boolean
notGreen f = do
    b <- green
    e <- equals f b
    return $ not e

notRed :: Number -> SAT Boolean
notRed f = do
    b <- red
    e <- equals f b
    return $ not e

notEqual :: Number -> Number -> SAT Boolean
notEqual a b = do
    e <- equals a b
    return $ not e
```

今回使ったのは[satchmo](https://github.com/jwaldmann/satchmo "jwaldmann/satchmo")というライブラリで、モナドで制約条件をガンガン書いていけば、いい感じにMaybeで返してくれるというライブラリだった。
面倒なSAT符号化を制約条件羅列するだけで済ませてくれるので楽だった。
バックエンドはminisatを使っているらしい。

久々にHaskell触ったし、SATソルバーが良く分かってなかったんで、使い方を調べるのに半日ぐらいかかったので、多分手でやった方が絶対早かった気がするが、正月休み中の暇潰しとしては楽しかったので良しとしておく。