module Data.Boolean.SatSolver (
Boolean(..), SatSolver, Literal(..), literalVar, invLiteral, isPositiveLiteral, CNF, Clause, booleanToCNF,
newSatSolver, isSolved,
lookupVar, assertTrue, assertTrue', branchOnVar, selectBranchVar, solve, isSolvable
) where
import Data.List
import Data.Boolean
import Control.Monad.Writer
import qualified Data.IntMap as IM
data SatSolver = SatSolver { clauses :: CNF, bindings :: IM.IntMap Bool }
deriving Show
newSatSolver :: SatSolver
newSatSolver = SatSolver [] IM.empty
isSolved :: SatSolver -> Bool
isSolved = null . clauses
lookupVar :: Int -> SatSolver -> Maybe Bool
lookupVar name = IM.lookup name . bindings
assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver
assertTrue formula solver = do
newClauses <- foldl (addClause (bindings solver))
(return (clauses solver))
(booleanToCNF formula)
simplify (solver { clauses = newClauses })
assertTrue' :: MonadPlus m => CNF -> SatSolver -> m SatSolver
assertTrue' formula solver = do
newClauses <- foldl (addClause (bindings solver))
(return (clauses solver))
formula
simplify (solver { clauses = newClauses })
branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolver
branchOnVar name solver =
maybe (branchOnUnbound name solver)
(const (return solver))
(lookupVar name solver)
selectBranchVar :: SatSolver -> Int
selectBranchVar = literalVar . head . head . sortBy shorter . clauses
solve :: MonadPlus m => SatSolver -> m SatSolver
solve solver
| isSolved solver = return solver
| otherwise = branchOnUnbound (selectBranchVar solver) solver >>= solve
isSolvable :: SatSolver -> Bool
isSolvable = not . (null :: [a] -> Bool) . solve
addClause :: MonadPlus m => IM.IntMap Bool -> m [Clause] -> Clause -> m [Clause]
addClause binds mclauses newClause = do
oldClauses <- mclauses
let unboundLits = foldl (addUnbound binds) (Just []) newClause
maybe (return oldClauses)
(\lits -> guard (not (null lits)) >> return (lits:oldClauses))
unboundLits
addUnbound :: IM.IntMap Bool -> Maybe Clause -> Literal -> Maybe Clause
addUnbound binds mlits lit = do
lits <- mlits
maybe (Just (lit:lits))
(\b -> guard (b /= isPositiveLiteral lit) >> return lits)
(IM.lookup (literalVar lit) binds)
updateSolver :: MonadPlus m => CNF -> [(Int,Bool)] -> SatSolver -> m SatSolver
updateSolver cs bs solver = do
bs' <- foldr (uncurry insertBinding) (return (bindings solver)) bs
return $ solver { clauses = cs, bindings = bs' }
insertBinding :: MonadPlus m
=> Int -> Bool -> m (IM.IntMap Bool) -> m (IM.IntMap Bool)
insertBinding name newValue binds = do
bs <- binds
maybe (return (IM.insert name newValue bs))
(\oldValue -> do guard (oldValue==newValue); return bs)
(IM.lookup name bs)
simplify :: MonadPlus m => SatSolver -> m SatSolver
simplify solver = do
(cs,bs) <- runWriterT . simplifyClauses . clauses $ solver
updateSolver cs bs solver
simplifyClauses :: MonadPlus m => CNF -> WriterT [(Int,Bool)] m CNF
simplifyClauses [] = return []
simplifyClauses allClauses = do
let shortestClause = head . sortBy shorter $ allClauses
guard (not (null shortestClause))
if null (tail shortestClause)
then propagate (head shortestClause) allClauses >>= simplifyClauses
else return allClauses
propagate :: MonadPlus m => Literal -> CNF -> WriterT [(Int,Bool)] m CNF
propagate literal allClauses = do
tell [(literalVar literal, isPositiveLiteral literal)]
return (foldr prop [] allClauses)
where
prop c cs | literal `elem` c = cs
| otherwise = filter (invLiteral literal/=) c : cs
branchOnUnbound :: MonadPlus m => Int -> SatSolver -> m SatSolver
branchOnUnbound name solver =
guess (Pos name) solver `mplus` guess (Neg name) solver
guess :: MonadPlus m => Literal -> SatSolver -> m SatSolver
guess literal solver = do
(cs,bs) <- runWriterT (propagate literal (clauses solver) >>= simplifyClauses)
updateSolver cs bs solver
shorter :: [a] -> [a] -> Ordering
shorter [] [] = EQ
shorter [] _ = LT
shorter _ [] = GT
shorter (_:xs) (_:ys) = shorter xs ys