File size: 1,017 Bytes
56de343 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 | 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
|