File size: 1,978 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 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 | module SAT.CDCL (cdcl, SATResult(..)) where
import SAT.CNF
import SAT.UnitProp
import qualified Data.Map.Strict as Map
import Data.List (nub)
data SATResult
= SAT (Map.Map Int Bool)
| UNSAT [Clause]
deriving (Show)
data DecisionLevel = DecisionLevel
{ dlVar :: Int
, dlVal :: Bool
, dlLevel :: Int
, dlImplied :: [(Int, Bool)]
} deriving (Show)
cdcl :: CNF -> SATResult
cdcl (CNF clauses numVars) = go Map.empty clauses [] 0
where
go asgn cls trail level =
case unitPropagate asgn cls of
Conflict ->
if level == 0 then UNSAT cls
else
let learned = analyzeConflict trail cls
newLevel = backtrackLevel trail learned
asgn' = backtrack asgn trail newLevel
trail' = take newLevel trail
in go asgn' (learned : cls) trail' newLevel
Propagated asgn' cls' ->
if null cls' then SAT asgn'
else
let var = chooseVar asgn' cls'
level' = level + 1
asgn'' = Map.insert var True asgn'
dl = DecisionLevel var True level' []
in go asgn'' cls' (trail ++ [dl]) level'
analyzeConflict :: [DecisionLevel] -> [Clause] -> Clause
analyzeConflict trail _ =
case trail of
[] -> []
dls -> let lastDl = last dls
in [Neg (dlVar lastDl)]
backtrackLevel :: [DecisionLevel] -> Clause -> Int
backtrackLevel trail _ = max 0 (length trail - 1)
backtrack :: Map.Map Int Bool -> [DecisionLevel] -> Int -> Map.Map Int Bool
backtrack asgn trail level =
let toRemove = drop level trail
vars = map dlVar toRemove
in foldr Map.delete asgn vars
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
|