| module SAT.DPLL (dpll, SATResult(..)) where | |
| import SAT.CNF | |
| import SAT.UnitProp | |
| import qualified Data.Map.Strict as Map | |
| import Data.List (nub, sortOn) | |
| data SATResult | |
| = SAT (Map.Map Int Bool) | |
| | UNSAT | |
| deriving (Show) | |
| dpll :: CNF -> SATResult | |
| dpll (CNF clauses numVars) = solve Map.empty clauses | |
| where | |
| solve assignment [] = SAT assignment | |
| solve assignment cls = | |
| case unitPropagate assignment cls of | |
| Conflict -> UNSAT | |
| Propagated asgn' cls' -> | |
| if null cls' then SAT asgn' | |
| else | |
| let var = chooseVar asgn' cls' | |
| in case solve (Map.insert var True asgn') cls' of | |
| SAT a -> SAT a | |
| UNSAT -> solve (Map.insert var False asgn') cls' | |
| chooseVar :: Map.Map Int Bool -> [Clause] -> Int | |
| chooseVar asgn clauses = | |
| let allVars = nub $ map litVar $ concat clauses | |
| unassigned = filter (\v -> not (Map.member v asgn)) allVars | |
| in case unassigned of | |
| (v:_) -> v | |
| [] -> 0 | |