funsat 0.5 → 0.5.1
raw patch · 12 files changed
+849/−519 lines, 12 filesdep ~parse-dimacs
Dependency ranges changed: parse-dimacs
Files
- CHANGES +7/−0
- Funsat/Monad.hs +5/−4
- Funsat/Resolution.hs +10/−14
- Funsat/Solver.hs +179/−376
- Funsat/Types.hs +92/−75
- Funsat/Utils.hs +178/−8
- Main.hs +26/−13
- README +23/−10
- bugs.org +43/−0
- funsat.cabal +27/−9
- tests/Properties.hs +11/−10
- todo.org +248/−0
+ CHANGES view
@@ -0,0 +1,7 @@+-*- mode: outline -*-++* 0.5.1+** Update for compatibility with parse-dimacs 1.2,+which should mean faster parsing.+** Code cleanup+
Funsat/Monad.hs view
@@ -68,20 +68,21 @@ -- <http://haskell.org/haskellwiki/Performance/Monads>. 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
Funsat/Resolution.hs view
@@ -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
Funsat/Solver.hs view
@@ -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 "<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>"+ , 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
Funsat/Types.hs view
@@ -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 "<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>"
Funsat/Utils.hs view
@@ -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+
Main.hs view
@@ -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 }
README view
@@ -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
+ bugs.org view
@@ -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:
funsat.cabal view
@@ -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 <dbueno@gmail.com> 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
tests/Properties.hs view
@@ -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 <http://www.gnu.org/licenses/>.+ along with funsat. If not, see <http://www.gnu.org/licenses/>. 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
+ todo.org view
@@ -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]+