ErsatzはSATソルバの入力を__モナドの力__で生成してくれるライブラリ。適当にexistsとassertを並べればうまくやってくれるらしい。ということで、数独ソルバを実装してみた。素晴らしい…

sudoku.hs

import Prelude hiding ((||), (&&), not, and, or)
import Data.Char
import Data.Array
import Data.Ix
import Data.Word
import Control.Monad
import Control.Monad.State
import Ersatz -- (ersatz-0.2)

fieldRange = ((1,1),(9,9))

unique :: Equatable a => [a] -> Bit
unique = go [] where
    go ss (x:xs) = and (map (/==x) ss) && go (x : ss) xs
    go _ [] = true

sudoku :: (MonadState s m, HasSAT s) => Array (Int, Int) Char
    -> Array (Int, Int) Bit4 -> m (Array (Int, Int) Bit4)
sudoku problem answer = do
    forM_ (range fieldRange) $ \ix -> assert $ if isDigit (problem ! ix)
        -- 既に埋められているマスを確定
        then answer ! ix === encode (toEnum $ digitToInt $ problem ! ix)
        -- 空いているマスには1から9までの数字が入る
        else let Bit4 b3 b2 b1 b0 = answer ! ix in or
                [ b3 && not b2 && not b1 -- 8,9
                , not b3 && (b2 || b1 || b0) -- excepting 0
                ]
    -- 行が一意
    forM_ [1..9] $ \r -> assert $ unique [answer ! (c, r) | c <- [1..9]]
    -- 列が一意
    forM_ [1..9] $ \c -> assert $ unique [answer ! (c, r) | r <- [1..9]]
    -- ブロック内が一意
    forM_ (range ((0,0),(2,2))) $ \(sc, sr) ->
        assert $ unique [answer ! (sc * 3 + c, sc * 3 + r) | c <- [1..3], r <- [1..3]]
    return answer

showField :: (Result, Maybe (Array (Int, Int) Word8)) -> IO ()
showField (_, Just answer) = forM_ [1..9] $ \r -> do
    forM_ [1..9] $ \c -> putChar $ intToDigit $ fromEnum $ answer ! (c, r)
    putChar '\n'
showField _ = fail "Impossible"

main :: IO ()
main = do
    problem <- liftM (array fieldRange . concat)
        $ forM [1..9] $ \r -> do
            line <- getLine
            return [((c, r), ch) | (c, ch) <- zip [1..9] line]
    let sat = replicateM 81 exists >>= sudoku problem . listArray fieldRange
    minisatPath "cryptominisat" `solveWith` sat >>= showField

$ runhaskell sudoku.hs
-9---3---
-7----8--
---5--2--
5--------
-----7-91
2---4----
----6-4--
6--2-----
-------7-
192783645
375691824
864539217
548912763
426857391
217346958
739165482
681274539
953428176