diff --git a/CHANGES b/CHANGES new file mode 100644 --- /dev/null +++ b/CHANGES @@ -0,0 +1,7 @@ +-*- mode: outline -*- + +* 0.5.1 +** Update for compatibility with parse-dimacs 1.2, +which should mean faster parsing. +** Code cleanup + diff --git a/Funsat/Monad.hs b/Funsat/Monad.hs --- a/Funsat/Monad.hs +++ b/Funsat/Monad.hs @@ -68,20 +68,21 @@ -- . newtype SSTErrMonad e st s a = SSTErrMonad { unSSTErrMonad :: forall r. (a -> (st -> ST s (Either e r, st))) - -> (st -> ST s (Either e r, st)) } + -> (st -> ST s (Either e r, st)) } instance Monad (SSTErrMonad e st s) where return x = SSTErrMonad ($ x) (>>=) = bindSSTErrMonad -bindSSTErrMonad :: SSTErrMonad e st s a -> (a -> SSTErrMonad e st s b) -> SSTErrMonad e st s b +bindSSTErrMonad :: SSTErrMonad e st s a -> (a -> SSTErrMonad e st s b) + -> SSTErrMonad e st s b {-# INLINE bindSSTErrMonad #-} bindSSTErrMonad m f = {-# SCC "bindSSTErrMonad" #-} SSTErrMonad (\k -> unSSTErrMonad m (\a -> unSSTErrMonad (f a) k)) instance MonadState st (SSTErrMonad e st s) where - get = SSTErrMonad (\k s -> k s s) + get = SSTErrMonad (\k s -> k s s) put s' = SSTErrMonad (\k _ -> k () s') instance (Error e) => MonadError e (SSTErrMonad e st s) where @@ -94,7 +95,7 @@ Right result -> k result s') instance (Error e) => MonadPlus (SSTErrMonad e st s) where - mzero = SSTErrMonad (\_ s -> return (Left noMsg, s)) + mzero = SSTErrMonad (\_ s -> return (Left noMsg, s)) mplus m n = SSTErrMonad (\k s -> do (r, s') <- runSSTErrMonad m s case r of diff --git a/Funsat/Resolution.hs b/Funsat/Resolution.hs --- a/Funsat/Resolution.hs +++ b/Funsat/Resolution.hs @@ -35,8 +35,7 @@ , ResolutionTrace(..) , initResolutionTrace , ResolutionError(..) - , UnsatisfiableCore - , ClauseId ) + , UnsatisfiableCore ) where import Control.Monad.Error @@ -48,7 +47,7 @@ import qualified Data.IntSet as IntSet import qualified Data.Map as Map import Funsat.Types -import Funsat.Utils( isSingle ) +import Funsat.Utils( isSingle, getUnit, isFalseUnder ) -- IDs = Ints @@ -84,19 +83,17 @@ , traceOriginalClauses = Map.empty , traceAntecedents = Map.empty } -type ClauseId = Int - -- | A type indicating an error in the checking process. Assuming this -- checker's code is correct, such an error indicates a bug in the SAT solver. data ResolutionError = ResolveError Var Clause Clause - -- ^ Indicates that the clauses do not properly resolve on the - -- variable. + -- ^ Indicates that the clauses do not properly resolve on the + -- variable. | CannotResolve [Var] Clause Clause - -- ^ Indicates that the clauses do not have complementary variables - -- or have too many. The complementary variables (if any) are in - -- the list. + -- ^ Indicates that the clauses do not have complementary variables or + -- have too many. The complementary variables (if any) are in the + -- list. | AntecedentNotUnit Clause -- ^ Indicates that the constructed antecedent clause not unit under @@ -163,8 +160,7 @@ data ResState = ResState { clauseIdMap :: Map ClauseId Clause - , unsatCore :: UnsatCoreIntSet - } + , unsatCore :: UnsatCoreIntSet } type UnsatCoreIntSet = IntSet -- set of ClauseIds @@ -185,7 +181,7 @@ checkDFClause resClause recursiveBuild :: ClauseId -> ResM Clause -recursiveBuild clauseId {-id-} = do +recursiveBuild clauseId = do maybeClause <- getClause case maybeClause of Just clause -> return clause @@ -264,7 +260,7 @@ chooseLiteral :: Clause -> ResM Lit chooseLiteral (l:_) = return l -chooseLiteral _ = error "chooseLiteral: empty clause" +chooseLiteral _ = error "chooseLiteral: empty clause" checkAnteClause :: Var -> Clause -> ResM () checkAnteClause v anteClause = do diff --git a/Funsat/Solver.hs b/Funsat/Solver.hs --- a/Funsat/Solver.hs +++ b/Funsat/Solver.hs @@ -91,35 +91,29 @@ -} -import Control.Arrow ((&&&)) -import Control.Exception (assert) -import Control.Monad.Error hiding ((>=>), forM_, runErrorT) +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 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.Graph.Inductive.Graphviz -import Data.Int (Int64) -import Data.List (intercalate, nub, tails, sortBy, intersect, sort) -import Data.Map (Map) +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.Ord( comparing ) import Data.STRef -import Data.Sequence (Seq) -import Data.Set (Set) -import Debug.Trace (trace) +import Data.Sequence( Seq ) +-- 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 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 @@ -133,7 +127,7 @@ -- | Run the DPLL-based SAT solver on the given CNF instance. Returns a -- solution, along with internal solver statistics and possibly a resolution -- trace. The trace is for checking a proof of `Unsat', and thus is only --- present then. +-- present when the result is `Unsat'. solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace) solve cfg fIn = -- To solve, we simply take baby steps toward the solution using solveStep, @@ -142,30 +136,24 @@ 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 } + (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 -- If returns True, then problem is unsat. initialState :: MAssignment s -> DPLLMonad s (IAssignment, Bool) initialState m = do initialLevel <- liftST $ newSTUArray (V 1, V (numVars f)) noLevel - modify $ \s -> s{level = initialLevel} + 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)) [] @@ -173,22 +161,65 @@ 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) - -- conflict data is ignored here, so safe to fake - (do traceClauseId cid - throwError (L 0, [], 0))) - a <- liftST (unsafeFreezeAss m) - return (a, False) + -- Watch each clause, making sure to bork if we find a contradiction. + (`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) + -- conflict data is ignored here, so safe to fake + (do traceClauseId cid ; throwError (L 0, [], 0))) + a <- liftST (unsafeFreezeAss m) + return (a, False) -- | Solve with the default configuration `defaultConfig'. solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace) solve1 f = solve (defaultConfig f) f +-- | This function applies `solveStep' recursively until SAT instance is +-- solved, starting with the given initial assignment. It also implements the +-- conflict-based restarting (see `DPLLConfig'). +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 +-- trace ("Restarting...") $ +-- trace (statSummary stats) $ + resetState m) + stepToSolution m + Right s -> return s + where + resetState m = do + modify $ \s -> s{ numConfl = 0 } + -- Require more conflicts before next restart. + 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) + + -- | Configuration parameters for the solver. data DPLLConfig = Cfg { configRestart :: !Int64 -- ^ Number of conflicts before a restart. @@ -248,16 +279,17 @@ -- function takes one step in that transition system. Given an unsatisfactory -- assignment, perform one state transition, producing a new assignment and a -- new state. -solveStep :: MAssignment s -> DPLLMonad s (Step s) +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 - s <- get - voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze . varOrderArr . varOrder $ s) - newState $ + mFr <- unsafeFreezeAss m + voArr <- gets (varOrderArr . varOrder) + voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze voArr) + s <- get + stepForward $ -- Check if unsat. unsat maybeConfl s ==> postProcessUnsat maybeConfl -- Unit propagation may reveal conflicts; check. @@ -266,22 +298,17 @@ >< selector mFr voFr >=> decide m where -- Take the step chosen by the transition guards above. - newState stepMaybe = - case stepMaybe of - -- No step to do => satisfying assignment. (p. 6) - Nothing -> unsafeFreezeAss m >>= return . Right . Sat - -- A step to do => do it, then see what it says. - Just step -> do - r <- step - case r of - Nothing -> do a <- liftST (unsafeFreezeAss m) - return . Right . Unsat $ a - Just m -> return . Left $ m --- liftM (maybe (Right Unsat) Left) + 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 -- | /Precondition:/ problem determined to be unsat. -- --- Records id of conflicting clause in trace. +-- Records id of conflicting clause in trace before failing. Always returns +-- `Nothing'. postProcessUnsat :: Maybe (Lit, Clause, ClauseId) -> DPLLMonad s (Maybe a) postProcessUnsat maybeConfl = do traceClauseId $ (thd . fromJust) maybeConfl @@ -294,103 +321,33 @@ solveStepInvariants :: IAssignment -> DPLLMonad s () {-# INLINE solveStepInvariants #-} solveStepInvariants _m = assert True $ do - s <- get - -- no dups in decision list or trail - assert ((length . dl) s == (length . nub . dl) s) $ - assert ((length . trail) s == (length . nub . trail) s) $ - return () - + s <- get + -- no dups in decision list or trail + assert ((length . dl) s == (length . nub . dl) s) $ + assert ((length . trail) s == (length . nub . trail) s) $ + return () --- | A state transition, or /step/, produces either an intermediate assignment --- (using `Left') or a solution to the instance. -type Step s = Either (MAssignment s) Solution --- | The solution to a SAT problem is either an assignment or unsatisfiable. +-- | The solution to a SAT problem. In each case we return an assignment, +-- which is obviously right in the `Sat' case; in the `Unsat' case, the reason +-- is to assist in the generation of an unsatisfiable core. data Solution = Sat IAssignment | Unsat IAssignment deriving (Eq) -finalAssignment :: Solution -> IAssignment -finalAssignment (Sat a) = a -finalAssignment (Unsat a) = a - --- | This function applies `solveStep' recursively until SAT instance is --- solved. It also implements the conflict-based restarting (see --- `DPLLConfig'). -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 --- trace ("Restarting...") $ --- trace (statSummary stats) $ - resetState m) - stepToSolution (solveStep m) - Right s -> return s - where - resetState m = do - modify $ \s -> s{ numConfl = 0 } - -- Require more conflicts before next restart. - 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" - --- ** Internal data types - -type Level = Int +finalAssignment :: Solution -> IAssignment +finalAssignment (Sat a) = a +finalAssignment (Unsat a) = a --- | A /level array/ maintains a record of the decision level of each variable --- in the solver. If @level@ is such an array, then @level[i] == j@ means the --- decision level for var number @i@ is @j@. @j@ must be non-negative when --- the level is defined, and `noLevel' otherwise. --- --- Whenever an assignment of variable @v@ is made at decision level @i@, --- @level[unVar v]@ is set to @i@. -type LevelArray s = STUArray s Var Level --- | Immutable version. -type FrozenLevelArray = UArray Var Level +-- ** Internals -- | Value of the `level' array if corresponding variable unassigned. Had -- better be less that 0. noLevel :: Level noLevel = -1 --- | The VSIDS-like dynamic variable ordering. -newtype VarOrder s = VarOrder { varOrderArr :: STUArray s Var Double } - deriving Show -newtype FrozenVarOrder = FrozenVarOrder (UArray Var Double) - deriving Show - --- | Each pair of watched literals is paired with its clause and id. -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)] - -- Singleton clauses are not stored in the database, they are assigned. - -- But we need to record their ids, so we put them here. - , resSourceMap :: Map ClauseId [ClauseId] } - deriving (Show) - -type ReasonMap = Map Var (Clause, ClauseId) -type ClauseId = Int - -- ** State and Phases data FunsatState s = SC @@ -433,18 +390,7 @@ , resolutionTrace :: PartialResolutionTrace - , dpllConfig :: DPLLConfig - } - deriving Show - -instance Show (STRef s a) where - show = const "" -instance Show (STUArray s Var Int) where - show = const "" -instance Show (STUArray s Var Double) where - show = const "" -instance Show (STArray s a b) where - show = const "" + , dpllConfig :: DPLLConfig } deriving Show -- | Our star monad, the DPLL State monad. We use @ST@ for mutable arrays and -- references, when necessary. Most of the state, however, is kept in @@ -712,16 +658,16 @@ undoOne :: MAssignment s -> DPLLMonad s () {-# INLINE undoOne #-} 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) } + 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) } -- | Increase the recorded activity of given variable. bump :: Var -> DPLLMonad s () @@ -757,19 +703,19 @@ -- | Keep the smaller half of the learned clauses. 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:)) + 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:)) -- *** Unit propagation @@ -788,26 +734,26 @@ -> DPLLMonad s Bool {-# INLINE watchClause #-} 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 -- avoid watching dup clauses - | 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 + 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 -- avoid watching dup clauses + | 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 literal in the `propQ' and place it in the current assignment. -- If this conflicts with an existing assignment, returns @False@; otherwise @@ -826,30 +772,30 @@ {-# INLINE enqueue #-} -- enqueue _m l _r | trace ("enqueue " ++ show l) $ False = undefined enqueue m l r = do - mFr <- unsafeFreezeAss m - case l `statusUnder` mFr of - Right b -> return b -- conflict/already assigned - Left () -> do - liftST $ m `assign` l - -- assign decision level for literal - 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 + mFr <- unsafeFreezeAss m + case l `statusUnder` mFr of + Right b -> return b -- conflict/already assigned + Left () -> do + liftST $ m `assign` l + -- assign decision level for literal + 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 -- | Pop the `propQ'. Error (crash) if it is empty. dequeue :: DPLLMonad s Lit {-# INLINE dequeue #-} 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 + 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 -- | Clear the `propQ'. clearQueue :: DPLLMonad s () @@ -913,6 +859,7 @@ -- | Guard a transition action. If the boolean is true, return the action -- given as an argument. Otherwise, return `Nothing'. (==>) :: (Monad m) => Bool -> m a -> Maybe (m a) +{-# INLINE (==>) #-} (==>) b amb = guard b >> return amb infixr 6 ==> @@ -937,166 +884,24 @@ infixl 5 >< -- *** Misc - - - --- | The union of the reason side and the conflict side are all the nodes in --- the `cutGraph' (excepting, perhaps, the nodes on the reason side at --- decision level 0, which should never be present in a learned clause). -data Cut f gr a b = - Cut { reasonSide :: f Graph.Node - -- ^ The reason side contains at least the decision variables. - , conflictSide :: f Graph.Node - -- ^ The conflict side contains the conflicting literal. - , 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 ++ ")" - --- | Generate a cut using the given UIP node. The cut generated contains --- exactly the (transitively) implied nodes starting with (but not including) --- the UIP on the conflict side, with the rest of the nodes on the reason --- side. -uipCut :: (Graph gr) => - [Lit] -- ^ decision literals - -> FrozenLevelArray - -> gr a b -- ^ conflict graph - -> Graph.Node -- ^ unassigned, implied conflicting node - -> Graph.Node -- ^ a UIP in the conflict graph - -> 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 - -- Transitively implied, and not including the UIP. - impliedByUIP = Set.insert extraNode $ - Set.fromList $ tail $ DFS.reachable uip conflGraph - -- The UIP may not imply the assigned conflict variable which needs to - -- be on the conflict side, unless it's a decision variable or the UIP - -- itself. - extraNode = if L (negate conflNode) `elem` dlits || negate conflNode == uip - then conflNode -- idempotent addition - else negate conflNode - allNodes = Set.fromList $ Graph.nodes conflGraph - - --- | Generate a learned clause from a cut of the graph. Returns a pair of the --- learned clause and the decision level to which to backtrack. -cutLearn :: (Graph gr, Foldable f) => IAssignment -> FrozenLevelArray - -> Cut f gr a b -> (Clause, Int) -cutLearn a levelArr cut = - ( clause - -- The new decision level is the max level of all variables in the - -- clause, excluding the uip (which is always at the current decision - -- level). - , maximum0 (map (levelArr!) . (`without` V (abs $ cutUIP cut)) . map var $ clause) ) - where - -- The clause is composed of the variables on the reason side which have - -- at least one successor on the conflict side. The value of the variable - -- is the negation of its value under the current assignment. - 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 has 0 as its max for the empty list - maximum0 xs = maximum xs - - --- | Annotate each variable in the conflict graph with literal (indicating its --- assignment) and decision level. The only reason we make a new datatype for --- this is for its `Show' instance. -data CGNodeAnnot = CGNA Lit Level -instance Show CGNodeAnnot where - show (CGNA (L 0) _) = "lambda" - show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")" - --- | Creates the conflict graph, where each node is labeled by its literal and --- level. --- --- Useful for getting pretty graphviz output of a conflict. -mkConflGraph :: DynGraph gr => - IAssignment - -> FrozenLevelArray - -> Map Var Clause - -> [Lit] -- ^ decision lits, in rev. chron. order - -> (Lit, Clause) -- ^ conflict info - -> gr CGNodeAnnot () -mkConflGraph mFr lev reasonMap _dlits (cLit, confl) = - Graph.mkGraph nodes' edges' - where - -- we pick out all the variables from the conflict graph, specially adding - -- both literals of the conflict variable, so that that variable has two - -- nodes in the graph. - nodes' = - ((0, CGNA (L 0) (-1)) :) $ -- lambda node - ((unLit cLit, CGNA cLit (-1)) :) $ - ((negate (unLit cLit), CGNA (negate cLit) (lev!(var cLit))) :) $ - -- annotate each node with its literal and level - map (\v -> (unVar v, CGNA (varToLit v) (lev!v))) $ - filter (\v -> v /= var cLit) $ - toList nodeSet' - - -- node set includes all variables reachable from conflict. This node set - -- construction needs a `seen' set because it might infinite loop - -- otherwise. - (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) - - -- seed with both conflicting literals - 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) -- unimplied lits from reasons are - -- complemented - , 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 = -- lit to node - if var l == var cLit -- preserve sign of conflicting lit - 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 = () +instance Error (Lit, Clause, ClauseId) where noMsg = (L 0, [], 0) +instance Error () where noMsg = () -data VerifyError = SatError [(Clause, Either () Bool)] - -- ^ Indicates a unsatisfactory assignment that was claimed - -- satisfactory. Each clause is tagged with its status - -- using 'Funsat.Types.Model'@.statusUnder@. +data VerifyError = + SatError [(Clause, Either () Bool)] + -- ^ Indicates a unsatisfactory assignment that was claimed + -- satisfactory. Each clause is tagged with its status using + -- 'Funsat.Types.Model'@.statusUnder@. - | UnsatError ResolutionError - -- ^ Indicates an error in the resultion checking process. + | UnsatError ResolutionError + -- ^ Indicates an error in the resultion checking process. deriving (Show) @@ -1115,7 +920,7 @@ in if null unsatClauses then Nothing else Just . SatError $ unsatClauses - Unsat m -> + Unsat _ -> case Resolution.checkDepthFirst (fromJust maybeRT) of Left er -> Just . UnsatError $ er Right _ -> Nothing @@ -1149,11 +954,9 @@ -- | The show instance uses the wrapped string. newtype ShowWrapped = WrapString { unwrapString :: String } -instance Show ShowWrapped where - show = unwrapString +instance Show ShowWrapped where show = unwrapString -instance Show Stats where - show = show . statTable +instance Show Stats where show = show . statTable -- | Convert statistics to a nice-to-display tabular form. statTable :: Stats -> Tabular.Table ShowWrapped diff --git a/Funsat/Types.hs b/Funsat/Types.hs --- a/Funsat/Types.hs +++ b/Funsat/Types.hs @@ -39,20 +39,22 @@ import Control.Monad.ST.Strict import Data.Array.ST import Data.Array.Unboxed -import Data.BitSet (BitSet) -import Data.Foldable hiding (sequence_) -import Data.Map (Map) -import Data.Set (Set) +import Data.BitSet ( BitSet ) +import Data.Foldable hiding ( sequence_ ) +import Data.Map ( Map ) +import Data.Set ( Set ) +import Data.STRef import Funsat.Monad -import Funsat.Utils -import Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum) +import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) import qualified Data.BitSet as BitSet import qualified Data.Foldable as Fl +import qualified Data.Graph.Inductive.Graph as Graph import qualified Data.List as List import qualified Data.Map as Map import qualified Data.Set as Set + -- * Basic Types newtype Var = V {unVar :: Int} deriving (Eq, Ord, Enum, Ix) @@ -71,24 +73,7 @@ | otherwise = V $ fromInteger l newtype Lit = L {unLit :: Int} deriving (Eq, Ord, Enum, Ix) -inLit f = L . f . unLit --- | The polarity of the literal. Negative literals are false; positive --- literals are true. The 0-literal is an error. -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)]) - --- | The variable for the given literal. -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" @@ -99,25 +84,32 @@ fromInteger l | l == 0 = error "0 is not a literal" | otherwise = L $ fromInteger l -type Clause = [Lit] +inLit :: (Int -> Int) -> Lit -> Lit +inLit f = L . f . unLit --- | ''Generic'' conjunctive normal form. It's ''generic'' because the --- elements of the clause set are polymorphic. And they are polymorphic so --- that I can easily get a `Foldable' instance. -data GenCNF a = CNF { - numVars :: Int, - numClauses :: Int, - clauses :: Set a - } - deriving (Show, Read, Eq) +-- | The polarity of the literal. Negative literals are false; positive +-- literals are true. The 0-literal is an error. +litSign :: Lit -> Bool +litSign (L x) | x < 0 = False + | x > 0 = True + | otherwise = error "litSign of 0" -type CNF = GenCNF Clause +instance Show Lit where show = show . unLit +instance Read Lit where + readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s) -instance Foldable GenCNF where - -- TODO it might be easy to make this instance more efficient. - foldMap toM cnf = foldMap toM (clauses cnf) +-- | The variable for the given literal. +var :: Lit -> Var +var = V . abs . unLit +type Clause = [Lit] +data CNF = CNF + { numVars :: Int + , numClauses :: Int + , clauses :: Set Clause } deriving (Show, Read, Eq) + + -- | Represents a container of type @t@ storing elements of type @a@ that -- support membership, insertion, and deletion. -- @@ -216,6 +208,30 @@ [] (range . bounds $ mFr) +-- | The union of the reason side and the conflict side are all the nodes in +-- the `cutGraph' (excepting, perhaps, the nodes on the reason side at +-- decision level 0, which should never be present in a learned clause). +data Cut f gr a b = + Cut { reasonSide :: f Graph.Node + -- ^ The reason side contains at least the decision variables. + , conflictSide :: f Graph.Node + -- ^ The conflict side contains the conflicting literal. + , 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 ++ ")" + +-- | Annotate each variable in the conflict graph with literal (indicating its +-- assignment) and decision level. The only reason we make a new datatype for +-- this is for its `Show' instance. +data CGNodeAnnot = CGNA Lit Int +instance Show CGNodeAnnot where + show (CGNA (L 0) _) = "lambda" + show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")" + + + -- * Model @@ -238,12 +254,14 @@ 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 -- true if c intersect m is not null == a member of c in m @@ -251,50 +269,49 @@ -- false if all its literals are false under m. | Fl.all (`isFalseUnder` m) c = Right False | otherwise = Left () - - - --- | `True' if and only if the object is undefined in the model. -isUndefUnder :: Model a m => a -> m -> Bool -isUndefUnder x m = isUndef $ x `statusUnder` m - where isUndef (Left ()) = True - isUndef _ = False + where + isFalseUnder x m = isFalse $ x `statusUnder` m + where isFalse (Right False) = True + isFalse _ = False --- | `True' if and only if the object is true in the model. -isTrueUnder :: Model a m => a -> m -> Bool -isTrueUnder x m = isTrue $ x `statusUnder` m - where isTrue (Right True) = True - isTrue _ = False +-- * Internal data types --- | `True' if and only if the object is false in the model. -isFalseUnder :: Model a m => a -> m -> Bool -isFalseUnder x m = isFalse $ x `statusUnder` m - where isFalse (Right False) = True - isFalse _ = False +type Level = Int --- * Helpers +-- | A /level array/ maintains a record of the decision level of each variable +-- in the solver. If @level@ is such an array, then @level[i] == j@ means the +-- decision level for var number @i@ is @j@. @j@ must be non-negative when +-- the level is defined, and `noLevel' otherwise. +-- +-- Whenever an assignment of variable @v@ is made at decision level @i@, +-- @level[unVar v]@ is set to @i@. +type LevelArray s = STUArray s Var Level +-- | Immutable version. +type FrozenLevelArray = UArray Var Level --- isUnitUnder c m | trace ("isUnitUnder " ++ show c ++ " " ++ showAssignment m) $ False = undefined - --- | Whether all the elements of the model in the list are false but one, and --- none is true, under the model. -isUnitUnder :: (Model a m) => [a] -> m -> Bool -{-# SPECIALISE INLINE isUnitUnder :: Clause -> IAssignment -> Bool #-} -isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) - && not (Fl.any (`isTrueUnder` m) c) - --- Precondition: clause is unit. --- getUnit :: (Model a m, Show a, Show m) => [a] -> m -> a --- getUnit c m | trace ("getUnit " ++ show c ++ " " ++ showAssignment m) $ False = undefined +-- | The VSIDS-like dynamic variable ordering. +newtype VarOrder s = VarOrder { varOrderArr :: STUArray s Var Double } + deriving Show +newtype FrozenVarOrder = FrozenVarOrder (UArray Var Double) + deriving Show --- | Get the element of the list which is not false under the model. If no --- such element, throws an error. -getUnit :: (Model a m, Show a) => [a] -> m -> a -{-# SPECIALISE INLINE getUnit :: Clause -> IAssignment -> Lit #-} -getUnit c m = case filter (not . (`isFalseUnder` m)) c of - [u] -> u - xs -> error $ "getUnit: not unit: " ++ show xs +-- | Each pair of watched literals is paired with its clause and id. +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)] + -- Singleton clauses are not stored in the database, they are assigned. + -- But we need to record their ids, so we put them here. + , resSourceMap :: Map ClauseId [ClauseId] } deriving (Show) +type ReasonMap = Map Var (Clause, ClauseId) +type ClauseId = Int +instance Show (STRef s a) where show = const "" +instance Show (STUArray s Var Int) where show = const "" +instance Show (STUArray s Var Double) where show = const "" +instance Show (STArray s a b) where show = const "" diff --git a/Funsat/Utils.hs b/Funsat/Utils.hs --- a/Funsat/Utils.hs +++ b/Funsat/Utils.hs @@ -34,19 +34,71 @@ module Funsat.Utils where import Control.Monad.ST.Strict -import Control.Monad.State.Lazy hiding ((>=>), forM_) +import Control.Monad.State.Lazy hiding ( (>=>), forM_ ) import Data.Array.ST import Data.Array.Unboxed -import Data.Foldable hiding (sequence_) -import Data.List (foldl1') -import Debug.Trace (trace) -import Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum) -import System.IO.Unsafe (unsafePerformIO) -import System.IO (hPutStr, stderr) +import Data.Foldable hiding ( sequence_ ) +import Data.Graph.Inductive.Graph( DynGraph, Graph ) +import Data.List( foldl1' ) +import Data.Map (Map) +import Data.Set (Set) +import Debug.Trace( trace ) +import Funsat.Types +import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) +import System.IO.Unsafe( unsafePerformIO ) +import System.IO( hPutStr, stderr ) import qualified Data.Foldable as Fl +import qualified Data.Graph.Inductive.Graph as Graph +import qualified Data.Graph.Inductive.Query.DFS as DFS import qualified Data.List as List +import qualified Data.Map as Map +import qualified Data.Set as Set + +-- | `True' if and only if the object is undefined in the model. +isUndefUnder :: Model a m => a -> m -> Bool +isUndefUnder x m = isUndef $ x `statusUnder` m + where isUndef (Left ()) = True + isUndef _ = False + +-- | `True' if and only if the object is true in the model. +isTrueUnder :: Model a m => a -> m -> Bool +isTrueUnder x m = isTrue $ x `statusUnder` m + where isTrue (Right True) = True + isTrue _ = False + +-- | `True' if and only if the object is false in the model. +isFalseUnder :: Model a m => a -> m -> Bool +isFalseUnder x m = isFalse $ x `statusUnder` m + where isFalse (Right False) = True + isFalse _ = False + +-- * Helpers + + +-- isUnitUnder c m | trace ("isUnitUnder " ++ show c ++ " " ++ showAssignment m) $ False = undefined + +-- | Whether all the elements of the model in the list are false but one, and +-- none is true, under the model. +isUnitUnder :: (Model a m) => [a] -> m -> Bool +{-# SPECIALISE INLINE isUnitUnder :: Clause -> IAssignment -> Bool #-} +isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) + && not (Fl.any (`isTrueUnder` m) c) + +-- Precondition: clause is unit. +-- getUnit :: (Model a m, Show a, Show m) => [a] -> m -> a +-- getUnit c m | trace ("getUnit " ++ show c ++ " " ++ showAssignment m) $ False = undefined + +-- | Get the element of the list which is not false under the model. If no +-- such element, throws an error. +getUnit :: (Model a m, Show a) => [a] -> m -> a +{-# SPECIALISE INLINE getUnit :: Clause -> IAssignment -> Lit #-} +getUnit c m = case filter (not . (`isFalseUnder` m)) c of + [u] -> u + xs -> error $ "getUnit: not unit: " ++ show xs + + {-# INLINE mytrace #-} mytrace msg expr = unsafePerformIO $ do hPutStr stderr msg @@ -87,7 +139,8 @@ -- | Count the number of elements in the list that satisfy the predicate. count :: (a -> Bool) -> [a] -> Int count p = foldl' f 0 - where f x y = x + (if p y then 1 else 0) + where f x y | p y = x + 1 + | otherwise = x -- | /O(1)/ @argmin f x y@ is the argument whose image is least under @f@; if -- the images are equal, returns the first. @@ -108,4 +161,121 @@ -- | Returns a predicate which holds exactly when both of the given predicates -- hold. p .&&. q = \x -> p x && q x + + +-- | Generate a cut using the given UIP node. The cut generated contains +-- exactly the (transitively) implied nodes starting with (but not including) +-- the UIP on the conflict side, with the rest of the nodes on the reason +-- side. +uipCut :: (Graph gr) => + [Lit] -- ^ decision literals + -> FrozenLevelArray + -> gr a b -- ^ conflict graph + -> Graph.Node -- ^ unassigned, implied conflicting node + -> Graph.Node -- ^ a UIP in the conflict graph + -> 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 + -- Transitively implied, and not including the UIP. + impliedByUIP = Set.insert extraNode $ + Set.fromList $ tail $ DFS.reachable uip conflGraph + -- The UIP may not imply the assigned conflict variable which needs to + -- be on the conflict side, unless it's a decision variable or the UIP + -- itself. + extraNode = if L (negate conflNode) `elem` dlits || negate conflNode == uip + then conflNode -- idempotent addition + else negate conflNode + allNodes = Set.fromList $ Graph.nodes conflGraph + + +-- | Generate a learned clause from a cut of the graph. Returns a pair of the +-- learned clause and the decision level to which to backtrack. +cutLearn :: (Graph gr, Foldable f) => IAssignment -> FrozenLevelArray + -> Cut f gr a b -> (Clause, Int) +cutLearn a levelArr cut = + ( clause + -- The new decision level is the max level of all variables in the + -- clause, excluding the uip (which is always at the current decision + -- level). + , maximum0 (map (levelArr!) . (`without` V (abs $ cutUIP cut)) . map var $ clause) ) + where + -- The clause is composed of the variables on the reason side which have + -- at least one successor on the conflict side. The value of the variable + -- is the negation of its value under the current assignment. + 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 has 0 as its max for the empty list + maximum0 xs = maximum xs + + +-- | Creates the conflict graph, where each node is labeled by its literal and +-- level. +-- +-- Useful for getting pretty graphviz output of a conflict. +mkConflGraph :: DynGraph gr => + IAssignment + -> FrozenLevelArray + -> Map Var Clause + -> [Lit] -- ^ decision lits, in rev. chron. order + -> (Lit, Clause) -- ^ conflict info + -> gr CGNodeAnnot () +mkConflGraph mFr lev reasonMap _dlits (cLit, confl) = + Graph.mkGraph nodes' edges' + where + -- we pick out all the variables from the conflict graph, specially adding + -- both literals of the conflict variable, so that that variable has two + -- nodes in the graph. + nodes' = + ((0, CGNA (L 0) (-1)) :) $ -- lambda node + ((unLit cLit, CGNA cLit (-1)) :) $ + ((negate (unLit cLit), CGNA (negate cLit) (lev!(var cLit))) :) $ + -- annotate each node with its literal and level + map (\v -> (unVar v, CGNA (varToLit v) (lev!v))) $ + filter (\v -> v /= var cLit) $ + toList nodeSet' + + -- node set includes all variables reachable from conflict. This node set + -- construction needs a `seen' set because it might infinite loop + -- otherwise. + (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) + + -- seed with both conflicting literals + 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) -- unimplied lits from reasons are + -- complemented + , 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 = -- lit to node + if var l == var cLit -- preserve sign of conflicting lit + then unLit l + else (abs . unLit) l + diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -21,11 +21,12 @@ Copyright 2008 Denis Bueno -} -import Control.Monad ( when, forM_ ) -import Data.Foldable ( fold, toList, elem ) -import Data.List ( intercalate ) +import Control.Monad( when, forM_ ) +import Data.Array.Unboxed( elems ) +import Data.Foldable( fold, toList, elem ) +import Data.List( intercalate ) import Data.Monoid -import Data.Set ( Set ) +import Data.Set( Set ) import Funsat.Solver ( solve , verify @@ -33,11 +34,11 @@ , defaultConfig , ShowWrapped(..) , statTable ) -import Funsat.Types( CNF, GenCNF(..) ) +import Funsat.Types( CNF(..) ) import Prelude hiding ( elem ) import System.Console.GetOpt -import System.Environment ( getArgs ) -import System.Exit ( ExitCode(..), exitWith ) +import System.Environment( getArgs ) +import System.Exit( ExitCode(..), exitWith ) import Data.Time.Clock import qualified Data.Set as Set import qualified Language.CNF.Parse.ParseDIMACS as ParseCNF @@ -52,15 +53,20 @@ | ClauseLearning | Restarts | VSIDS + | ResolutionChecker + | UnsatCoreGeneration deriving (Eq, Ord) instance Show Feature where show WatchedLiterals = "watched literals" show ClauseLearning = "conflict clause learning" show Restarts = "restarts" show VSIDS = "dynamic variable ordering" + show ResolutionChecker = "resolution UNSAT checker" + show UnsatCoreGeneration = "UNSAT core generation" allFeatures :: Set Feature -allFeatures = Set.fromList [WatchedLiterals, ClauseLearning, Restarts, VSIDS] +allFeatures = Set.fromList [WatchedLiterals, ClauseLearning, Restarts, VSIDS + ,ResolutionChecker, UnsatCoreGeneration] validOptions :: [OptDescr RunOptions] @@ -113,10 +119,10 @@ putStr "Enabled features: " putStrLn $ intercalate ", " $ map show $ toList (allFeatures Set.\\ features) - forM_ files $ \path -> readFile path >>= parseAndSolve path + forM_ files $ parseAndSolve where - parseAndSolve path contents = do - let cnf = asCNF $ ParseCNF.parseCNF path contents + parseAndSolve path = do + cnf <- parseCNF path putStrLn $ show (numVars cnf) ++ " variables, " ++ show (numClauses cnf) ++ " clauses" Set.map seqList (clauses cnf) @@ -146,11 +152,18 @@ seqList l@[] = l seqList l@(x:xs) = x `seq` seqList xs `seq` l +parseCNF :: FilePath -> IO CNF +parseCNF path = do + result <- ParseCNF.parseFile path + case result of + Left err -> error . show $ err + Right c -> return . asCNF $ c + -- | Convert parsed CNF to internal representation. asCNF :: ParseCNF.CNF -> CNF asCNF (ParseCNF.CNF v c is) = - CNF { numVars = v + CNF { numVars = v , numClauses = c - , clauses = Set.fromList . map (map fromIntegral) $ is } + , clauses = Set.fromList . map (map fromIntegral . elems) $ is } diff --git a/README b/README --- a/README +++ b/README @@ -1,26 +1,39 @@ -*- mode: outline -*- -* A DPLL-style SAT solver in pure Haskell +* Funsat: A DPLL-style SAT solver in pure Haskell + +Funsat is a native Haskell SAT solver that uses modern techniques for solving +SAT instances. Current features include two-watched literals, conflict-directed +learning, non-chronological backtracking, a VSIDS-like dynamic variable +ordering, and restarts. Our goal is to facilitate convenient embedding of a +reasonably fast SAT solver as a constraint solving backend in other +applications. + +Currently along this theme we provide /unsatisfiable core/ generation, giving +(hopefully) small unsatisfiable sub-problems of unsatisfiable input problems +(see "Funsat.Resolution"). + + +* Installation Install using the typical Cabal procedure: -$ ./Setup.lhs configure -$ ./Setup.lhs build + $ ghc --make -o Setup Setup.hs + $ ./Setup configure + $ ./Setup build This will produce a binary called funsat at ./dist/build/funsat/funsat and a standalone library interface for the solver. If you feel like profiling the -code, uncomment the profiling executable in funsat.cabal, and a profiling -binary will automatically be built in ./dist/build/funsat-prof/funsat-prof. +code, a profiling binary is automatically built in +./dist/build/funsat-prof/funsat-prof. ** Dependencies -All the dependences are cabal-ised and available from hackage. URLs below. - -They're also available in subdirectories. +All the dependences are cabal-ised and available from hackage, or in etc/. -*** parse-dimacs [cnf] +*** parse-dimacs A haskell CNF file parser. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parse-dimacs -*** bitset [bitset] +*** bitset http://hackage.haskell.org/cgi-bin/hackage-scripts/package/bitset diff --git a/bugs.org b/bugs.org new file mode 100644 --- /dev/null +++ b/bugs.org @@ -0,0 +1,43 @@ +#+STARTUP: content hidestars +#+TYP_TODO: DEFECT(d@) FEATURE(f@) VERIFY(v@) | FIXED(@/!) WONTFIX(@/!) POSTPONED(@/!) NOTREPRO(@/!) DUPLICATE(@/!) BYDESIGN(@/!) + + - Top-level headings are modules. + - Under each is a bug entry, initially classified as a defect or feature. + - The DONE states indicate the decision made on the bug. + +* Funsat + :PROPERTIES: + :CATEGORY: Funsat + :END: +** DEFECT resTrace field of resolution trace needn't be there + - State "DEFECT" [2008-10-10 Fri 16:30] \\ + I think it's just keeping around too much info. + +* fiblib +** FEATURE Implement ST-based fibonacci heap + - State "FEATURE" [2008-10-18 Sat 14:26] +* website + :PROPERTIES: + :CATEGORY: website + :END: + +* bitset + :PROPERTIES: + :CATEGORY: bitset + :END: + +* parse-dimacs + :PROPERTIES: + :CATEGORY: parse-dimacs + :END: +** FIXED Lazy or strict bytestrings? + - State "FIXED" [2008-10-18 Sat 14:18] \\ + Used lazy. + - State "DEFECT" [2008-10-10 Fri 16:25] \\ + I need to settle the question of whether to use lazy or strict bytestrings for + the parser. I need to benchmark it. + +* sat-micro + :PROPERTIES: + :CATEGORY: sat-micro + :END: diff --git a/funsat.cabal b/funsat.cabal --- a/funsat.cabal +++ b/funsat.cabal @@ -1,5 +1,5 @@ Name: funsat -Version: 0.5 +Version: 0.5.1 Cabal-Version: >= 1.2 Description: @@ -15,6 +15,7 @@ problems (see "Funsat.Resolution"). Synopsis: A modern DPLL-style SAT solver +Homepage: http://github.com/dbueno/funsat Category: Algorithms Stability: alpha License: LGPL @@ -22,12 +23,15 @@ Author: Denis Bueno Maintainer: Denis Bueno Build-type: Simple -Extra-source-files: README +Extra-source-files: README CHANGES bugs.org todo.org Executable funsat Main-is: Main.hs - Ghc-options: -W -funbox-strict-fields + Ghc-options: -funbox-strict-fields + -W + -fwarn-dodgy-imports -fwarn-incomplete-record-updates + -fwarn-unused-binds -fwarn-unused-imports Extensions: CPP CPP-options: -DTESTING Hs-source-dirs: . tests @@ -43,19 +47,30 @@ Properties Build-Depends: base, parsec, containers, pretty, mtl - , array, QuickCheck, parse-dimacs, bitset + , array, QuickCheck, parse-dimacs >= 1.2, bitset , fgl, time -- Executable funsat-prof -- Main-is: Main.hs --- Ghc-options: -W -prof -auto-all +-- Ghc-options: -prof -auto-all +-- -funbox-strict-fields +-- -W +-- -fwarn-dodgy-imports -fwarn-incomplete-record-updates +-- -fwarn-unused-binds -fwarn-unused-imports -- Extensions: CPP -- CPP-options: -DTESTING -- Hs-source-dirs: . tests --- Other-modules: DPLLSat Properties FastDom Utils Text.Tabular DPLL.Monad +-- Other-modules: Funsat.Solver +-- Funsat.Types +-- Funsat.Resolution +-- Funsat.FastDom +-- Funsat.Utils +-- Funsat.Monad +-- Text.Tabular -- Control.Monad.MonadST +-- Properties -- Build-Depends: base, parsec, containers, pretty, mtl --- , random, array, QuickCheck, parse-dimacs, bitset +-- , random, array, QuickCheck, parse-dimacs >= 1.2, bitset -- , fgl, time @@ -67,9 +82,12 @@ Control.Monad.MonadST Text.Tabular Other-modules: Funsat.FastDom Funsat.Utils - Ghc-options: -W -funbox-strict-fields + Ghc-options: -funbox-strict-fields + -W + -fwarn-dodgy-imports -fwarn-incomplete-record-updates + -fwarn-unused-binds -fwarn-unused-imports Extensions: CPP Hs-source-dirs: . tests Build-Depends: base, parsec, containers, pretty, mtl - , random, array, QuickCheck, parse-dimacs, bitset + , random, array, QuickCheck, parse-dimacs >= 1.2, bitset , fgl diff --git a/tests/Properties.hs b/tests/Properties.hs --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -2,20 +2,20 @@ module Properties where {- - This file is part of DPLLSat. + This file is part of funsat. - DPLLSat is free software: you can redistribute it and/or modify + funsat is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. - DPLLSat is distributed in the hope that it will be useful, + funsat is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License - along with DPLLSat. If not, see . + along with funsat. If not, see . Copyright 2008 Denis Bueno -} @@ -33,8 +33,8 @@ import Debug.Trace import Funsat.Solver( verify ) import Funsat.Types -import Funsat.Utils( count, argmin ) -import Language.CNF.Parse.ParseDIMACS( parseCNF ) +import Funsat.Utils +import Language.CNF.Parse.ParseDIMACS( parseFile ) import Prelude hiding ( or, and, all, any, elem, minimum, foldr, splitAt, concatMap , sum, concat ) import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace ) @@ -480,9 +480,10 @@ return (generate (maxVars * 3) g arbitrary) prob :: IO ParseCNF.CNF -prob = do let file = "./tests/problems/uf20/uf20-0119.cnf" - s <- readFile file - return $ parseCNF file s +prob = do cnfOrError <- parseFile "./tests/problems/uf20/uf20-0119.cnf" + case cnfOrError of + Left err -> error . show $ err + Right c -> return c -- | Convert parsed CNF to internal representation. @@ -490,7 +491,7 @@ asCNF (ParseCNF.CNF v c is) = CNF {numVars = v ,numClauses = c - ,clauses = Set.fromList . map (map fromIntegral) $ is} + ,clauses = Set.fromList . map (map fromIntegral . elems) $ is} -- import qualified Data.ByteString.Char8 as B diff --git a/todo.org b/todo.org new file mode 100644 --- /dev/null +++ b/todo.org @@ -0,0 +1,248 @@ +* Sat todo file + +* TODO Group paired result.x files into their own graphs. :GraphResult: +This would make GraphResult generate n graphs when n benchmark results are +available from both timestamps. This is just another dimension of generality +that isn't hard to support. + + +* TODO resTrace field of resolution trace in solver can go +Why do I even need the trace? I just need the original clause ids and the +source map, right? + +* DONE Export and document defaultConfig :release: + CLOSED: [2008-06-07 Sat 14:29] + +* DONE Release initial version to hackage + CLOSED: [2008-06-06 Fri 10:49] + +* DONE Derive resolution proof of UNSAT in order to aid debugging :feature: + CLOSED: [2008-06-07 Sat 20:32] +This feature essentially enables the following one, or vice versa. + ++Add Writer capability to the Funsat monad+ +Just put it in the state record. + +** DONE Write quickCheck tests for checker + CLOSED: [2008-07-07 Mon 20:05] +Use a generater that will always generate unsat problems, then check them, and +make sure unsat core is correct too. + +*** TODO [#A] Resolution.check has a bug. Find it. :bug:ARCHIVE: + +** DONE Add unique ids to clauses + CLOSED: [2008-06-07 Sat 20:32] + +** DONE [#A] Add unsatisfiable core extraction :feature: + CLOSED: [2008-06-07 Sat 14:23] + +Algorithm from DATE_2003: + +1. Each time learned clause generated, clause's ID is recorded, along with + each encountered "reason". + + So I should be able to simply assign IDs to each original clause and + learned clause. When I do the conflict analysis, each reason (by the + invariant) already has an ID. I record all of these and generate a new ID + for the learned clause. + +2. When unsat is determined, record reason for conflicting variable + assignment. That is, the clause that propagated the conflicting variable + assignment must have been false, so record its ID. [Is this true? Suppose + at decision level 0 bcp propagates -1 and 1 is assigned. It propagated -1 + because some clause was entirely false except it had -1. But 1 is + assigned. So, it must have been the clause was entirely false. Hence the + reason for the propagation of the last conflicting clause is the ID we + should record. QED.] + +3. Before returning Unsat from the solver, record all assigned variables + (which by construction are all at decision level 0) and their values, and + record the IDs of the "reason" for each variable. + +It should be sufficient to start with a linear trace of IDs along with the +final variable assignments (produced in step 3). In particular, we don't need +all the literals of each learned clause at recording time. + +** Correctness +@recursive_build@ reconstructs the clause corresponding to the input id. +First we build the final conflicting clause. This clause must be false under +the terminating assignment. Call this clause X. + +If the loop terminates and no errors, clearly we have a proper proof. + +If the loop never terminates, then X is never the empty clause. But if +resolve() finds a resolvent, cl is always "smaller". Since there are only +finitely many variables & reasons, we will get the empty clause or find an +error. + +*** In check_depth_first, can we resolve on any lit in clause & get a clause +that is false? + +Proof: +Assume SAT solver is correct. Let l be in the last clause. The antecedent +for l propagated -l (*), and therefore contains -l. Hence we can resolve and +still get a clause that is false. + +Suppose X is the antecedent clause for l in a clause Z. By induction +hypothesis, Z is false. Since X is the antecedent for l, X propagated -l (*). +... Hence, we can resolve on l preserving. + +If we cannot, SAT solver is incorrect. In particular, the assumptions marked +(*) are the ones guaranteed by the correct operation of the solver. + +*** In recursive_build + * recursive_build first bottoms out when it hits an original clause. + +**** Original clause +Suppose cl_id is an original clause. Then it is already built (i.e. should be +supplied to checker). + +If not, the clause we're constructing corresponds to a learned clause. +Construct clause CL of first source. (*) Then construct clause of second +source. Resolve them into X1. Resolve X1 with build clause of next source of +cl_id. Resolve into X2...Xn. Build and return Xn. + + [Both of these clauses are either reasons used or the conflicting clause + used when generating the learned clause. + + Suppose the conflict clause has only two sources. Obviously both must + mention the conflicting lit. Otherwise they would not be present.] + +*** Invariants +INVARIANT: every variable in the final assignment has an antecedent. This is +true if the SAT solver is correct. + +INVARIANT: every variable in an antecedent (reason) is assigned. Also true if +the SAT solver is true. + +INVARIANT: All reasons are non-empty. Duh, otherwise they could not have +propagated. + +Therefore, if any of these fails, there might be an error in the solver/trace +generation. So they should be reported as ResolutionErrors. + +* DONE Add -funbox-strict-fields to the ghc-options :bench: + CLOSED: [2008-06-06 Fri 13:49] +and see how it affects performance. + +Did this long ago. Minus the "see how it affects performance" part. + +* DONE [#A] Remove stupid command-line options :cleanup: + CLOSED: [2008-06-06 Fri 11:47] + +* TODO [#C] Initial state for dynamic variable ordering should be +based on the number of occurrences of literals in the clause database at the +beginning, or something. Some heuristic that puts important variables first +at the beginning, instead of starting out all at zero. + +* DONE [#A] Remove the monad stack from bcpLit + CLOSED: [2008-06-05 Thu 20:14] +There are three monads there! Can we just write a single monad data type on +top of ST that has errors and whatnot? + +Did this long ago. +** Result ... + +* TODO [#K] On some problems, select is a bottleneck, much :heuristics: +more than bcpLit. Even so, reverting to a static ordering gives worse +runtime. So ... if we had a faster way of selecting the min, it would be +nice. + +* TODO There is a bug in mkConflGraph :ARCHIVE: +mkConflGraph' is the old code that seemed to work, but it's much slower. + +* DONE Bug fixed + CLOSED: [2008-05-08 Thu 22:17] +** decision list wasn't reset on restarts +** propQ wasn't reset on restarts + +* TODO Problem simplification +** Whenever we restart, remove the negations of all unit facts from each clause. + +* DONE [#A] Debug clause learning + CLOSED: [2008-04-24 Thu 15:57] +Currently, bugs. + +** There is a confusion between reasons and actual assigned variables +When asking for the level of a variable in the current assignment, the +conflict variable should be treated specially -- it's at the current level. +Otherwise, you can just ask for the level of the variable. + +Say the conflicting literals is -20. Then 20 is in the current assignment --- +that's why -20 conflicts. Now, suppose you expand a literal `x' whose reason +contains -20 -- that is, since 20 is true, -20 was in a clause which became +unit, and propagated `x'. Asking for the level of -20 is wrong -- when asking +for the level of a *reason*, we always want the level of the corresponding +variable, so that we don't confuse it with the conflicting literal. + +* DONE VSIDS bumping should happen for each variable encountered + CLOSED: [2008-06-05 Thu 20:15] +while generating the learnt clause. + +* TODO [#K] Recursive learning/parallel stuff + +* DONE Learned clause deletion + CLOSED: [2008-04-03 Thu 12:18] + +* DONE Make "bad" bag use bitset + CLOSED: [2008-03-18 Tue 10:11] + +* 29 Feb 2008 16:43:29 +I had to re-install GHC 6.8.1 for a reason that is not important. I was going +to install 6.8.2, which I had to compile myself. While waiting for that, I +worked on DPLLSat with 6.8.1. My tests run in 5 seconds, without +optimisations! Last night I was waiting 10 minutes. And this is user time! +I have no idea why. I did change the unit propagation code today, but only +making it do more work! + +I'm going to install 6.8.2, and then put 6.8.1 somewhere else so I can switch +between them easily, somehow. Weird, weird. + +This could be explained by a different test distribution ... + +* DONE Make unit propagation propagate with learned clauses too. + CLOSED: [2008-03-18 Tue 10:11] + +* TODO [#K] Incorporate stupid frequency-based decision heuristic :ARCHIVE: + +* DONE Implement clause learning but only after + CLOSED: [2008-03-18 Tue 10:11] +watched literals, otherwise the number of times we have to walk the set of +clauses will really kill the runtime. + +* DONE Change watched literal imp so that we only propagate assignments + CLOSED: [2008-02-22 Fri 11:37] +that have actually been made since the last iteration; this saves time. + +So unitProp (maybe rename bcp?) should take a list of literals to propagate, +and compute until that list is emptied -- sounds like a worklist algorithm! + +* TODO Implement SAT-MICRO annotated clauses and literals :ARCHIVE: +instead of using the current dl (decision list). + +* TODO Probably don't need the cnf :ARCHIVE: +and wch fields of the state. Probably can get away with some watcher. + +* DONE [#A] Make watched literals work as follows: + CLOSED: [2008-02-22 Fri 11:38] +-- watcherMap: Map Lit [((Lit, Lit), Clause)] + +** When l first added to assignment (either decision or propagation): +if -l is watched, then for each clause associated with -l, look at -l's paired +literal, q. If q is undefined under the assignment, then: + + -- If q is a unit literal of this clause, assign q. + + -- If q is *not* a unit literal of this clause, stop watching -l and +starting watching some other literal of the clause. (Choose next by removing +everything in the assignment from the clause, then picking a random element.) + +Write this in terms of a list of newly-assigned literals, so one can recurse +at the end. + + +* DONE [#A] Change assignment representation to O(1) + CLOSED: [2008-02-13 Wed 21:59] +** DONE Lits to Int + CLOSED: [2008-02-02 Sat 11:55] +