abc-puzzle 0.1 → 0.2
raw patch · 2 files changed
+152/−96 lines, 2 filesdep +random-shuffle
Dependencies added: random-shuffle
Files
- abc-puzzle.cabal +9/−4
- src/Main.hs +143/−92
abc-puzzle.cabal view
@@ -1,7 +1,11 @@ name: abc-puzzle-version: 0.1-synopsis: Generate instances of the ABC logic puzzle.--- description: +version: 0.2+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>).+ The implementation uses the MiniSat SAT solver (<http://minisat.se/>)+ to guide the search for a valid puzzle. Each generated puzzle has one+ unique solution. homepage: https://github.com/pa-ba/abc-puzzle bug-reports: https://github.com/pa-ba/abc-puzzle/issues license: BSD3@@ -19,7 +23,8 @@ 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+ build-depends: base >=4.7 && <5, vector >=0.10, minisat >=0.1, Safe >=0.1, random >=1.0, + random-shuffle >= 0.0.4 default-language: Haskell2010 source-repository head
src/Main.hs view
@@ -7,11 +7,12 @@ import Control.Monad import Data.List import qualified Data.Vector as Vector-import Data.Vector (Vector, (!))+import Data.Vector (Vector, (!),(//)) import MiniSat import Safe import System.Environment +import System.Random.Shuffle import System.Random type Puzzle = Vector (Vector Field) -- rows of columns@@ -41,8 +42,8 @@ genFull :: Env => IO Full genFull = liftM2 Full genPuzzle genHints -addClause' :: Env => [Lit] -> IO Bool-addClause' = addClause ?solver+addClause' :: Env => [Lit] -> IO ()+addClause' c = addClause ?solver c >> return () addClauses :: Env => [[Lit]] -> IO () addClauses = mapM_ addClause'@@ -96,6 +97,33 @@ conFields :: Env => 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 l1 l2 = do @@ -125,22 +153,27 @@ show Blank = " " show (Letter l) = [iterate succ 'A' !! l] -newtype Solution = Solution {unSolution :: [[Entry]]}+newtype Solution = Solution {unSolution :: Vector (Vector (Entry))} instance Show Solution where- show = unlines . map (unwords . map show) . unSolution+ show = unlines . map (unwords . map show . Vector.toList) . Vector.toList . unSolution getSolution :: Env => Puzzle -> IO Solution-getSolution p = liftM Solution $ sequence [ sequence [ getEntry f | f <- Vector.toList r] | r <- Vector.toList p ]+getSolution p = liftM Solution $ liftM Vector.fromList $ + sequence [ liftM Vector.fromList $ + sequence [ getEntry f | f <- Vector.toList r] | r <- Vector.toList p ] getHints :: Env => Vector Field -> IO [Entry] getHints h = sequence [ getEntry f | f <- Vector.toList h] -getAllHints :: Env => Hints -> IO AllHints-getAllHints (Hints t r b l) = liftM4 AllHints (getHints t) (getHints r) (getHints b) (getHints l)+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 -data AllHints = AllHints {atop, aright, abottom, aleft :: [Entry]} deriving Show +data AllHints = AllHints {atop, aright, abottom, aleft :: Vector Entry, hintSize :: Int} deriving Show+ getEntry :: Env => Field -> IO Entry getEntry l = do Just b <- modelValue ?solver (l!0) if b then return Blank else getLetter@@ -149,35 +182,40 @@ let Just n = findIndex (== Just True) res return $ Letter n --- To be called after a successful 'solve'. It tries to find another--- solution.-solveAgain :: Solver -> [Lit] -> IO Bool-solveAgain solver set = - do n <- minisat_num_vars solver - addClause solver =<<- sequence [(modelValue solver lit >>= (\ (Just b) ->- return (if b then neg lit else lit)))- | lit <- map (MkLit . fromInteger . toInteger) [0..(n-1)]]- solve solver set+-- Adds clause to avoid the currently found solution.+removeCurrentSolution :: Env => IO Bool+removeCurrentSolution = do + n <- minisat_num_vars ?solver + addClause ?solver =<<+ sequence [(modelValue ?solver lit >>= (\ (Just b) ->+ return (if b then neg lit else lit)))+ | lit <- map (MkLit . fromInteger . toInteger) [0..(n-1)]] +entryToInt :: Entry -> Int+entryToInt Blank = 0+entryToInt (Letter i) = i + 1++removeSolution :: Env' => 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) = " | " ++ (intercalate " | " $ map show t) ++ " | \n"- ++ rule- ++ intercalate rule rows- ++ rule- ++ " | " ++ (intercalate " | " $ map show b) ++ " | \n"+prettyHints (AllHints t r b l s) = + " | " ++ (intercalate " | " $ map show $ Vector.toList t) ++ " | \n"+ ++ rule+ ++ intercalate rule rows+ ++ rule+ ++ " | " ++ (intercalate " | " $ map show $ Vector.toList 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") l r- size = length t+ rows = zipWith (\l r -> show l ++ divider ++ show r ++ "\n") (Vector.toList l) (Vector.toList r)+ size = Vector.length t -type Env' = (Env, ?space :: ([(Int,Int)]), - ?hints :: [((Int,Int),Int)], ?full :: Full)+type Env' = (Env, ?full :: Full) --- complete list of hint positions-hintPositions :: Env => [(Int,Int)]-hintPositions = [ (side,i) | side <- [0..3], i<- sx] :: [(Int,Int)]+-- complete list of entry positions search :: Int -> Int -> IO AllHints@@ -188,78 +226,91 @@ ?letters = letters f <- genFull conFull f+ conAmbFields (puzzle f) let ?full = f- ?space = hintPositions- ?hints = []- growHints+ generateConfiguration -growHints :: Env' => IO AllHints-growHints = do case ?space of- -- reset search if we hit a hint selection with- -- multiple solutions- [] -> let ?space = hintPositions- ?hints = []- in growHints- _ -> do- (choice, space') <- pick ?space- letter <- randomRIO (1,?letters)- let hints' = (choice,letter): ?hints- sat <- solve ?solver (map hintValue hints')- if sat then let ?space = space'- ?hints = hints'- in growHints- else do - -- We found an unsatisfiable set of hints. We- -- backtrack and check whether we found a set of- -- hints with a unique solution.- let set = map hintValue ?hints- solve ?solver set- sat <- solveAgain ?solver set- if sat then do - -- Solution is not unique. Reset the- -- solver and start growing the hints.- deleteSolver ?solver- solver <- newSolver- let ?solver = solver- f <- genFull- conFull f- let ?full = f- growHints- else minimize ?hints []+generateConfiguration :: Env' => IO AllHints+generateConfiguration = do space <- shuffleM [ (i,j) | i <- sx, j<- sx]+ growPuzzle space []+++growPuzzle :: Env' => [(Int,Int)] -> [((Int,Int),Int)] -> IO AllHints+-- reset search if we hit a hint selection with+-- multiple solutions+growPuzzle [] _ = generateConfiguration+growPuzzle (choice:space') entries = do+ letter <- randomRIO (0,?letters)+ let entries' = (choice,letter): entries+ sat <- solve ?solver (map entryValue entries')+ if sat then growPuzzle space' entries'+ 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+ + -- turn a hint position and letter into a literal hintValue :: Env' => ((Int, Int), Int) -> Lit hintValue ((h,i),l) = (([top, right, bottom , left]!! h) (hints ?full) ! i) ! l -pick l = do i <- randomRIO (0,length l -1)- let (l1, choice:l2) = splitAt i l- return (choice, l1++l2)+entryValue :: Env' => ((Int, Int), Int) -> Lit+entryValue ((i,j),l) = (((puzzle ?full) ! i) ! j) ! l -minimize :: Env' => [((Int, Int), Int)] -> [((Int, Int), Int)] -> IO AllHints-minimize [] acc = do - -- We minimised the set of hints. Now we just verify that we indeed- -- have a unique solution.- deleteSolver ?solver- solver <- newSolver- let ?solver = solver- f <- genFull- conFull f- let set = map hintValue acc- sat <- solve ?solver set- sat' <- solveAgain ?solver set- when (not sat || sat') (error "solution is wrong")- getAllHints (hints f)-minimize (h: r) acc = do sat <- solve ?solver (map hintValue (r ++ acc))- if sat then minimize r (h:acc)- else minimize r acc +minimize :: Env' => Bool -> [((Int, Int), Int)] -> [((Int, Int), Int)] -> IO AllHints+minimize True [] _ = generateConfiguration+minimize False [] result = do+ -- We minimised the set of hints. Now we just verify that we indeed+ -- have a unique solution.+ deleteSolver ?solver+ solver <- newSolver+ let ?solver = solver+ f <- genFull+ conFull f+ let set = map hintValue result+ sat <- solve ?solver set+ when (not sat) (error "solution is wrong: not satisfiable!")+ s <- getSolution (puzzle ?full)+ removeSolution s+ 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 + main = do c <- getArgs case c of - [size,letters] -> case (readMay size, readMay letters) of- (Just size, Just letters) | size >= letters ->- search size letters >>= (putStr . prettyHints)- _ -> usage+ [size,letters] -> + case (readMay size, readMay letters) of+ (Just size, Just letters)+ | size < letters -> putStrLn "The the number of letters may not be larger than the puzzle size."+ | letters < 1 -> putStrLn "The the number of letters must be a positive integer"+ | otherwise -> search size letters >>= (putStr . prettyHints)+ _ -> usage _ -> usage where usage = do name <- getProgName putStrLn $ "usage: " ++ name ++ " <puzzle size> <number of letters>"- ++ "\n\nThe the number of letters may not be larger than the puzzle size."