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.Int( Int64 )
import Data.List( intercalate, nub, tails, sortBy, sort )
import Data.Maybe
import Data.Ord( comparing )
import Data.STRef
import Data.Sequence( Seq )
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.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 initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0
(a, isUnsat) <- initialState initialAssignment
if isUnsat then reportSolution (Unsat a)
else stepToSolution initialAssignment >>= reportSolution)
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
stepToSolution :: MAssignment s -> DPLLMonad s Solution
stepToSolution assignment = do
step <- solveStep assignment
useRestarts <- gets (configUseRestarts . dpllConfig)
isTimeToRestart <- uncurry ((>=)) `liftM`
gets (numConfl &&& (configRestart . dpllConfig))
case step of
Left m -> do when (useRestarts && isTimeToRestart)
(do _stats <- extractStats
resetState m)
stepToSolution 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
reportSolution :: Solution -> DPLLMonad s (Solution, Stats, Maybe ResolutionTrace)
reportSolution s = do
stats <- extractStats
case s of
Sat _ -> return (s, stats, Nothing)
Unsat _ -> do
resTrace <- constructResTrace s
return (s, stats, Just resTrace)
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 (Either (MAssignment s) Solution)
solveStep m = do
unsafeFreezeAss m >>= solveStepInvariants
conf <- gets dpllConfig
let selector = if configUseVSIDS conf then select else selectStatic
maybeConfl <- bcp m
mFr <- unsafeFreezeAss m
voArr <- gets (varOrderArr . varOrder)
voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze voArr)
s <- get
stepForward $
unsat maybeConfl s ==> postProcessUnsat maybeConfl
>< maybeConfl >=> backJump m
>< selector mFr voFr >=> decide m
where
stepForward Nothing = (Right . Sat) `liftM` unsafeFreezeAss m
stepForward (Just step) = do
r <- step
case r of
Nothing -> (Right . Unsat) `liftM` liftST (unsafeFreezeAss m)
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 ()
data Solution = Sat IAssignment | Unsat IAssignment deriving (Eq)
instance Show Solution where
show (Sat a) = "satisfiable: " ++ showAssignment a
show (Unsat _) = "unsatisfiable"
finalAssignment :: Solution -> IAssignment
finalAssignment (Sat a) = a
finalAssignment (Unsat a) = a
noLevel :: Level
noLevel = 1
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
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 ><
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 _ ->
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)