diff --git a/abc-puzzle.cabal b/abc-puzzle.cabal --- a/abc-puzzle.cabal +++ b/abc-puzzle.cabal @@ -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 + (). + The implementation uses the MiniSat SAT solver () + 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 diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -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 ++ " " - ++ "\n\nThe the number of letters may not be larger than the puzzle size."