----------------------------------------------------------------------------- -- | -- Module : Documentation.SBV.Examples.Puzzles.Euler185 -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- A solution to Project Euler problem #185: ----------------------------------------------------------------------------- module Documentation.SBV.Examples.Puzzles.Euler185 where import Data.Char (ord) import Data.SBV -- | The given guesses and the correct digit counts, encoded as a simple list. guesses :: [(String, SWord8)] guesses = [ ("5616185650518293", 2), ("3847439647293047", 1), ("5855462940810587", 3) , ("9742855507068353", 3), ("4296849643607543", 3), ("3174248439465858", 1) , ("4513559094146117", 2), ("7890971548908067", 3), ("8157356344118483", 1) , ("2615250744386899", 2), ("8690095851526254", 3), ("6375711915077050", 1) , ("6913859173121360", 1), ("6442889055042768", 2), ("2321386104303845", 0) , ("2326509471271448", 2), ("5251583379644322", 2), ("1748270476758276", 3) , ("4895722652190306", 1), ("3041631117224635", 3), ("1841236454324589", 3) , ("2659862637316867", 2) ] -- | Encode the problem, note that we check digits are within 0-9 as -- we use 8-bit words to represent them. Otherwise, the constraints are simply -- generated by zipping the alleged solution with each guess, and making sure the -- number of matching digits match what's given in the problem statement. euler185 :: Symbolic SBool euler185 = do soln <- mkExistVars 16 return \$ sAll digit soln .&& sAnd (map (genConstr soln) guesses) where genConstr a (b, c) = sum (zipWith eq a b) .== (c :: SWord8) digit x = (x :: SWord8) .>= 0 .&& x .<= 9 eq x y = ite (x .== fromIntegral (ord y - ord '0')) 1 0 -- | Print out the solution nicely. We have: -- -- >>> solveEuler185 -- 4640261571849533 -- Number of solutions: 1 solveEuler185 :: IO () solveEuler185 = do res <- allSat euler185 cnt <- displayModels disp res putStrLn \$ "Number of solutions: " ++ show cnt where disp _ (_, ss) = putStrLn \$ concatMap show (ss :: [Word8])