gistfile1.hs

import Control.Applicative
import Control.Monad
import Data.Char
import Data.List.Split
import Data.SBV

main :: IO ()
main = do
  t <- map read . words <$> getLine
  case t of
    [0, 0] -> do
      return ()
    [h, w] -> do
      bd <- replicateM h $ getLine
      go h w bd
      main

go :: Int -> Int -> [[Char]] -> IO ()
go h w bd = do
  let mine ass = do
        let zeroOrOne = bAll (\n -> n .== 0 ||| n .== 1) $ concat ass

            dotIsNotMine =
              [ a .== 0
              | j <- [0..h-1]
              , i <- [0..w-1]
              , let c = bd !! j !! i
              , let a = ass !! j !! i
              , c == '.'
              ]

            numIsCorrect =
              [ sum
                [ ass !! (j + dj) !! (i + di)
                | dj <- [-1 .. 1], di <- [-1 .. 1]
                , j + dj >= 0 && j + dj < h
                , i + di >= 0 && i + di < w
                ]
                .== literal n
              | j <- [0..h-1]
              , i <- [0..w-1]
              , let c = bd !! j !! i
              , isDigit c
              , let n = read [c] :: Integer
              ]

        bAnd $ [zeroOrOne] ++ dotIsNotMine ++ numIsCorrect

  Just res <- minimize Quantified sum (h * w) (mine . chunksOf w)
  print $ sum res