abc-puzzle 0.2 → 0.2.1
raw patch · 2 files changed
+109/−127 lines, 2 filesdep +arraydep −vectordep ~base
Dependencies added: array
Dependencies removed: vector
Dependency ranges changed: base
Files
- abc-puzzle.cabal +3/−3
- src/Main.hs +106/−124
abc-puzzle.cabal view
@@ -1,5 +1,5 @@ name: abc-puzzle-version: 0.2+version: 0.2.1 synopsis: Generate instances of the ABC Logic Puzzle. description: This program generate instances of the ABC Logic Puzzle (<http://en.wikipedia.org/wiki/Buchstabensalat_%28logic_puzzle%29>).@@ -22,8 +22,8 @@ hs-source-dirs: src ghc-options: -W -- other-modules: - other-extensions: ImplicitParams, ConstraintKinds- build-depends: base >=4.7 && <5, vector >=0.10, minisat >=0.1, Safe >=0.1, random >=1.0, + other-extensions: ImplicitParams+ build-depends: base >=3 && <5, array, minisat >=0.1, Safe >=0.1, random >=1.0, random-shuffle >= 0.0.4 default-language: Haskell2010
src/Main.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE ImplicitParams, ConstraintKinds #-}+{-# LANGUAGE ImplicitParams #-} -- ABC logic puzzle @@ -6,8 +6,7 @@ import Control.Monad import Data.List-import qualified Data.Vector as Vector-import Data.Vector (Vector, (!),(//))+import Data.Array.IArray import MiniSat import Safe import System.Environment@@ -15,50 +14,57 @@ import System.Random.Shuffle import System.Random -type Puzzle = Vector (Vector Field) -- rows of columns-type Field = Vector Lit+type Puzzle = Array Int (Array Int Field) -- rows of columns+type Field = Array Int Lit data Hints = Hints {- top, right, bottom, left :: Vector Field}+ top, right, bottom, left :: Array Int Field} data Full = Full { puzzle :: Puzzle, hints :: Hints} -type Env = (?size :: Int, ?letters :: Int, ?solver :: Solver)--genLit :: Env => IO Lit+genLit :: (?solver :: Solver) => IO Lit genLit = newLit ?solver +replicateAM :: Monad m => Int -> m a -> m (Array Int a)+replicateAM l m = liftM (listArray (0,l-1)) (replicateM l m) -genField :: Env => IO Field-genField = Vector.replicateM (?letters+1) genLit+replicateA :: Int -> a -> Array Int a+replicateA l m = listArray (0,l-1) (replicate l m) -genPuzzle :: Env => IO Puzzle-genPuzzle = Vector.replicateM ?size $ Vector.replicateM ?size genField -genHints :: Env => IO Hints+genField :: (?letters :: Int, ?solver :: Solver) => IO Field+genField = replicateAM (?letters+1) genLit++genPuzzle :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => IO Puzzle+genPuzzle = replicateAM ?size $ replicateAM ?size genField++genHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => IO Hints genHints = liftM4 Hints side side side side- where side = Vector.replicateM ?size genField+ where side = replicateAM ?size genField -genFull :: Env => IO Full+genFull :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => IO Full genFull = liftM2 Full genPuzzle genHints -addClause' :: Env => [Lit] -> IO ()+addClause' :: (?solver :: Solver) => [Lit] -> IO () addClause' c = addClause ?solver c >> return () -addClauses :: Env => [[Lit]] -> IO ()+addClauses :: (?solver :: Solver) => [[Lit]] -> IO () addClauses = mapM_ addClause' -lx :: Env => [Int]+lx :: (?letters :: Int) => [Int] lx = [1 .. ?letters] -fx :: Env => [Int]+fx :: (?letters :: Int) => [Int] fx = [0 .. ?letters] -sx :: Env => [Int]+sx :: (?size :: Int) => [Int] sx = [0 .. ?size - 1] +sx_reverse :: (?size :: Int) => [Int]+sx_reverse = [?size - 1, (?size - 2).. 0] -conHint :: Env => Field -- ^ hint field++conHint :: (?letters :: Int, ?solver :: Solver) => Field -- ^ hint field -> [Field] -- ^ neighbouring fields, the closest field is last -- in the list -> IO ()@@ -67,83 +73,56 @@ where blanks = map (\f -> neg (f!0)) -conBottomHints :: Env => Vector Field -> Puzzle -> IO ()+conBottomHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> Puzzle -> IO () conBottomHints h p = sequence_ [conHint (h!i) [(p!j)!i|j<-[(?letters-1) .. (?size-1)]]| i <- sx]- >> mapM_ conField (Vector.toList h)+ >> mapM_ conField (elems h) -conRightHints :: Env => Vector Field -> Puzzle -> IO ()+conRightHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> Puzzle -> IO () conRightHints h p = sequence_ [conHint (h!i) [(p!i)!j|j<-[(?letters-1) .. (?size-1)]]| i <- sx]- >> mapM_ conField (Vector.toList h)+ >> mapM_ conField (elems h) -conTopHints :: Env => Vector Field -> Puzzle -> IO ()+conTopHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> Puzzle -> IO () conTopHints h p = sequence_ [conHint (h!i) [(p!j)!i|j<-[(?size - ?letters),(?size - ?letters - 1) .. 0]]| i <- sx]- >> mapM_ conField (Vector.toList h)+ >> mapM_ conField (elems h) -conLeftHints :: Env => Vector Field -> Puzzle -> IO ()+conLeftHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> Puzzle -> IO () conLeftHints h p = sequence_ [conHint (h!i) [(p!i)!j|j<-[(?size - ?letters),(?size - ?letters - 1) .. 0]]| i <- sx]- >> mapM_ conField (Vector.toList h)+ >> mapM_ conField (elems h) -conHints :: Env => Full -> IO ()+conHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Full -> IO () conHints (Full p h) = conBottomHints (bottom h) p >> conRightHints (right h) p >> conTopHints (top h) p >> conLeftHints (left h) p -conFull :: Env => Full -> IO ()+conFull :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Full -> IO () conFull full = conPuzzle (puzzle full) >> conHints full -conField :: Env => Field -> IO ()-conField l = do addClause' $ Vector.toList l+conField :: (?letters :: Int, ?solver :: Solver) => Field -> IO ()+conField l = do addClause' $ elems l addClauses [ [neg (l!i), neg (l!j)] | i <- fx, j <- [0 .. i-1]] -conFields :: Env => Puzzle -> IO ()+conFields :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO () conFields p = sequence_ [conField ((p!i)!j) | i <- sx, j <- sx] --- generate contstraits that avoid ambiguous configurations-conAmbFields :: Env => Puzzle -> IO ()-conAmbFields p = when (?size >= 2) $ do- vis <- Vector.generateM ?size (\i -> Vector.generateM ?size (generate i))- let getVis i j = if i < low || j < low || i >= hi || j >= hi then- [((vis!i)!j)] else []- addClauses [ map neg [(((p!i)!j)!l), (((p!di)!dj)!l), (((p!i)!dj)!f), (((p!di)!j)!f)] - ++ getVis i j ++ getVis di dj ++ getVis i dj ++getVis di j- | i <- range, j <- range, di<-[0..i-1]++[i+1..(?size-1)]- , dj<-[j+1..(?size-1)], l <- lx, f<- fx, l/=f]-- where range = [0..(?size-2)]- low = ?size - ?letters + 1- hi = ?letters - 1- generate i j = if i < low || j < low || i >= hi || j >= hi- then do - lit <- genLit - con lit i j- return lit- else return (error "position is not on the fringe")- con lit i j = do - when (i < low) $ addClause' (lit : [neg (((p!i')!j)!0) |i'<-[0..i-1]])- when (j < low) $ addClause' (lit : [neg (((p!i)!j')!0) |j'<-[0..j-1]])- when (i >= hi) $ addClause' (lit : [neg (((p!i')!j)!0) |i'<-[i+1..(?size-1)]])- when (j >= hi) $ addClause' (lit : [neg (((p!i)!j')!0) |j'<-[j+1..(?size-1)]])-- -- fields must be different letters (however, both can be blank)-conDiffFields :: Env => Field -> Field -> IO ()+conDiffFields :: (?letters :: Int, ?solver :: Solver) => Field -> Field -> IO () conDiffFields l1 l2 = do addClauses [[neg (l1!i), neg (l2!i)] | i <- lx] -conRows :: Env => Puzzle -> IO ()+conRows :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO () conRows p = do -- fields must be different letters- sequence_ [conDiffFields (r!i) (r!j) | r <- Vector.toList p, i <- sx, j <- [0..i-1]] + sequence_ [conDiffFields (r!i) (r!j) | r <- elems p, i <- sx, j <- [0..i-1]] -- each letter must appear- addClauses [[(r!i)!l | i <- sx] | r <- Vector.toList p, l <- lx]+ addClauses [[(r!i)!l | i <- sx] | r <- elems p, l <- lx] -conColumns :: Env => Puzzle -> IO ()+conColumns :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO () conColumns p = do -- letters must be different letters sequence_ [conDiffFields ((p!i)!c) ((p!j)!c) | c <- sx, i <- sx, j <- [0..i-1]] -- each letter must appear addClauses [[((p!i!)c)!l | i <- sx] | c <- sx, l <- lx] -conPuzzle :: Env => Puzzle -> IO ()+conPuzzle :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO () conPuzzle p = conRows p >> conColumns p >> conFields p data Entry = Blank@@ -153,28 +132,28 @@ show Blank = " " show (Letter l) = [iterate succ 'A' !! l] -newtype Solution = Solution {unSolution :: Vector (Vector (Entry))}+newtype Solution = Solution {unSolution :: Array Int (Array Int (Entry))} instance Show Solution where- show = unlines . map (unwords . map show . Vector.toList) . Vector.toList . unSolution+ show = unlines . map (unwords . map show . elems) . elems . unSolution -getSolution :: Env => Puzzle -> IO Solution-getSolution p = liftM Solution $ liftM Vector.fromList $ - sequence [ liftM Vector.fromList $ - sequence [ getEntry f | f <- Vector.toList r] | r <- Vector.toList p ]+getSolution :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO Solution+getSolution p = liftM Solution $ liftM (listArray (0,?size-1)) $ + sequence [ liftM (listArray (0,?size-1)) $ + sequence [ getEntry f | f <- elems r] | r <- elems p ] -getHints :: Env => Vector Field -> IO [Entry]-getHints h = sequence [ getEntry f | f <- Vector.toList h]+getHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> IO [Entry]+getHints h = sequence [ getEntry f | f <- elems h] getAllHints :: Int -> [((Int,Int),Int)] -> AllHints getAllHints size hints = (AllHints t r b l (length hints))- where [t,r,b,l] = [ emp // [ (i,Letter (letter-1)) | ((s',i),letter) <- hints, s' == s] | s <- [0..3]] - emp = Vector.replicate size Blank+ where [t,r,b,l] = [ emp // [ (i,Letter (letter-1)) | ((s',i),letter) <- hints, s' == s] | s <- [0..3]]+ emp = replicateA size Blank -data AllHints = AllHints {atop, aright, abottom, aleft :: Vector Entry, hintSize :: Int} deriving Show+data AllHints = AllHints {atop, aright, abottom, aleft :: Array Int Entry, hintSize :: Int} deriving Show -getEntry :: Env => Field -> IO Entry+getEntry :: (?letters :: Int, ?solver :: Solver) => Field -> IO Entry getEntry l = do Just b <- modelValue ?solver (l!0) if b then return Blank else getLetter where getLetter :: IO Entry@@ -183,7 +162,7 @@ return $ Letter n -- Adds clause to avoid the currently found solution.-removeCurrentSolution :: Env => IO Bool+removeCurrentSolution :: (?solver :: Solver) => IO Bool removeCurrentSolution = do n <- minisat_num_vars ?solver addClause ?solver =<<@@ -196,24 +175,22 @@ entryToInt Blank = 0 entryToInt (Letter i) = i + 1 -removeSolution :: Env' => Solution -> IO ()+removeSolution :: (?size :: Int, ?letters :: Int, ?solver :: Solver, ?full :: Full) => Solution -> IO () removeSolution (Solution sol) = addClause' [neg (entryValue ((i,j),entryToInt $ (sol!i)!j))| i<-sx,j<-sx] prettyHints :: AllHints -> String prettyHints (AllHints t r b l s) = - " | " ++ (intercalate " | " $ map show $ Vector.toList t) ++ " | \n"+ " | " ++ (intercalate " | " $ map show $ elems t) ++ " | \n" ++ rule ++ intercalate rule rows ++ rule- ++ " | " ++ (intercalate " | " $ map show $ Vector.toList b) ++ " | \n\n"+ ++ " | " ++ (intercalate " | " $ map show $ elems b) ++ " | \n\n" ++ "number of hints: " ++ show s ++ "\n"- where rule = "-" ++ concat (replicate size "+---") ++ "+-\n"- divider = concat (replicate size "| ") ++ "|"- rows = zipWith (\l r -> show l ++ divider ++ show r ++ "\n") (Vector.toList l) (Vector.toList r)- size = Vector.length t--type Env' = (Env, ?full :: Full)+ where rule = "--" ++ concat (replicate size "+---") ++ "+--\n"+ divider = concat (replicate size " | ") ++ " | "+ rows = zipWith (\l r -> show l ++ divider ++ show r ++ "\n") (elems l) (elems r)+ size = length $ indices t -- complete list of entry positions @@ -226,19 +203,20 @@ ?letters = letters f <- genFull conFull f- conAmbFields (puzzle f) let ?full = f generateConfiguration -generateConfiguration :: Env' => IO AllHints+generateConfiguration :: (?size :: Int, ?letters :: Int, ?solver :: Solver, ?full :: Full)+ => IO AllHints generateConfiguration = do space <- shuffleM [ (i,j) | i <- sx, j<- sx] growPuzzle space [] -growPuzzle :: Env' => [(Int,Int)] -> [((Int,Int),Int)] -> IO AllHints+growPuzzle :: (?size :: Int, ?letters :: Int, ?solver :: Solver, ?full :: Full)+ => [(Int,Int)] -> [((Int,Int),Int)] -> IO AllHints -- reset search if we hit a hint selection with -- multiple solutions-growPuzzle [] _ = generateConfiguration+growPuzzle [] _ = putStrLn "did not find a puzzle" >> generateConfiguration growPuzzle (choice:space') entries = do letter <- randomRIO (0,?letters) let entries' = (choice,letter): entries@@ -247,41 +225,45 @@ else do -- We found an unsatisfiable set of hints. True <- solve ?solver (map entryValue entries)- generateHints--generateHints :: Env' => IO AllHints-generateHints = do- s@(Solution sol) <- getSolution (puzzle ?full)- deleteSolver ?solver- solver <- newSolver- let ?solver = solver- f <- genFull- conFull f- let ?full = f- removeSolution s- let space = [((3,i),getLetter (Vector.toList (sol ! i))) | i <- sx]- ++ [((0,i),getLetter [(sol!j)!i | j<-sx]) | i <- sx]- ++ [((1,i),getLetter (reverse $ Vector.toList (sol ! i))) | i <- sx]- ++ [((2,i),getLetter $ reverse [(sol!j)!i | j<-sx]) | i <- sx]- space' <- shuffleM space- sat <- solve ?solver (map hintValue space')- minimize sat space' []- where getLetter [] = error "Internal error: cannot find letter in solution!"- getLetter (Blank : r) = getLetter r- getLetter (Letter l : _) = l + 1+ s@(Solution sol) <- getSolution (puzzle ?full)+ removeSolution s+ let getLetters i = let soli = sol ! i+ in [((3,i),getLetter [soli!j | j<- sx]),+ ((0,i),getLetter [(sol!j)!i | j<-sx]),+ ((1,i),getLetter [soli!j | j<- sx_reverse]),+ ((2,i),getLetter [(sol!j)!i | j<-sx_reverse])]+ space = concatMap getLetters sx+ sat <- solve ?solver (map hintValue space)+ if sat then generateConfiguration -- not unique, start again+ else do -- check whether solution is it really unique+ -- (we excluded some previous solutions)+ deleteSolver ?solver+ solver <- newSolver+ let ?solver = solver+ f <- genFull+ conFull f+ removeSolution s+ sat <- solve ?solver (map hintValue space)+ if sat then generateConfiguration -- not unique, start again+ else do+ space' <- shuffleM space+ minimize space' []+ where getLetter = foldr getLetterRun (error "Internal error: cannot find letter in solution!")+ getLetterRun Blank r = r+ getLetterRun (Letter l) _ = l + 1 -- turn a hint position and letter into a literal-hintValue :: Env' => ((Int, Int), Int) -> Lit+hintValue :: (?full :: Full) => ((Int, Int), Int) -> Lit hintValue ((h,i),l) = (([top, right, bottom , left]!! h) (hints ?full) ! i) ! l -entryValue :: Env' => ((Int, Int), Int) -> Lit+entryValue :: (?full :: Full) => ((Int, Int), Int) -> Lit entryValue ((i,j),l) = (((puzzle ?full) ! i) ! j) ! l -minimize :: Env' => Bool -> [((Int, Int), Int)] -> [((Int, Int), Int)] -> IO AllHints-minimize True [] _ = generateConfiguration-minimize False [] result = do+minimize :: (?size :: Int, ?letters :: Int, ?solver :: Solver, ?full :: Full)+ => [((Int, Int), Int)] -> [((Int, Int), Int)] -> IO AllHints+minimize [] result = do -- We minimised the set of hints. Now we just verify that we indeed -- have a unique solution. deleteSolver ?solver@@ -297,9 +279,9 @@ sat' <- solve ?solver set when sat' (error "solution is wrong: not unique!") return(getAllHints ?size result)-minimize sat (h: r) acc = do sat' <- solve ?solver (map hintValue (r ++ acc))- if sat' then minimize sat r (h:acc)- else minimize sat' r acc+minimize (h: r) acc = do sat' <- solve ?solver (map hintValue (r ++ acc))+ if sat' then minimize r (h:acc)+ else minimize r acc main = do c <- getArgs