Akari (美術館) Solver using SAT solvers

Cell.hs

{-# LANGUAGE DeriveAnyClass, DeriveDataTypeable, DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies, FlexibleInstances, MultiWayIf #-}
{-# LANGUAGE TypeFamilies                                      #-}
module Cell where
import Control.Applicative (empty)
import Data.Typeable       (Typeable)
import Data.Word
import Ersatz
import GHC.Generics        (Generic)

newtype MCell = MCell Bit4
          deriving (Show, Typeable, Generic,
                    Equatable, Variable, Boolean)

data Cell = Empty | Light | Lit | Wall (Maybe Word8)
  deriving (Read, Show, Eq, Ord, Generic)

instance Codec MCell where
  type Decoded MCell = Cell
  decode s (MCell n) = do
    i <- decode s n
    if | i <= 4    -> pure $ Wall $ Just i
       | i == 5    -> pure Empty
       | i == 6    -> pure Light
       | i == 7    -> pure $ Wall Nothing
       | i == 8    -> pure Lit
       | otherwise -> empty
  encode Empty = MCell $ encode 5
  encode Light = MCell $ encode 6
  encode (Wall Nothing) = MCell $ encode 7
  encode Lit = MCell $ encode 8
  encode (Wall (Just n))
    | n <= 4 = MCell $ encode n
    | otherwise = error $ "Block number out of bound: " ++ show n

instance Num Cell where
  fromInteger = Wall . Just . fromInteger
  (+) = error "not implemented"
  (-) = error "not implemented"
  (*) = error "not implemented"
  abs = error "not implemented"
  signum = error "not implemented"

Main.hs

{-# LANGUAGE LambdaCase, PatternSynonyms #-}
module Main where
import           Cell
import qualified Data.Vector as V
import           Ersatz
import           Problem

pattern W :: Cell
pattern W = Wall Nothing

pattern E :: Cell
pattern E = Empty

input :: Grid
input = V.fromList $ map V.fromList
  [[E, E, W, E, E, E, W]
  ,[E, 4, E, E, 1, E, W]
  ,[E, E, E, 2, E, E, E]
  ,[E, W, E, E, E, W, E]
  ,[E, E, E, W, E, E, E]
  ,[W, E, W, E, E, 1, E]
  ,[1, E, E, E, 1, E, E]
  ]
-- Problem taken from  the NIKOLI web site:
-- https://www.nikoli.co.jp/ja/puzzles/akari/


main :: IO ()
main = solve input >>= \case
  (Satisfied, Just grid) -> putStrLn $ prettyGrid grid
  ans -> print ans
{-
ghci> :ma
＋○■＋＋○■
○４○＋１＋■
＋○＋２○＋＋
＋■＋○＋■＋
＋＋＋■＋＋○
■＋■○＋１＋
１○＋＋１○＋
-}

Problem.hs

{-# LANGUAGE LambdaCase, PartialTypeSignatures #-}
module Problem where
import Cell

import           Control.Arrow
import           Control.Monad.Reader
import           Control.Monad.State
import           Data.Semigroup
import           Data.Vector          (Vector)
import qualified Data.Vector          as V
import           Data.Word
import           Ersatz
import           Prelude              hiding (all, any, not, (&&), (||))

type Grid = Vector (Vector Cell)
type MGrid = Vector (Vector MCell)

solve :: MonadIO f => Grid -> f (Result, Maybe Grid)
solve grid =
  second (fmap $ V.fromList . map V.fromList) <$> solveWith minisat (problem grid)


prettyGrid :: Grid -> String
prettyGrid = unlines . V.toList . V.map (foldMap pret)
  where
    pret Empty            = "　"
    pret Lit              = "＋"
    pret (Wall Nothing)   = "■"
    pret (Wall (Just 0))  = "０"
    pret (Wall (Just 1))  = "１"
    pret (Wall (Just 2))  = "２"
    pret (Wall (Just 3))  = "３"
    pret (Wall (Just ~4)) = "４"
    pret Light            = "○"


problem :: (HasSAT s, MonadState s m, MonadIO m) => Grid -> m [[MCell]]
problem gri = do
  let height = V.length gri
      Max width  = foldMap (Max . V.length) gri
  matrix <- V.mapM (V.mapM $ const exists) gri
  let pMat = zipMatrix gri matrix
      toIni i j (Empty, v) =
        let mcs = accessible width height pMat (i, j)
        in assert $
           v === encode Lit && any (=== encode Light) mcs ||
           v === encode Light && all (=== encode Lit) mcs
      toIni _ _ (b, v)     = assert $ v === encode b
  -- Preservation of initial placemants
  V.imapM_ (V.imapM_ . toIni) pMat

  -- Processing cells adjacent to numbered wall
  V.imapM_ (V.imapM_ . procAdj matrix height width) pMat
  return $ map V.toList $ V.toList matrix

accessible :: Width -> Height
           -> Vector (Vector (Cell, MCell)) -> (YCoord, XCoord) -> [MCell]
accessible w h mat (i, j) =
  let getIt k = foldMap (map snd . filter ((/= k) . fst) . V.toList) .
                filter (any $ (== k) . fst) . emptySegments

      r = getIt j $
          V.imap (\k (a, b) -> (a, (k, b))) $ mat V.! i
      c = getIt i $
          V.imap (\k (a, b) -> (a, (k, b))) $ transpose w h mat V.! j
  in r ++ c


type Height = Int
type Width = Int
type XCoord = Int
type YCoord = Int

procAdj :: (HasSAT s, MonadState s m)
        => MGrid -> Height -> Width -> YCoord -> XCoord -> (Cell, MCell) -> m ()
procAdj mc h w i j (Wall (Just n), _) = do
  let as = [ (i', j')
           | (dy, dx) <- [(-1, 0), (1, 0), (0, -1), (0, 1)]
           , let i' = i + dy; j' = j + dx
           , 0 <= i' && i' < h
           , 0 <= j' && j' < w
           ]
      pos = comb n as
  assert $ any (\(ps, ns) -> all ((=== encode Light) . (mc !@)) ps && all ((/== encode Light) . (mc !@)) ns) pos
procAdj _ _ _ _ _ _                  = return ()

(!@) :: Vector (Vector a) -> (Int, Int) -> a
m !@ (i, j) = m V.! i V.! j

zipMatrix :: Vector (Vector a) -> Vector (Vector b) -> Vector (Vector (a, b))
zipMatrix = V.zipWith V.zip

transpose :: Width -> Height -> Vector (Vector a) -> Vector (Vector a)
transpose w h m =
  V.generate w $ \j -> V.generate h $ \ i ->
  m V.! i V.! j

emptySegments :: Vector (Cell, a) -> [Vector a]
emptySegments vc =
  map (V.map snd) $
  filter (not . V.null) $
  splitOn ((`notElem` [Empty, Light]) . fst) vc

splitOn :: (a -> Bool) -> Vector a -> [Vector a]
splitOn p vs =
  let (ls, rs) = V.break p vs
  in if V.null rs
  then if V.null ls then [] else [ls]
  else ls : splitOn p (V.tail rs)

comb :: Word8 -> [a] -> [([a], [a])]
comb 0 [] = [([], [])]
comb _ [] = []
comb n (x : xs) =
  [(x : ys, zs) | (ys, zs) <- comb (n - 1) xs ]
  ++ [ (ys, x:zs) | (ys, zs) <- comb n xs ]

uniqueLight :: [MCell] -> Bit
uniqueLight vs =
  any (\(~[a], bs) -> a === encode Light && all (/== encode Light) bs) $ comb 1 vs