module Funsat.Solver
#ifndef TESTING
( solve
, solve1
, DPLLConfig(..)
, Solution(..)
, IAssignment
, litAssignment
, litSign
, Stats(..)
, CNF
, GenCNF(..)
, Clause
, Lit(..)
, Var(..)
, var
, NonStupidString(..)
, statTable
, verify
)
#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.BitSet (BitSet)
import Data.Foldable hiding (sequence_)
import Data.Graph.Inductive.Graph( DynGraph, Graph )
import Data.Graph.Inductive.Graphviz
import Data.Graph.Inductive.Tree( Gr )
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 Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum)
import Text.Printf( printf )
import Funsat.Utils
import DPLL.Monad
import qualified Data.BitSet as BitSet
import qualified Data.Graph.Inductive.Graph as Graph
import qualified Data.Graph.Inductive.Query.BFS as BFS
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.FastDom as Dom
import qualified Text.Tabular as Tabular
solve :: DPLLConfig -> CNF -> (Solution, Stats)
solve cfg fIn =
either (error "no solution") id $
runST $
evalSSTErrMonad
(do sol <- stepToSolution $ do
initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0
isUnsat <- initialState initialAssignment
if isUnsat then return (Right Unsat)
else solveStep initialAssignment
stats <- extractStats
return (sol, stats))
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
, dpllConfig=cfg }
where
f = preprocessCNF fIn
initialState :: MAssignment s -> DPLLMonad s 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 $ return True)) $ do
forM_ (clauses f)
(\c -> do isConsistent <- watchClause m c False
when (not isConsistent)
(throwError (L 0, [])))
return False
solve1 :: CNF -> (Solution, Stats)
solve1 f = solve (defaultConfig f) f
data DPLLConfig = Cfg
{ configRestart :: !Int64
, configRestartBump :: !Double
, configUseVSIDS :: !Bool
, configUseWatchedLiterals :: !Bool
, configUseRestarts :: !Bool
, configUseLearning :: !Bool }
deriving Show
defaultConfig :: CNF -> DPLLConfig
defaultConfig f = Cfg { configRestart = 100
, configRestartBump = 1.5
, configUseVSIDS = True
, configUseWatchedLiterals = True
, configUseRestarts = True
, configUseLearning = 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) -> (p, filter (/= negate l) c))
modifyArray (watches s) l filterL
modifyArray (learnt s) l filterL
writeArray (watches s) (negate l) []
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
let bcper = if configUseWatchedLiterals conf then bcp else bcpDumb
maybeConfl <- bcper m
mFr <- unsafeFreezeAss m
s <- get
voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze . varOrderArr . varOrder $ s)
newState $
unsat maybeConfl s ==> return Nothing
>< maybeConfl >=> backJump m
>< selector mFr voFr >=> decide m
where
newState stepMaybe =
case stepMaybe of
Nothing -> unsafeFreezeAss m >>= return . Right . Sat
Just step -> step >>= return . maybe (Right Unsat) Left
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 deriving (Eq)
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"
newtype Var = V {unVar :: Int} deriving (Eq, Ord, Enum, Ix)
instance Show Var where
show (V i) = show i ++ "v"
instance Num Var where
_ + _ = error "+ doesn't make sense for variables"
_ _ = error "- doesn't make sense for variables"
_ * _ = error "* doesn't make sense for variables"
signum _ = error "signum doesn't make sense for variables"
negate = error "negate doesn't make sense for variables"
abs = id
fromInteger l | l <= 0 = error $ show l ++ " is not a variable"
| otherwise = V $ fromInteger l
newtype Lit = L {unLit :: Int} deriving (Eq, Ord, Enum, Ix)
inLit f = L . f . unLit
litSign :: Lit -> Bool
litSign (L x) | x < 0 = False
| x > 0 = True
instance Show Lit where
show l = show ul
where ul = unLit l
instance Read Lit where
readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s :: [(Int, String)])
var :: Lit -> Var
var = V . abs . unLit
instance Num Lit where
_ + _ = error "+ doesn't make sense for literals"
_ _ = error "- doesn't make sense for literals"
_ * _ = error "* doesn't make sense for literals"
signum _ = error "signum doesn't make sense for literals"
negate = inLit negate
abs = inLit abs
fromInteger l | l == 0 = error "0 is not a literal"
| otherwise = L $ fromInteger l
type Clause = [Lit]
data GenCNF a = CNF {
numVars :: Int,
numClauses :: Int,
clauses :: Set a
}
deriving (Show, Read, Eq)
type CNF = GenCNF Clause
instance Foldable GenCNF where
foldMap toM cnf = foldMap toM (clauses cnf)
class Ord a => Setlike t a where
without :: t -> a -> t
with :: t -> a -> t
contains :: t -> a -> Bool
instance Ord a => Setlike (Set a) a where
without = flip Set.delete
with = flip Set.insert
contains = flip Set.member
instance Ord a => Setlike [a] a where
without = flip List.delete
with = flip (:)
contains = flip List.elem
instance Setlike IAssignment Lit where
without a l = a // [(var l, 0)]
with a l = a // [(var l, unLit l)]
contains a l = unLit l == a ! (var l)
instance (Ord k, Ord a) => Setlike (Map k a) (k, a) where
with m (k,v) = Map.insert k v m
without m (k,_) = Map.delete k m
contains = error "no contains for Setlike (Map k a) (k, a)"
instance (Ord a, BitSet.Hash a) => Setlike (BitSet a) a where
with = flip BitSet.insert
without = flip BitSet.delete
contains = flip BitSet.member
instance (BitSet.Hash Lit) where
hash l = if li > 0 then 2 * vi else (2 * vi) + 1
where li = unLit l
vi = abs li
instance (BitSet.Hash Var) where
hash = unVar
type IAssignment = UArray Var Int
type MAssignment s = STUArray s Var Int
freezeAss :: MAssignment s -> ST s IAssignment
freezeAss = freeze
unsafeFreezeAss :: MAssignment s -> DPLLMonad s IAssignment
unsafeFreezeAss = liftST . unsafeFreeze
thawAss :: IAssignment -> ST s (MAssignment s)
thawAss = thaw
unsafeThawAss :: IAssignment -> ST s (MAssignment s)
unsafeThawAss = unsafeThaw
assign :: MAssignment s -> Lit -> ST s (MAssignment s)
assign a l = writeArray a (var l) (unLit l) >> return a
unassign :: MAssignment s -> Lit -> ST s (MAssignment s)
unassign a l = writeArray a (var l) 0 >> return a
class Model a m where
statusUnder :: a -> m -> Either () Bool
instance Model Lit IAssignment where
statusUnder l a | a `contains` l = Right True
| a `contains` negate l = Right False
| otherwise = Left ()
instance Model Var IAssignment where
statusUnder v a | a `contains` pos = Right True
| a `contains` neg = Right False
| otherwise = Left ()
where pos = L (unVar v)
neg = negate pos
instance Model Clause IAssignment where
statusUnder c m
| Fl.any (\e -> m `contains` e) c = Right True
| Fl.all (`isFalseUnder` m) c = Right False
| otherwise = Left ()
isUndefUnder :: Model a m => a -> m -> Bool
isUndefUnder x m = isUndef $ x `statusUnder` m
where isUndef (Left ()) = True
isUndef _ = False
isTrueUnder :: Model a m => a -> m -> Bool
isTrueUnder x m = isTrue $ x `statusUnder` m
where isTrue (Right True) = True
isTrue _ = False
isFalseUnder :: Model a m => a -> m -> Bool
isFalseUnder x m = isFalse $ x `statusUnder` m
where isFalse (Right False) = True
isFalse _ = False
isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c)
&& not (Fl.any (`isTrueUnder` m) c)
getUnit c m = case filter (not . (`isFalseUnder` m)) c of
[u] -> u
xs -> error $ "getUnit: not unit: " ++ show xs
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)
type WatchArray s = STArray s Lit [WatchedPair s]
data DPLLStateContents s = SC
{ cnf :: CNF
, dl :: [Lit]
, watches :: WatchArray s
, learnt :: WatchArray s
, propQ :: Seq Lit
, level :: LevelArray s
, trail :: [Lit]
, reason :: Map Var Clause
, numConfl :: !Int64
, numConflTotal :: !Int64
, numDecisions :: !Int64
, numImpl :: !Int64
, varOrder :: VarOrder s
, 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 = StateT (DPLLStateContents s) (ST s)
instance Control.Monad.MonadST.MonadST s (DPLLMonad' s) where
liftST = lift
type DPLLMonad s = SSTErrMonad (Lit, Clause) (DPLLStateContents s) s
bcpLit :: MAssignment s
-> Lit
-> DPLLMonad s (Maybe (Lit, Clause))
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) : 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)
when (not isConsistent) $ do
alter (restClauses ++) l
clearQueue
throwError (negate q, c)
bcp :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause))
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)
bcpDumb :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause))
bcpDumb m = do
mFr <- liftST $ freezeAss m
s <- get
let candidates = Set.filter (not . (`isTrueUnder` mFr)) (clauses . cnf $ s)
case find (`isFalseUnder` mFr) candidates of
Just fClause -> return $ Just (head fClause, fClause)
Nothing ->
case find (`isUnitUnder` mFr) candidates of
Nothing -> return Nothing
Just clause -> do
let unitLit = getUnit clause mFr
modify $ \s -> s{ numImpl = numImpl s + 1 }
isConsistent <- assert (unitLit `isUndefUnder` mFr) $
enqueue m unitLit (Just clause)
clearQueue
if not isConsistent
then return $ Just (unitLit, clause)
else bcpDumb m
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)
-> 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, newLevel) <-
do mFr <- unsafeFreezeAss m
useLearning <- configUseLearning `liftM` gets dpllConfig
if useLearning then analyse mFr levelArr dl c
else analyseDecision 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
enqueue m (getUnit learntCl mFr) (Just learntCl)
watchClause m learntCl True
return $ Just m
analyseDecision :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause)
-> DPLLMonad s (Clause, Int)
analyseDecision mFr levelArr dlits c@(cLit, _cClause) = do
st <- get
let decisionCut = uipCut dlits levelArr conflGraph (unLit cLit)
(decisionUIP conflGraph)
conflGraph = mkConflGraph mFr levelArr (reason st) dlits c
:: Gr CGNodeAnnot ()
return $ cutLearn mFr levelArr decisionCut
where
decisionUIP :: (Graph gr) => gr CGNodeAnnot () -> Graph.Node
decisionUIP _ = abs . unLit $ head dlits
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)
-> DPLLMonad s (Clause, Int)
analyse mFr levelArr dlits (cLit, cClause) = do
st <- get
m <- liftST $ unsafeThawAss mFr
a <- firstUIPBFS m (numVars . cnf $ st) (reason st)
return a
where
firstUIPBFS :: MAssignment s -> Int -> Map Var Clause -> DPLLMonad s (Clause, Int)
firstUIPBFS m nVars reasonMap = do
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
else Map.findWithDefault [] (var l) reasonMap
`without` l)
(`doWhile` (liftST (readSTRef counterR) >>= return . (> 0))) $
do p <- liftST $ readSTRef pR
forM_ (reasonL p) (bump . var)
liftST . forM_ (reasonL p) $ \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
return (out_learned, out_btlevel)
firstUIP conflGraph =
argminimum distanceFromConfl uips :: Graph.Node
where
uips = domConfl `intersect` domAssigned :: [Graph.Node]
domConfl = filter (\i -> levelN i == currentLevel && i /= conflNode) $
fromJust $ lookup conflNode domFromLastd
domAssigned =
if negate conflNode `elem` DFS.reachable (abs $ unLit lastd) conflGraph
then
filter (\i -> levelN i == currentLevel && i /= conflNode) $
fromJust $ lookup (negate conflNode) domFromLastd
else [(abs $ unLit lastd)]
domFromLastd = Dom.dom conflGraph (abs $ unLit lastd)
distanceFromConfl x = length $ BFS.esp x conflNode conflGraph
lastd = head dlits
conflNode = unLit cLit
currentLevel = length dlits
levelL l = levelArr!(var l)
levelN i = if i == unLit cLit then currentLevel else ((levelArr!) . V . abs) i
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
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 -> DPLLStateContents 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 . snd)) 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
-> Bool
-> DPLLMonad s Bool
watchClause m c isLearnt = do
conf <- gets dpllConfig
case c of
[] -> return True
[l] -> do result <- enqueue m l (Just c)
levelArr <- gets level
liftST $ writeArray levelArr (var l) 0
return result
_ -> if configUseWatchedLiterals conf then
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)
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
else do modify $ \s ->
let cs = c `Set.insert` (clauses . cnf) s
in s{ cnf = (cnf s){ clauses = cs
, numClauses = Set.size cs } }
return True
enqueue :: MAssignment s
-> Lit
-> Maybe Clause
-> 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)
(==>) :: (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 ><
showAssignment a = intercalate " " ([show (a!i) | i <- range . bounds $ a,
(a!i) /= 0])
initialActivity :: Double
initialActivity = 1.0
instance Error (Lit, Clause) where
noMsg = (L 0, [])
instance Error () where
noMsg = ()
data Stats = Stats
{ statsNumConfl :: Int64
, statsNumConflTotal :: Int64
, statsNumLearnt :: Int64
, statsAvgLearntLen :: Double
, statsNumDecisions :: Int64
, statsNumImpl :: Int64 }
newtype NonStupidString = Stupid { stupefy :: String }
instance Show NonStupidString where
show = stupefy
instance Show Stats where
show = show . statTable
statTable :: Stats -> Tabular.T NonStupidString
statTable s =
Tabular.mkTable
[ [Stupid "Num. Conflicts"
,Stupid $ show (statsNumConflTotal s)]
, [Stupid "Num. Learned Clauses"
,Stupid $ show (statsNumLearnt s)]
, [Stupid " --> Avg. Lits/Clause"
,Stupid $ show (statsAvgLearntLen s)]
, [Stupid "Num. Decisions"
,Stupid $ show (statsNumDecisions s)]
, [Stupid "Num. Propagations"
,Stupid $ show (statsNumImpl s)] ]
statSummary :: Stats -> String
statSummary s =
show (Tabular.mkTable
[[Stupid $ show (statsNumConflTotal s) ++ " Conflicts"
,Stupid $ "| " ++ 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 . snd) (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
litAssignment :: IAssignment -> [Lit]
litAssignment mFr = map (L . (mFr!)) (range . bounds $ mFr)
verify :: IAssignment -> CNF -> Maybe [(Clause, Either () Bool)]
verify m cnf =
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 unsatClauses
where isTrue (Right True) = True
isTrue _ = False