module Funsat.Solver
#ifndef TESTING
(
solve
, solve1
, Solution(..)
, verify
, VerifyError(..)
, DPLLConfig(..)
, defaultConfig
, Stats(..)
, ShowWrapped(..)
, statTable
, statSummary
)
#endif
where
import Control.Arrow ((&&&))
import Control.Exception (assert)
import Control.Monad.Error hiding ((>=>), forM_, runErrorT)
import Control.Monad.MonadST( MonadST(..) )
import Control.Monad.ST.Strict
import Control.Monad.State.Lazy hiding ((>=>), forM_)
import Data.Array.ST
import Data.Array.Unboxed
import Data.Foldable hiding (sequence_)
import Data.Graph.Inductive.Graph( DynGraph, Graph )
import Data.Int (Int64)
import Data.List (intercalate, nub, tails, sortBy, intersect, sort)
import Data.Map (Map)
import Data.Maybe
import Data.Ord (comparing)
import Data.STRef
import Data.Sequence (Seq)
import Data.Set (Set)
import Debug.Trace (trace)
import Funsat.Monad
import Funsat.Utils
import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace )
import Funsat.Types
import Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum)
import Funsat.Resolution( ResolutionError(..) )
import Text.Printf( printf )
import qualified Data.Graph.Inductive.Graph as Graph
import qualified Data.Graph.Inductive.Query.DFS as DFS
import qualified Data.Foldable as Fl
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import qualified Funsat.Resolution as Resolution
import qualified Text.Tabular as Tabular
solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace)
solve cfg fIn =
either (error "no solution") id $
runST $
evalSSTErrMonad
(do sol <- stepToSolution $ do
initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0
(a, isUnsat) <- initialState initialAssignment
if isUnsat then return (Right (Unsat a))
else solveStep initialAssignment
stats <- extractStats
case sol of
Sat _ -> return (sol, stats, Nothing)
Unsat _ -> do resTrace <- constructResTrace sol
return (sol, stats, Just resTrace))
SC{ cnf=f{clauses = Set.empty}, dl=[]
, watches=undefined, learnt=undefined, propQ=Seq.empty
, trail=[], numConfl=0, level=undefined, numConflTotal=0
, numDecisions=0, numImpl=0
, reason=Map.empty, varOrder=undefined
, resolutionTrace=PartialResolutionTrace 1 [] [] Map.empty
, dpllConfig=cfg }
where
f = preprocessCNF fIn
initialState :: MAssignment s -> DPLLMonad s (IAssignment, Bool)
initialState m = do
initialLevel <- liftST $ newSTUArray (V 1, V (numVars f)) noLevel
modify $ \s -> s{level = initialLevel}
initialWatches <- liftST $ newSTArray (L ( (numVars f)), L (numVars f)) []
modify $ \s -> s{ watches = initialWatches }
initialLearnts <- liftST $ newSTArray (L ( (numVars f)), L (numVars f)) []
modify $ \s -> s{ learnt = initialLearnts }
initialVarOrder <- liftST $ newSTUArray (V 1, V (numVars f)) initialActivity
modify $ \s -> s{ varOrder = VarOrder initialVarOrder }
(`catchError` (const $ liftST (unsafeFreezeAss m) >>= \a -> return (a,True))) $ do
forM_ (clauses f)
(\c -> do cid <- nextTraceId
isConsistent <- watchClause m (c, cid) False
when (not isConsistent)
(do traceClauseId cid
throwError (L 0, [], 0)))
a <- liftST (unsafeFreezeAss m)
return (a, False)
solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace)
solve1 f = solve (defaultConfig f) f
data DPLLConfig = Cfg
{ configRestart :: !Int64
, configRestartBump :: !Double
, configUseVSIDS :: !Bool
, configUseRestarts :: !Bool }
deriving Show
defaultConfig :: CNF -> DPLLConfig
defaultConfig _f = Cfg { configRestart = 100
, configRestartBump = 1.5
, configUseVSIDS = True
, configUseRestarts = True }
preprocessCNF :: CNF -> CNF
preprocessCNF f = f{clauses = simpClauses (clauses f)}
where simpClauses = Set.map nub
simplifyDB :: IAssignment -> DPLLMonad s ()
simplifyDB mFr = do
n <- numVars `liftM` gets cnf
s <- get
liftST . forM_ [V 1 .. V n] $ \i -> when (mFr!i /= 0) $ do
let l = L (mFr!i)
filterL _i = map (\(p, c, cid) -> (p, filter (/= negate l) c, cid))
modifyArray (learnt s) l filterL
writeArray (learnt s) (negate l) []
solveStep :: MAssignment s -> DPLLMonad s (Step s)
solveStep m = do
unsafeFreezeAss m >>= solveStepInvariants
conf <- gets dpllConfig
let selector = if configUseVSIDS conf then select else selectStatic
maybeConfl <- bcp m
mFr <- unsafeFreezeAss m
s <- get
voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze . varOrderArr . varOrder $ s)
newState $
unsat maybeConfl s ==> postProcessUnsat maybeConfl
>< maybeConfl >=> backJump m
>< selector mFr voFr >=> decide m
where
newState stepMaybe =
case stepMaybe of
Nothing -> unsafeFreezeAss m >>= return . Right . Sat
Just step -> do
r <- step
case r of
Nothing -> do a <- liftST (unsafeFreezeAss m)
return . Right . Unsat $ a
Just m -> return . Left $ m
postProcessUnsat :: Maybe (Lit, Clause, ClauseId) -> DPLLMonad s (Maybe a)
postProcessUnsat maybeConfl = do
traceClauseId $ (thd . fromJust) maybeConfl
return Nothing
where
thd (_,_,i) = i
solveStepInvariants :: IAssignment -> DPLLMonad s ()
solveStepInvariants _m = assert True $ do
s <- get
assert ((length . dl) s == (length . nub . dl) s) $
assert ((length . trail) s == (length . nub . trail) s) $
return ()
type Step s = Either (MAssignment s) Solution
data Solution = Sat IAssignment | Unsat IAssignment deriving (Eq)
finalAssignment :: Solution -> IAssignment
finalAssignment (Sat a) = a
finalAssignment (Unsat a) = a
stepToSolution :: DPLLMonad s (Step s) -> DPLLMonad s Solution
stepToSolution stepAction = do
step <- stepAction
useRestarts <- gets (configUseRestarts . dpllConfig)
restart <- uncurry ((>=)) `liftM`
gets (numConfl &&& (configRestart . dpllConfig))
case step of
Left m -> do when (useRestarts && restart)
(do _stats <- extractStats
resetState m)
stepToSolution (solveStep m)
Right s -> return s
where
resetState m = do
modify $ \s -> s{ numConfl = 0 }
modifySlot dpllConfig $ \s c ->
s{ dpllConfig = c{ configRestart = ceiling (configRestartBump c
* fromIntegral (configRestart c))
} }
lvl :: FrozenLevelArray <- gets level >>= liftST . unsafeFreeze
undoneLits <- takeWhile (\l -> lvl ! (var l) > 0) `liftM` gets trail
forM_ undoneLits $ const (undoOne m)
modify $ \s -> s{ dl = [], propQ = Seq.empty }
compactDB
unsafeFreezeAss m >>= simplifyDB
instance Show Solution where
show (Sat a) = "satisfiable: " ++ showAssignment a
show (Unsat _) = "unsatisfiable"
type Level = Int
type LevelArray s = STUArray s Var Level
type FrozenLevelArray = UArray Var Level
noLevel :: Level
noLevel = 1
newtype VarOrder s = VarOrder { varOrderArr :: STUArray s Var Double }
deriving Show
newtype FrozenVarOrder = FrozenVarOrder (UArray Var Double)
deriving Show
type WatchedPair s = (STRef s (Lit, Lit), Clause, ClauseId)
type WatchArray s = STArray s Lit [WatchedPair s]
data PartialResolutionTrace = PartialResolutionTrace
{ resTraceIdCount :: !Int
, resTrace :: ![Int]
, resTraceOriginalSingles :: ![(Clause, ClauseId)]
, resSourceMap :: Map ClauseId [ClauseId] }
deriving (Show)
type ReasonMap = Map Var (Clause, ClauseId)
type ClauseId = Int
data FunsatState s = SC
{ cnf :: CNF
, dl :: [Lit]
, watches :: WatchArray s
, learnt :: WatchArray s
, propQ :: Seq Lit
, level :: LevelArray s
, trail :: [Lit]
, reason :: ReasonMap
, numConfl :: !Int64
, numConflTotal :: !Int64
, numDecisions :: !Int64
, numImpl :: !Int64
, varOrder :: VarOrder s
, resolutionTrace :: PartialResolutionTrace
, dpllConfig :: DPLLConfig
}
deriving Show
instance Show (STRef s a) where
show = const "<STRef>"
instance Show (STUArray s Var Int) where
show = const "<STUArray Var Int>"
instance Show (STUArray s Var Double) where
show = const "<STUArray Var Double>"
instance Show (STArray s a b) where
show = const "<STArray>"
type DPLLMonad s = SSTErrMonad (Lit, Clause, ClauseId) (FunsatState s) s
bcpLit :: MAssignment s
-> Lit
-> DPLLMonad s (Maybe (Lit, Clause, ClauseId))
bcpLit m l = do
ws <- gets watches ; ls <- gets learnt
clauses <- liftST $ readArray ws l
learnts <- liftST $ readArray ls l
liftST $ do writeArray ws l [] ; writeArray ls l []
(`catchError` return . Just) $ do
forM_ (tails clauses) (updateWatches
(\ f l -> liftST $ modifyArray ws l (const f)))
forM_ (tails learnts) (updateWatches
(\ f l -> liftST $ modifyArray ls l (const f)))
return Nothing
where
updateWatches _ [] = return ()
updateWatches alter (annCl@(watchRef, c, cid) : restClauses) = do
mFr <- unsafeFreezeAss m
q <- liftST $ do (x, y) <- readSTRef watchRef
return $ if x == l then y else x
if negate q `isTrueUnder` mFr
then alter (annCl:) l
else
case find (\x -> x /= negate q && x /= negate l
&& not (x `isFalseUnder` mFr)) c of
Just l' -> do
liftST $ writeSTRef watchRef (q, negate l')
alter (annCl:) (negate l')
Nothing -> do
modify $ \s -> s{ numImpl = numImpl s + 1 }
alter (annCl:) l
isConsistent <- enqueue m (negate q) (Just (c, cid))
when (not isConsistent) $ do
alter (restClauses ++) l
clearQueue
throwError (negate q, c, cid)
bcp :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause, ClauseId))
bcp m = do
q <- gets propQ
if Seq.null q then return Nothing
else do
p <- dequeue
bcpLit m p >>= maybe (bcp m) (return . Just)
select :: IAssignment -> FrozenVarOrder -> Maybe Var
select = varOrderGet
selectStatic :: IAssignment -> a -> Maybe Var
selectStatic m _ = find (`isUndefUnder` m) (range . bounds $ m)
decide :: MAssignment s -> Var -> DPLLMonad s (Maybe (MAssignment s))
decide m v = do
let ld = L (unVar v)
(SC{dl=dl}) <- get
modify $ \s -> s{ dl = ld:dl
, numDecisions = numDecisions s + 1 }
enqueue m ld Nothing
return $ Just m
backJump :: MAssignment s
-> (Lit, Clause, ClauseId)
-> DPLLMonad s (Maybe (MAssignment s))
backJump m c@(_, _conflict, _) = get >>= \(SC{dl=dl, reason=_reason}) -> do
_theTrail <- gets trail
modify $ \s -> s{ numConfl = numConfl s + 1
, numConflTotal = numConflTotal s + 1 }
levelArr :: FrozenLevelArray <- do s <- get
liftST $ unsafeFreeze (level s)
(learntCl, learntClId, newLevel) <-
do mFr <- unsafeFreezeAss m
analyse mFr levelArr dl c
s <- get
let numDecisionsToUndo = length dl newLevel
dl' = drop numDecisionsToUndo dl
undoneLits = takeWhile (\lit -> levelArr ! (var lit) > newLevel) (trail s)
forM_ undoneLits $ const (undoOne m)
mFr <- unsafeFreezeAss m
assert (numDecisionsToUndo > 0) $
assert (not (null learntCl)) $
assert (learntCl `isUnitUnder` mFr) $
modify $ \s -> s{ dl = dl' }
mFr <- unsafeFreezeAss m
watchClause m (learntCl, learntClId) True
enqueue m (getUnit learntCl mFr) (Just (learntCl, learntClId))
return $ Just m
doWhile :: (Monad m) => m () -> m Bool -> m ()
doWhile body test = do
body
shouldContinue <- test
when shouldContinue $ doWhile body test
analyse :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause, ClauseId)
-> DPLLMonad s (Clause, ClauseId, Int)
analyse mFr levelArr dlits (cLit, cClause, cCid) = do
st <- get
m <- liftST $ unsafeThawAss mFr
a <- firstUIPBFS m (numVars . cnf $ st) (reason st)
return a
where
firstUIPBFS :: MAssignment s -> Int -> ReasonMap
-> DPLLMonad s (Clause, ClauseId, Int)
firstUIPBFS m nVars reasonMap = do
resolveSourcesR <- liftST $ newSTRef []
let addResolveSource clauseId =
liftST $ modifySTRef resolveSourcesR (clauseId:)
seenArr <- liftST $ newSTUArray (V 1, V nVars) False
counterR <- liftST $ newSTRef 0
pR <- liftST $ newSTRef cLit
out_learnedR <- liftST $ newSTRef []
out_btlevelR <- liftST $ newSTRef 0
let reasonL l = if l == cLit then (cClause, cCid)
else
let (r, rid) =
Map.findWithDefault (error "analyse: reasonL")
(var l) reasonMap
in (r `without` l, rid)
(`doWhile` (liftM (> 0) (liftST $ readSTRef counterR))) $
do p <- liftST $ readSTRef pR
let (p_reason, p_rid) = reasonL p
traceClauseId p_rid
addResolveSource p_rid
forM_ p_reason (bump . var)
liftST . forM_ p_reason $ \q -> do
seenq <- readArray seenArr (var q)
when (not seenq) $
do writeArray seenArr (var q) True
if levelL q == currentLevel
then modifySTRef counterR (+ 1)
else if levelL q > 0
then do modifySTRef out_learnedR (q:)
modifySTRef out_btlevelR $ max (levelL q)
else return ()
(`doWhile` (liftST (readSTRef pR >>= readArray seenArr . var)
>>= return . not)) $ do
p <- head `liftM` gets trail
liftST $ writeSTRef pR p
undoOne m
liftST $ modifySTRef counterR (\c -> c 1)
p <- liftST $ readSTRef pR
liftST $ modifySTRef out_learnedR (negate p:)
bump . var $ p
out_learned <- liftST $ readSTRef out_learnedR
out_btlevel <- liftST $ readSTRef out_btlevelR
learnedClauseId <- nextTraceId
storeResolvedSources resolveSourcesR learnedClauseId
traceClauseId learnedClauseId
return (out_learned, learnedClauseId, out_btlevel)
currentLevel = length dlits
levelL l = levelArr!(var l)
storeResolvedSources rsR clauseId = do
rsReversed <- liftST $ readSTRef rsR
modifySlot resolutionTrace $ \s rt ->
s{resolutionTrace =
rt{resSourceMap =
Map.insert clauseId (reverse rsReversed) (resSourceMap rt)}}
undoOne :: MAssignment s -> DPLLMonad s ()
undoOne m = do
trl <- gets trail
lvl <- gets level
case trl of
[] -> error "undoOne of empty trail"
(l:trl') -> do
liftST $ m `unassign` l
liftST $ writeArray lvl (var l) noLevel
modify $ \s ->
s{ trail = trl'
, reason = Map.delete (var l) (reason s) }
bump :: Var -> DPLLMonad s ()
bump v = varOrderMod v (+ varInc)
varInc :: Double
varInc = 1.0
unsat :: Maybe a -> FunsatState s -> Bool
unsat maybeConflict (SC{dl=dl}) = isUnsat
where isUnsat = (null dl && isJust maybeConflict)
compactDB :: DPLLMonad s ()
compactDB = do
n <- numVars `liftM` gets cnf
lArr <- gets learnt
clauses <- liftST $ (nub . Fl.concat) `liftM`
forM [L ( n) .. L n]
(\v -> do val <- readArray lArr v ; writeArray lArr v []
return val)
let clauses' = take (length clauses `div` 2)
$ sortBy (comparing (length . (\(_,s,_) -> s))) clauses
liftST $ forM_ clauses'
(\ wCl@(r, _, _) -> do
(x, y) <- readSTRef r
modifyArray lArr x $ const (wCl:)
modifyArray lArr y $ const (wCl:))
watchClause :: MAssignment s
-> (Clause, ClauseId)
-> Bool
-> DPLLMonad s Bool
watchClause m (c, cid) isLearnt = do
case c of
[] -> return True
[l] -> do result <- enqueue m l (Just (c, cid))
levelArr <- gets level
liftST $ writeArray levelArr (var l) 0
when (not isLearnt) (
modifySlot resolutionTrace $ \s rt ->
s{resolutionTrace=rt{resTraceOriginalSingles=
(c,cid): resTraceOriginalSingles rt}})
return result
_ -> do let p = (negate (c !! 0), negate (c !! 1))
_insert annCl@(_, cl) list
| any (\(_, c) -> cl == c) list = list
| otherwise = annCl:list
r <- liftST $ newSTRef p
let annCl = (r, c, cid)
addCl arr = do modifyArray arr (fst p) $ const (annCl:)
modifyArray arr (snd p) $ const (annCl:)
get >>= liftST . addCl . (if isLearnt then learnt else watches)
return True
enqueue :: MAssignment s
-> Lit
-> Maybe (Clause, ClauseId)
-> DPLLMonad s Bool
enqueue m l r = do
mFr <- unsafeFreezeAss m
case l `statusUnder` mFr of
Right b -> return b
Left () -> do
liftST $ m `assign` l
gets (level &&& (length . dl)) >>= \(levelArr, dlInt) ->
liftST (writeArray levelArr (var l) dlInt)
modify $ \s -> s{ trail = l : (trail s)
, propQ = propQ s Seq.|> l }
when (isJust r) $
modifySlot reason $ \s m -> s{reason = Map.insert (var l) (fromJust r) m}
return True
dequeue :: DPLLMonad s Lit
dequeue = do
q <- gets propQ
case Seq.viewl q of
Seq.EmptyL -> error "dequeue of empty propQ"
top Seq.:< q' -> do
modify $ \s -> s{propQ = q'}
return top
clearQueue :: DPLLMonad s ()
clearQueue = modify $ \s -> s{propQ = Seq.empty}
varOrderMod :: Var -> (Double -> Double) -> DPLLMonad s ()
varOrderMod v f = do
vo <- varOrderArr `liftM` gets varOrder
vActivity <- liftST $ readArray vo v
when (f vActivity > 1e100) $ rescaleActivities vo
liftST $ writeArray vo v (f vActivity)
where
rescaleActivities vo = liftST $ do
indices <- range `liftM` getBounds vo
forM_ indices (\i -> modifyArray vo i $ const (* 1e-100))
varOrderGet :: IAssignment -> FrozenVarOrder -> Maybe Var
varOrderGet mFr (FrozenVarOrder voFr) =
(`fmap` goUndef highestIndex) $ \start -> goActivity start start
where
highestIndex = snd . bounds $ voFr
maxActivity v v' = if voFr!v > voFr!v' then v else v'
goActivity !(V 0) !h = h
goActivity !v@(V n) !h = if v `isUndefUnder` mFr
then goActivity (V $! n1) (v `maxActivity` h)
else goActivity (V $! n1) h
goUndef !(V 0) = Nothing
goUndef !v@(V n) | v `isUndefUnder` mFr = Just v
| otherwise = goUndef (V $! n1)
nextTraceId :: DPLLMonad s Int
nextTraceId = do
counter <- gets (resTraceIdCount . resolutionTrace)
modifySlot resolutionTrace $ \s rt ->
s{ resolutionTrace = rt{ resTraceIdCount = succ counter }}
return $! counter
traceClauseId :: ClauseId -> DPLLMonad s ()
traceClauseId cid = do
modifySlot resolutionTrace $ \s rt ->
s{resolutionTrace = rt{ resTrace = [cid] }}
(==>) :: (Monad m) => Bool -> m a -> Maybe (m a)
(==>) b amb = guard b >> return amb
infixr 6 ==>
(>=>) :: (Monad m) => Maybe a -> (a -> m b) -> Maybe (m b)
(>=>) = flip fmap
infixr 6 >=>
(><) :: (Monad m) => Maybe (m a) -> Maybe (m a) -> Maybe (m a)
a1 >< a2 =
case (a1, a2) of
(Nothing, Nothing) -> Nothing
(Just _, _) -> a1
_ -> a2
infixl 5 ><
data Cut f gr a b =
Cut { reasonSide :: f Graph.Node
, conflictSide :: f Graph.Node
, cutUIP :: Graph.Node
, cutGraph :: gr a b }
instance (Show (f Graph.Node), Show (gr a b)) => Show (Cut f gr a b) where
show (Cut { conflictSide = c, cutUIP = uip }) =
"Cut (uip=" ++ show uip ++ ", cSide=" ++ show c ++ ")"
uipCut :: (Graph gr) =>
[Lit]
-> FrozenLevelArray
-> gr a b
-> Graph.Node
-> Graph.Node
-> Cut Set gr a b
uipCut dlits levelArr conflGraph conflNode uip =
Cut { reasonSide = Set.filter (\i -> levelArr!(V $ abs i) > 0) $
allNodes Set.\\ impliedByUIP
, conflictSide = impliedByUIP
, cutUIP = uip
, cutGraph = conflGraph }
where
impliedByUIP = Set.insert extraNode $
Set.fromList $ tail $ DFS.reachable uip conflGraph
extraNode = if L (negate conflNode) `elem` dlits || negate conflNode == uip
then conflNode
else negate conflNode
allNodes = Set.fromList $ Graph.nodes conflGraph
cutLearn :: (Graph gr, Foldable f) => IAssignment -> FrozenLevelArray
-> Cut f gr a b -> (Clause, Int)
cutLearn a levelArr cut =
( clause
, maximum0 (map (levelArr!) . (`without` V (abs $ cutUIP cut)) . map var $ clause) )
where
clause =
foldl' (\ls i ->
if any (`elem` conflictSide cut) (Graph.suc (cutGraph cut) i)
then L (negate $ a!(V $ abs i)):ls
else ls)
[] (reasonSide cut)
maximum0 [] = 0
maximum0 xs = maximum xs
data CGNodeAnnot = CGNA Lit Level
instance Show CGNodeAnnot where
show (CGNA (L 0) _) = "lambda"
show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")"
mkConflGraph :: DynGraph gr =>
IAssignment
-> FrozenLevelArray
-> Map Var Clause
-> [Lit]
-> (Lit, Clause)
-> gr CGNodeAnnot ()
mkConflGraph mFr lev reasonMap _dlits (cLit, confl) =
Graph.mkGraph nodes' edges'
where
nodes' =
((0, CGNA (L 0) (1)) :) $
((unLit cLit, CGNA cLit (1)) :) $
((negate (unLit cLit), CGNA (negate cLit) (lev!(var cLit))) :) $
map (\v -> (unVar v, CGNA (varToLit v) (lev!v))) $
filter (\v -> v /= var cLit) $
toList nodeSet'
(nodeSet', edges') =
mkGr Set.empty (Set.empty, [ (unLit cLit, 0, ())
, ((negate . unLit) cLit, 0, ()) ])
[negate cLit, cLit]
varToLit v = (if v `isTrueUnder` mFr then id else negate) $ L (unVar v)
mkGr _ ne [] = ne
mkGr (seen :: Set Graph.Node) ne@(nodes, edges) (lit:lits) =
if haveSeen
then mkGr seen ne lits
else newNodes `seq` newEdges `seq`
mkGr seen' (newNodes, newEdges) (lits ++ pred)
where
haveSeen = seen `contains` litNode lit
newNodes = var lit `Set.insert` nodes
newEdges = [ ( litNode (negate x)
, litNode lit, () )
| x <- pred ] ++ edges
pred = filterReason $
if lit == cLit then confl else
Map.findWithDefault [] (var lit) reasonMap `without` lit
filterReason = filter ( ((var lit /=) . var) .&&.
((<= litLevel lit) . litLevel) )
seen' = seen `with` litNode lit
litLevel l = if l == cLit then length _dlits else lev!(var l)
litNode l =
if var l == var cLit
then unLit l
else (abs . unLit) l
showAssignment a = intercalate " " ([show (a!i) | i <- range . bounds $ a,
(a!i) /= 0])
initialActivity :: Double
initialActivity = 1.0
instance Error (Lit, Clause, ClauseId) where
noMsg = (L 0, [], 0)
instance Error () where
noMsg = ()
data VerifyError = SatError [(Clause, Either () Bool)]
| UnsatError ResolutionError
deriving (Show)
verify :: Solution -> Maybe ResolutionTrace -> CNF -> Maybe VerifyError
verify sol maybeRT cnf =
case sol of
Sat m ->
let unsatClauses = toList $
Set.filter (not . isTrue . snd) $
Set.map (\c -> (c, c `statusUnder` m)) (clauses cnf)
in if null unsatClauses
then Nothing
else Just . SatError $ unsatClauses
Unsat m ->
case Resolution.checkDepthFirst (fromJust maybeRT) of
Left er -> Just . UnsatError $ er
Right _ -> Nothing
where isTrue (Right True) = True
isTrue _ = False
data Stats = Stats
{ statsNumConfl :: Int64
, statsNumConflTotal :: Int64
, statsNumLearnt :: Int64
, statsAvgLearntLen :: Double
, statsNumDecisions :: Int64
, statsNumImpl :: Int64
}
newtype ShowWrapped = WrapString { unwrapString :: String }
instance Show ShowWrapped where
show = unwrapString
instance Show Stats where
show = show . statTable
statTable :: Stats -> Tabular.Table ShowWrapped
statTable s =
Tabular.mkTable
[ [WrapString "Num. Conflicts"
,WrapString $ show (statsNumConflTotal s)]
, [WrapString "Num. Learned Clauses"
,WrapString $ show (statsNumLearnt s)]
, [WrapString " --> Avg. Lits/Clause"
,WrapString $ show (statsAvgLearntLen s)]
, [WrapString "Num. Decisions"
,WrapString $ show (statsNumDecisions s)]
, [WrapString "Num. Propagations"
,WrapString $ show (statsNumImpl s)] ]
statSummary :: Stats -> String
statSummary s =
show (Tabular.mkTable
[[WrapString $ show (statsNumConflTotal s) ++ " Conflicts"
,WrapString $ "| " ++ show (statsNumLearnt s) ++ " Learned Clauses"
++ " (avg " ++ printf "%.2f" (statsAvgLearntLen s)
++ " lits/clause)"]])
extractStats :: DPLLMonad s Stats
extractStats = do
s <- get
learntArr <- liftST $ unsafeFreezeWatchArray (learnt s)
let learnts = (nub . Fl.concat)
[ map (sort . (\(_,c,_) -> c)) (learntArr!i)
| i <- (range . bounds) learntArr ] :: [Clause]
stats =
Stats { statsNumConfl = numConfl s
, statsNumConflTotal = numConflTotal s
, statsNumLearnt = fromIntegral $ length learnts
, statsAvgLearntLen =
fromIntegral (foldl' (+) 0 (map length learnts))
/ fromIntegral (statsNumLearnt stats)
, statsNumDecisions = numDecisions s
, statsNumImpl = numImpl s }
return stats
unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s])
unsafeFreezeWatchArray = freeze
constructResTrace :: Solution -> DPLLMonad s ResolutionTrace
constructResTrace sol = do
s <- get
watchesIndices <- range `liftM` liftST (getBounds (watches s))
origClauseMap <-
foldM (\origMap i -> do
clauses <- liftST $ readArray (watches s) i
return $
foldr (\(_, clause, clauseId) origMap ->
Map.insert clauseId clause origMap)
origMap
clauses)
Map.empty
watchesIndices
let singleClauseMap =
foldr (\(clause, clauseId) m -> Map.insert clauseId clause m)
Map.empty
(resTraceOriginalSingles . resolutionTrace $ s)
anteMap =
foldr (\l anteMap -> Map.insert (var l) (getAnteId s (var l)) anteMap)
Map.empty
(litAssignment . finalAssignment $ sol)
return
(initResolutionTrace
(head (resTrace . resolutionTrace $ s))
(finalAssignment sol))
{ traceSources = resSourceMap . resolutionTrace $ s
, traceOriginalClauses = origClauseMap `Map.union` singleClauseMap
, traceAntecedents = anteMap }
where
getAnteId s v = snd $
Map.findWithDefault (error $ "no reason for assigned var " ++ show v)
v (reason s)