diff --git a/DPLL/Monad.hs b/DPLL/Monad.hs deleted file mode 100644 --- a/DPLL/Monad.hs +++ /dev/null @@ -1,82 +0,0 @@ -{-# LANGUAGE PolymorphicComponents - ,MultiParamTypeClasses - ,FunctionalDependencies - ,FlexibleInstances - #-} - -{-| - -The main SAT solver monad. Embeds `ST'. See type `SSTErrMonad', which stands -for ''State ST Error Monad''. - -Most of the work done is in the form of `SSTErrMonad' actions. -} -module DPLL.Monad - ( liftST - , runSSTErrMonad - , evalSSTErrMonad - , SSTErrMonad ) - where -import Control.Monad.Error hiding ((>=>), forM_) -import Control.Monad.ST.Strict -import Control.Monad.State.Lazy hiding ((>=>), forM_) -import Control.Monad.MonadST - - -instance MonadST s (SSTErrMonad e st s) where - liftST = dpllST - --- | Perform an @ST@ action in the DPLL monad. -dpllST :: ST s a -> SSTErrMonad e st s a -{-# INLINE dpllST #-} -dpllST st = SSTErrMonad (\k s -> st >>= \x -> k x s) - --- | @runSSTErrMonad m s@ executes a `SSTErrMonad' action with initial state @s@ --- until an error occurs or a result is returned. -runSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> (st -> ST s (Either e a, st)) -runSSTErrMonad m = unSSTErrMonad m (\x s -> return (return x, s)) - -evalSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> st -> ST s (Either e a) -evalSSTErrMonad m s = do (result, _) <- runSSTErrMonad m s - return result - --- | @SSTErrMonad e st s a@: the error type @e@, state type @st@, @ST@ thread --- @s@ and result type @a@. --- --- This is a monad embedding @ST@ and supporting error handling and state --- threading. It uses CPS to avoid checking `Left' and `Right' for every --- `>>='; instead only checks on `catchError'. Idea adapted from --- . -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)) } - -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 -{-# 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) - put s' = SSTErrMonad (\k _ -> k () s') - -instance (Error e) => MonadError e (SSTErrMonad e st s) where - throwError err = -- throw away continuation - SSTErrMonad (\_ s -> return (Left err, s)) - catchError action handler = {-# SCC "catchErrorSSTErrMonad" #-} SSTErrMonad - (\k s -> do (x, s') <- runSSTErrMonad action s - case x of - Left error -> unSSTErrMonad (handler error) k s' - Right result -> k result s') - -instance (Error e) => MonadPlus (SSTErrMonad e st s) where - mzero = SSTErrMonad (\_ s -> return (Left noMsg, s)) - mplus m n = SSTErrMonad (\k s -> - do (r, s') <- runSSTErrMonad m s - case r of - Left _ -> unSSTErrMonad n k s' - Right x -> k x s') diff --git a/Funsat/Monad.hs b/Funsat/Monad.hs new file mode 100644 --- /dev/null +++ b/Funsat/Monad.hs @@ -0,0 +1,102 @@ +{-# LANGUAGE PolymorphicComponents + ,MultiParamTypeClasses + ,FunctionalDependencies + ,FlexibleInstances + #-} + +{- + This file is part of funsat. + + 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. + + 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 funsat. If not, see . + + Copyright 2008 Denis Bueno +-} + + +{-| + +The main SAT solver monad. Embeds `ST'. See type `SSTErrMonad', which stands +for ''State ST Error Monad''. + +-} +module Funsat.Monad + ( liftST + , runSSTErrMonad + , evalSSTErrMonad + , SSTErrMonad ) + where +import Control.Monad.Error +import Control.Monad.ST.Strict +import Control.Monad.State.Class +import Control.Monad.MonadST + + +instance MonadST s (SSTErrMonad e st s) where + liftST = dpllST + +-- | Perform an @ST@ action in the DPLL monad. +dpllST :: ST s a -> SSTErrMonad e st s a +{-# INLINE dpllST #-} +dpllST st = SSTErrMonad (\k s -> st >>= \x -> k x s) + +-- | @runSSTErrMonad m s@ executes a `SSTErrMonad' action with initial state @s@ +-- until an error occurs or a result is returned. +runSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> (st -> ST s (Either e a, st)) +runSSTErrMonad m = unSSTErrMonad m (\x s -> return (return x, s)) + +evalSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> st -> ST s (Either e a) +evalSSTErrMonad m s = do (result, _) <- runSSTErrMonad m s + return result + +-- | @SSTErrMonad e st s a@: the error type @e@, state type @st@, @ST@ thread +-- @s@ and result type @a@. +-- +-- This is a monad embedding @ST@ and supporting error handling and state +-- threading. It uses CPS to avoid checking `Left' and `Right' for every +-- `>>='; instead only checks on `catchError'. Idea adapted from +-- . +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)) } + +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 +{-# 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) + put s' = SSTErrMonad (\k _ -> k () s') + +instance (Error e) => MonadError e (SSTErrMonad e st s) where + throwError err = -- throw away continuation + SSTErrMonad (\_ s -> return (Left err, s)) + catchError action handler = {-# SCC "catchErrorSSTErrMonad" #-} SSTErrMonad + (\k s -> do (x, s') <- runSSTErrMonad action s + case x of + Left error -> unSSTErrMonad (handler error) k s' + Right result -> k result s') + +instance (Error e) => MonadPlus (SSTErrMonad e st s) where + mzero = SSTErrMonad (\_ s -> return (Left noMsg, s)) + mplus m n = SSTErrMonad (\k s -> + do (r, s') <- runSSTErrMonad m s + case r of + Left _ -> unSSTErrMonad n k s' + Right x -> k x s') diff --git a/Funsat/Resolution.hs b/Funsat/Resolution.hs new file mode 100644 --- /dev/null +++ b/Funsat/Resolution.hs @@ -0,0 +1,278 @@ + +{- + This file is part of funsat. + + 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. + + 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 funsat. If not, see . + + Copyright 2008 Denis Bueno +-} + +-- | Generates and checks a resolution proof of UNSAT from a resolution trace +-- of a SAT solver (Funsat in particular will generate this trace). This is +-- based on the implementation discussed in the paper ''Validating SAT Solvers +-- Using an Independent Resolution-Based Checker: Practical Implementations +-- and Other Applications'' by Lintao Zhang and Sharad Malik. +-- +-- As a side effect of this process an /unsatisfiable core/ is generated from +-- the resolution trace, as discussed in the paper ''Extracting Small +-- Unsatisfiable Cores from Unsatisfiable Boolean Formula'' by Zhang and +-- Malik. +module Funsat.Resolution + ( -- * Interface + checkDepthFirst + -- * Data Types + , ResolutionTrace(..) + , initResolutionTrace + , ResolutionError(..) + , UnsatisfiableCore + , ClauseId ) + where + +import Control.Monad.Error +import Control.Monad.Reader +import Control.Monad.State.Strict +import Data.IntSet( IntSet ) +import Data.List( nub ) +import Data.Map( Map ) +import qualified Data.IntSet as IntSet +import qualified Data.Map as Map +import Funsat.Types +import Funsat.Utils( isSingle ) + + +-- IDs = Ints +-- Lits = Lits + +data ResolutionTrace = ResolutionTrace + { traceFinalClauseId :: ClauseId + -- ^ The id of the last, conflicting clause in the solving process. + + , traceFinalAssignment :: IAssignment + -- ^ Final assignment. + -- + -- /Precondition/: All variables assigned at decision level zero. + + , traceSources :: Map ClauseId [ClauseId] + -- ^ /Invariant/: Each id has at least one source (otherwise that id + -- should not even have a mapping). + -- + -- /Invariant/: Should be ordered topologically backward (?) from each + -- conflict clause. (IOW, record each clause id as its encountered when + -- generating the conflict clause.) + + , traceOriginalClauses :: Map ClauseId Clause + -- ^ Original clauses of the CNF input formula. + + , traceAntecedents :: Map Var ClauseId } + deriving (Show) + +initResolutionTrace finalClauseId finalAssignment = ResolutionTrace + { traceFinalClauseId = finalClauseId + , traceFinalAssignment = finalAssignment + , traceSources = Map.empty + , 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. + + | 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. + + | AntecedentNotUnit Clause + -- ^ Indicates that the constructed antecedent clause not unit under + -- `traceFinalAssignment'. + + | AntecedentImplication (Clause, Lit) Var + -- ^ Indicates that in the clause-lit pair, the unit literal of clause + -- is the literal, but it ought to be the variable. + + | AntecedentMissing Var + -- ^ Indicates that the variable has no antecedent mapping, in which + -- case it should never have been assigned/encountered in the first + -- place. + + | EmptySource ClauseId + -- ^ Indicates that the clause id has an entry in `traceSources' but + -- no resolution sources. + + | OrphanSource ClauseId + -- ^ Indicates that the clause id is referenced but has no entry in + -- `traceSources'. + deriving Show +instance Error ResolutionError where -- Just for the Error monad. + +-- checkDepthFirstFix :: (CNF -> (Solution, Maybe ResolutionTrace)) +-- -> Solution +-- -> ResolutionTrace +-- -> Either ResolutionError UnsatisfiableCore +-- checkDepthFirstFix solver resTrace = +-- case checkDepthFirst resTrace of +-- Left err -> err +-- Right ucore -> +-- let (sol, rt) solver (rescaleIntoCNF ucore) + +-- | The depth-first method. +checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore +checkDepthFirst resTrace = + -- Turn internal unsat core into external. + fmap (map findClause . IntSet.toList) + + -- Check and create unsat core. + . (`runReader` resTrace) + . (`evalStateT` ResState { clauseIdMap = traceOriginalClauses resTrace + , unsatCore = IntSet.empty }) + . runErrorT + $ recursiveBuild (traceFinalClauseId resTrace) + >>= checkDFClause + + where + findClause clauseId = + Map.findWithDefault + (error $ "checkDFClause: unoriginal clause id: " ++ show clauseId) + clauseId (traceOriginalClauses resTrace) + + + +-- | Unsatisfiable cores are not unique. +type UnsatisfiableCore = [Clause] + + +------------------------------------------------------------------------------ +-- MAIN INTERNALS +------------------------------------------------------------------------------ + +data ResState = ResState + { clauseIdMap :: Map ClauseId Clause + , unsatCore :: UnsatCoreIntSet + } + +type UnsatCoreIntSet = IntSet -- set of ClauseIds + +type ResM = ErrorT ResolutionError (StateT ResState (Reader ResolutionTrace)) + + +-- Recursively resolve the (final, initially) clause with antecedents until +-- the empty clause is created. +checkDFClause :: Clause -> ResM UnsatCoreIntSet +checkDFClause clause = + if null clause + then gets unsatCore + else do l <- chooseLiteral clause + let v = var l + anteClause <- recursiveBuild =<< getAntecedentId v + checkAnteClause v anteClause + resClause <- resolve (Just v) clause anteClause + checkDFClause resClause + +recursiveBuild :: ClauseId -> ResM Clause +recursiveBuild clauseId {-id-} = do + maybeClause <- getClause + case maybeClause of + Just clause -> return clause + Nothing -> do + sourcesMap <- asks traceSources + case Map.lookup clauseId sourcesMap of + Nothing -> throwError (OrphanSource clauseId) + Just [] -> throwError (EmptySource clauseId) + Just (firstSourceId:ids) -> recursiveBuildIds clauseId firstSourceId ids + where + -- If clause is an *original* clause, stash it as part of the UNSAT core. + getClause = do + origMap <- asks traceOriginalClauses + case Map.lookup clauseId origMap of + Just origClause -> withClauseInCore $ return (Just origClause) + Nothing -> Map.lookup clauseId `liftM` gets clauseIdMap + + withClauseInCore = + (modify (\s -> s{ unsatCore = IntSet.insert clauseId (unsatCore s) }) >>) + +recursiveBuildIds clauseId firstSourceId sourceIds = do + rc <- recursiveBuild firstSourceId -- recursive_build(id) + clause <- foldM buildAndResolve rc sourceIds + storeClauseId clauseId clause + return clause + + where + -- This is the body of the while loop inside the recursiveBuild + -- procedure in the paper. + buildAndResolve :: Clause -> ClauseId -> ResM (Clause) + buildAndResolve clause1 clauseId = + recursiveBuild clauseId >>= resolve Nothing clause1 + + -- Maps ClauseId to built Clause. + storeClauseId :: ClauseId -> Clause -> ResM () + storeClauseId clauseId clause = modify $ \s -> + s{ clauseIdMap = Map.insert clauseId clause (clauseIdMap s) } + + +------------------------------------------------------------------------------ +-- HELPERS +------------------------------------------------------------------------------ + + +-- | Resolve both clauses on the given variable, and throw a resolution error +-- if anything is amiss. Specifically, it checks that there is exactly one +-- occurrence of a literal with the given variable (if variable given) in each +-- clause and they are opposite in polarity. +-- +-- If no variable specified, finds resolving variable, and ensures there's +-- only one such variable. +resolve :: Maybe Var -> Clause -> Clause -> ResM Clause +resolve maybeV c1 c2 = + -- Find complementary literals: + case filter ((`elem` c2) . negate) c1 of + [l] -> case maybeV of + Nothing -> resolveVar (var l) + Just v -> if v == var l + then resolveVar v + else throwError $ ResolveError v c1 c2 + vs -> throwError $ CannotResolve (nub . map var $ vs) c1 c2 + where + resolveVar v = return . nub $ deleteVar v c1 ++ deleteVar v c2 + + deleteVar v c = c `without` lit v `without` negate (lit v) + lit (V i) = L i + +-- | Get the antecedent (reason) for a variable. Every variable encountered +-- ought to have a reason. +getAntecedentId :: Var -> ResM ClauseId +getAntecedentId v = do + anteMap <- asks traceAntecedents + case Map.lookup v anteMap of + Nothing -> throwError (AntecedentMissing v) + Just ante -> return ante + +chooseLiteral :: Clause -> ResM Lit +chooseLiteral (l:_) = return l +chooseLiteral _ = error "chooseLiteral: empty clause" + +checkAnteClause :: Var -> Clause -> ResM () +checkAnteClause v anteClause = do + a <- asks traceFinalAssignment + when (not (anteClause `hasUnitUnder` a)) + (throwError $ AntecedentNotUnit anteClause) + let unitLit = getUnit anteClause a + when (not $ var unitLit == v) + (throwError $ AntecedentImplication (anteClause, unitLit) v) + where + hasUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) diff --git a/Funsat/Solver.hs b/Funsat/Solver.hs --- a/Funsat/Solver.hs +++ b/Funsat/Solver.hs @@ -18,1397 +18,1220 @@ {-| -Goal: A reasonably efficient, easy-to-understand modern sat solver. I want it -as architecturally simple as the description in /Abstract DPLL and Abstract -DPLL Modulo Theories/ is conceptually, while retaining some efficient -optimisations. - - Current state: decision heuristic\/code cleanup\/tests. - -* 24 Apr 2008 16:47:56 - -After some investigating, mad coding, and cursing, First UIP clause learning -has been implemented. For conceptual clarity, though, it is implemented in -terms of an explicit conflict graph, explicit dominator calculation, and -explicit cuts. Profiling shows that for conflict-heavy problems, -conflict-clause generation is no more a bottleneck than boolean constraint -propagation. - -This can and will be improved later. - -* 15 Dec 2007 22:46:11 - -backJump appears to work now. I used to have both Just and Nothing cases -there, but there was no reason why, since either you always reverse some past -decision (maybe the most recent one). Well, the problem had to do with -DecisionMap. Basically instead of keeping around the implications of a -decision literal (those as a result of unit propagation *and* reversed -decisions of higher decision levels), I was throwing them away. This was bad -for backJump. - -Anyway, now it appears to work properly. - -* 08 Dec 2007 22:15:44 - -IT IS ALIVE - -I do need the /bad/ variables to be kept around, but I should only update the -list after I'm forced to backtrack *all the way to decision level 0*. Only -then is a variable bad. The Chaff paper makes you think you mark it as /tried -both ways/ the *first* time you see that, no matter the decision level. - -On the other hand, why do I need a bad variable list at all? The DPLL paper -doesn't imply that I should. Hmm. - -* 08 Dec 2007 20:16:17 - -For some reason, the /unsat/ (or /fail/ condition, in the DPLL paper) was not -sufficient: I was trying out all possible assignments but in the end I didn't -get a conflict, just no more options. So I added an or to test for that case -in `unsat'. Still getting assignments under which some clauses are undefined; -though, it appears they can always be extended to proper, satisfying -assignments. But why does it stop before then? - -* 20 Nov 2007 14:52:51 - -Any time I've spent coding on this I've spent trying to figure out why some -inputs cause divergence. I finally figured out how (easily) to print out the -assignment after each step, and indeed the same decisions were being made -over, and over, and over again. So I decided to keep a /bad/ list of literals -which have been tried both ways, without success, so that decLit never decides -based on one of those literals. Now it terminates, but the models are (at -least) non-total, and (possibly) simply incorrect. This leads me to believ -that either (1) the DPLL paper is wrong about not having to keep track of -whether you've tried a particular variable both ways, or (2) I misread the -paper or (3) I implemented incorrectly what is in the paper. Hopefully before -I die I will know which of the three is the case. - -* 17 Nov 2007 11:58:59: - -Profiling reveals instance Model Lit Assignment accounts for 74% of time, and -instance Model Lit Clause Assignment accounts for 12% of time. These occur in -the call graph under unitPropLit. So clearly I need a *better way of -searching for the next unit literal*. - -* Bibliography - -''Abstract DPLL and DPLL Modulo Theories'' - -''Chaff: Engineering an Efficient SAT solver'' - -''An Extensible SAT-solver'' by Niklas Een, Niklas Sorensson - -''Efficient Conflict Driven Learning in a Boolean Satisfiability Solver'' by -Zhang, Madigan, Moskewicz, Malik - -''SAT-MICRO: petit mais costaud!'' by Conchon, Kanig, and Lescuyer - --} -module Funsat.Solver -#ifndef TESTING - ( solve - , solve1 - , DPLLConfig(..) - , Solution(..) - , IAssignment - , litAssignment - , litSign - , Stats(..) - , CNF - , GenCNF(..) - , Clause - , Lit(..) - , Var(..) - , var - , NonStupidString(..) - , statTable - , verify - ) -#endif - where - -{- - This file is part of funsat. - - 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. - - 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 funsat. If not, see . - - Copyright 2008 Denis Bueno --} - - -import Control.Arrow ((&&&)) -import Control.Exception (assert) -import Control.Monad.Error hiding ((>=>), forM_, runErrorT) -import Control.Monad.MonadST( MonadST(..) ) -import Control.Monad.ST.Strict -import Control.Monad.State.Lazy hiding ((>=>), forM_) -import Data.Array.ST -import Data.Array.Unboxed -import Data.BitSet (BitSet) -import Data.Foldable hiding (sequence_) -import Data.Graph.Inductive.Graph( DynGraph, Graph ) -import Data.Graph.Inductive.Graphviz -import Data.Graph.Inductive.Tree( Gr ) -import Data.Int (Int64) -import Data.List (intercalate, nub, tails, sortBy, intersect, sort) -import Data.Map (Map) -import Data.Maybe -import Data.Ord (comparing) -import Data.STRef -import Data.Sequence (Seq) -import Data.Set (Set) -import Debug.Trace (trace) -import Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum) -import Text.Printf( printf ) -import Funsat.Utils -import DPLL.Monad -import qualified Data.BitSet as BitSet -import qualified Data.Graph.Inductive.Graph as Graph -import qualified Data.Graph.Inductive.Query.BFS as BFS -import qualified Data.Graph.Inductive.Query.DFS as DFS -import qualified Data.Foldable as Fl -import qualified Data.List as List -import qualified Data.Map as Map -import qualified Data.Sequence as Seq -import qualified Data.Set as Set -import qualified Funsat.FastDom as Dom -import qualified Text.Tabular as Tabular - --- * Interface - --- | Run the DPLL-based SAT solver on the given CNF instance. -solve :: DPLLConfig -> CNF -> (Solution, Stats) -solve cfg fIn = - -- To solve, we simply take baby steps toward the solution using solveStep, - -- starting with an initial assignment. --- trace ("input " ++ show f) $ - either (error "no solution") id $ - runST $ - evalSSTErrMonad - (do sol <- stepToSolution $ do - initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0 - isUnsat <- initialState initialAssignment - if isUnsat then return (Right Unsat) - else solveStep initialAssignment - stats <- extractStats - return (sol, stats)) - SC{ cnf=f{clauses = Set.empty}, dl=[] - , watches=undefined, learnt=undefined, propQ=Seq.empty - , trail=[], numConfl=0, level=undefined, numConflTotal=0 - , numDecisions=0, numImpl=0 - , reason=Map.empty, varOrder=undefined - , dpllConfig=cfg } - where - f = preprocessCNF fIn - -- If returns True, then problem is unsat. - initialState :: MAssignment s -> DPLLMonad s Bool - initialState m = do - initialLevel <- liftST $ newSTUArray (V 1, V (numVars f)) noLevel - modify $ \s -> s{level = initialLevel} - initialWatches <- liftST $ newSTArray (L (- (numVars f)), L (numVars f)) [] - modify $ \s -> s{ watches = initialWatches } - initialLearnts <- liftST $ newSTArray (L (- (numVars f)), L (numVars f)) [] - modify $ \s -> s{ learnt = initialLearnts } - initialVarOrder <- liftST $ newSTUArray (V 1, V (numVars f)) initialActivity - modify $ \s -> s{ varOrder = VarOrder initialVarOrder } - - (`catchError` (const $ return True)) $ do - forM_ (clauses f) - (\c -> do isConsistent <- watchClause m c False - when (not isConsistent) - -- conflict data is ignored here, so safe to fake - (throwError (L 0, []))) - return False - - --- | Solve with a default configuration `defaultConfig' (for debugging). -solve1 :: CNF -> (Solution, Stats) -solve1 f = solve (defaultConfig f) f - --- | Configuration parameters for the solver. -data DPLLConfig = Cfg - { configRestart :: !Int64 -- ^ Number of conflicts before a restart. - , configRestartBump :: !Double -- ^ `configRestart' is altered after each - -- restart by multiplying it by this value. - , configUseVSIDS :: !Bool -- ^ If true, use dynamic variable ordering. - , configUseWatchedLiterals :: !Bool -- ^ If true, use watched literals - -- scheme. - , configUseRestarts :: !Bool - , configUseLearning :: !Bool } - deriving Show - --- | A default configuration based on the formula to solve. -defaultConfig :: CNF -> DPLLConfig -defaultConfig f = Cfg { configRestart = 100 -- fromIntegral $ max (numVars f `div` 10) 100 - , configRestartBump = 1.5 - , configUseVSIDS = True - , configUseWatchedLiterals = True - , configUseRestarts = True - , configUseLearning = True } - --- * Preprocessing - --- | Some kind of preprocessing. --- --- * remove duplicates -preprocessCNF :: CNF -> CNF -preprocessCNF f = f{clauses = simpClauses (clauses f)} - where simpClauses = Set.map nub -- rm dups - --- | Simplify the clause database. Eventually should supersede, probably, --- `preprocessCNF'. --- --- Precondition: no decisions. -simplifyDB :: IAssignment -> DPLLMonad s () -simplifyDB mFr = do - -- For each clause in the database, remove it if satisfied; if it contains a - -- literal whose negation is assigned, delete that literal. - n <- numVars `liftM` gets cnf - s <- get - liftST . forM_ [V 1 .. V n] $ \i -> when (mFr!i /= 0) $ do - let l = L (mFr!i) - filterL _i = map (\(p, c) -> (p, filter (/= negate l) c)) - -- Remove unsat literal `negate l' from clauses. - modifyArray (watches s) l filterL - modifyArray (learnt s) l filterL - -- Clauses containing `l' are Sat. - writeArray (watches s) (negate l) [] - writeArray (learnt s) (negate l) [] - --- * Internals - --- | The DPLL procedure is modeled as a state transition system. This --- 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 m = do - unsafeFreezeAss m >>= solveStepInvariants - conf <- gets dpllConfig - let selector = if configUseVSIDS conf then select else selectStatic - let bcper = if configUseWatchedLiterals conf then bcp else bcpDumb - maybeConfl <- bcper m - mFr <- unsafeFreezeAss m - s <- get - voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze . varOrderArr . varOrder $ s) - newState $ - -- Check if unsat. - unsat maybeConfl s ==> return Nothing - -- Unit propagation may reveal conflicts; check. - >< maybeConfl >=> backJump m - -- No conflicts. Decide. - >< 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 -> step >>= return . maybe (Right Unsat) Left - --- | Check data structure invariants. Unless @-fno-ignore-asserts@ is passed, --- this should be optimised away to nothing. -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 () - - --- | 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. -data Solution = Sat IAssignment | Unsat deriving (Eq) - --- | 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" - - --- ** Star Data Types - -newtype Var = V {unVar :: Int} deriving (Eq, Ord, Enum, Ix) - -instance Show Var where - show (V i) = show i ++ "v" - -instance Num Var where - _ + _ = error "+ doesn't make sense for variables" - _ - _ = error "- doesn't make sense for variables" - _ * _ = error "* doesn't make sense for variables" - signum _ = error "signum doesn't make sense for variables" - negate = error "negate doesn't make sense for variables" - abs = id - fromInteger l | l <= 0 = error $ show l ++ " is not a variable" - | otherwise = V $ fromInteger l - -newtype Lit = L {unLit :: Int} deriving (Eq, Ord, Enum, Ix) -inLit f = L . f . unLit - --- | The polarity of the literal. Negative literals are false; positive --- literals are true. -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" - _ * _ = error "* doesn't make sense for literals" - signum _ = error "signum doesn't make sense for literals" - negate = inLit negate - abs = inLit abs - fromInteger l | l == 0 = error "0 is not a literal" - | otherwise = L $ fromInteger l - -type Clause = [Lit] - --- | ''Generic'' conjunctive normal form. It's ''generic'' because the --- elements of the clause set are polymorphic. And they are polymorphic so --- that I can get a `Foldable' instance. -data GenCNF a = CNF { - numVars :: Int, - numClauses :: Int, - clauses :: Set a - } - deriving (Show, Read, Eq) - -type CNF = GenCNF Clause - -instance Foldable GenCNF where - -- TODO it might be easy to make this instance more efficient. - foldMap toM cnf = foldMap toM (clauses cnf) - - --- | There are a bunch of things in the state which are essentially used as --- ''set-like'' objects. I've distilled their interface into three methods. --- These methods are used extensively in the implementation of the solver. -class Ord a => Setlike t a where - -- | The set-like object with an element removed. - without :: t -> a -> t - -- | The set-like object with an element included. - with :: t -> a -> t - -- | Whether the set-like object contains a certain element. - contains :: t -> a -> Bool - -instance Ord a => Setlike (Set a) a where - without = flip Set.delete - with = flip Set.insert - contains = flip Set.member - -instance Ord a => Setlike [a] a where - without = flip List.delete - with = flip (:) - contains = flip List.elem - -instance Setlike IAssignment Lit where - without a l = a // [(var l, 0)] - with a l = a // [(var l, unLit l)] - contains a l = unLit l == a ! (var l) - -instance (Ord k, Ord a) => Setlike (Map k a) (k, a) where - with m (k,v) = Map.insert k v m - without m (k,_) = Map.delete k m - contains = error "no contains for Setlike (Map k a) (k, a)" - -instance (Ord a, BitSet.Hash a) => Setlike (BitSet a) a where - with = flip BitSet.insert - without = flip BitSet.delete - contains = flip BitSet.member - - -instance (BitSet.Hash Lit) where - hash l = if li > 0 then 2 * vi else (2 * vi) + 1 - where li = unLit l - vi = abs li - -instance (BitSet.Hash Var) where - hash = unVar - - --- | An ''immutable assignment''. Stores the current assignment according to --- the following convention. A literal @L i@ is in the assignment if in --- location @(abs i)@ in the array, @i@ is present. Literal @L i@ is absent --- if in location @(abs i)@ there is 0. It is an error if the location @(abs --- i)@ is any value other than @0@ or @i@ or @negate i@. --- --- Note that the `Model' instance for `Lit' and `IAssignment' takes constant --- time to execute because of this representation for assignments. Also --- updating an assignment with newly-assigned literals takes constant time, --- and can be done destructively, but safely. -type IAssignment = UArray Var Int - --- | Mutable array corresponding to the `IAssignment' representation. -type MAssignment s = STUArray s Var Int - --- | Same as @freeze@, but at the right type so GHC doesn't yell at me. -freezeAss :: MAssignment s -> ST s IAssignment -freezeAss = freeze --- | See `freezeAss'. -unsafeFreezeAss :: MAssignment s -> DPLLMonad s IAssignment -unsafeFreezeAss = liftST . unsafeFreeze - -thawAss :: IAssignment -> ST s (MAssignment s) -thawAss = thaw -unsafeThawAss :: IAssignment -> ST s (MAssignment s) -unsafeThawAss = unsafeThaw - --- | Destructively update the assignment with the given literal. -assign :: MAssignment s -> Lit -> ST s (MAssignment s) -assign a l = writeArray a (var l) (unLit l) >> return a - --- | Destructively undo the assignment to the given literal. -unassign :: MAssignment s -> Lit -> ST s (MAssignment s) -unassign a l = writeArray a (var l) 0 >> return a - - --- | An instance of this class is able to answer the question, Is a --- truth-functional object @x@ true under the model @m@? Or is @m@ a model --- for @x@? There are three possible answers for this question: `True' (''the --- object is true under @m@''), `False' (''the object is false under @m@''), --- and undefined, meaning its status is uncertain or unknown (as is the case --- with a partial assignment). --- --- The only method in this class is so named so it reads well when used infix. --- Also see: `isTrueUnder', `isFalseUnder', `isUndefUnder'. -class Model a m where - -- | @x ``statusUnder`` m@ should use @Right@ if the status of @x@ is - -- defined, and @Left@ otherwise. - statusUnder :: a -> m -> Either () Bool - --- /O(1)/. -instance Model Lit IAssignment where - statusUnder l a | a `contains` l = Right True - | a `contains` negate l = Right False - | otherwise = Left () -instance Model Var IAssignment where - statusUnder v a | a `contains` pos = Right True - | a `contains` neg = Right False - | otherwise = Left () - where pos = L (unVar v) - neg = negate pos -instance Model Clause IAssignment where - statusUnder c m - -- true if c intersect m is not null == a member of c in m - | Fl.any (\e -> m `contains` e) c = Right True - -- 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 - --- | `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 - --- isUnitUnder c m | trace ("isUnitUnder " ++ show c ++ " " ++ showAssignment m) $ False = undefined -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 -getUnit c m = case filter (not . (`isFalseUnder` m)) c of - [u] -> u - xs -> error $ "getUnit: not unit: " ++ show xs - -type Level = Int - --- | 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 - --- | 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. -type WatchedPair s = (STRef s (Lit, Lit), Clause) -type WatchArray s = STArray s Lit [WatchedPair s] - --- ** DPLL State and Phases - -data DPLLStateContents s = SC - { cnf :: CNF -- ^ The problem. - , dl :: [Lit] - -- ^ The decision level (last decided literal on front). - , watches :: WatchArray s - -- ^ Invariant: if @l@ maps to @((x, y), c)@, then @x == l || y == l@. - , learnt :: WatchArray s - -- ^ Same invariant as `watches', but only contains learned conflict - -- clauses. - , propQ :: Seq Lit - -- ^ A FIFO queue of literals to propagate. This should not be - -- manipulated directly; see `enqueue' and `dequeue'. - , level :: LevelArray s - , trail :: [Lit] - -- ^ Chronological trail of assignments, last-assignment-at-head. - , reason :: Map Var Clause - -- ^ For each variable, the clause that (was unit and) implied its value. - , numConfl :: !Int64 - -- ^ The number of conflicts that have occurred since the last restart. - , numConflTotal :: !Int64 - -- ^ The total number of conflicts. - , numDecisions :: !Int64 - -- ^ The total number of decisions. - , numImpl :: !Int64 - -- ^ The total number of implications (propagations). - , varOrder :: VarOrder s - , 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 "" - --- | 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 --- `DPLLStateContents' and is not mutable. -type DPLLMonad' s = StateT (DPLLStateContents s) (ST s) -instance Control.Monad.MonadST.MonadST s (DPLLMonad' s) where - liftST = lift - - -type DPLLMonad s = SSTErrMonad (Lit, Clause) (DPLLStateContents s) s - - --- *** Boolean constraint propagation - --- | Assign a new literal, and enqueue any implied assignments. If a conflict --- is detected, return @Just (impliedLit, conflictingClause)@; otherwise --- return @Nothing@. The @impliedLit@ is implied by the clause, but conflicts --- with the assignment. --- --- If no new clauses are unit (i.e. no implied assignments), simply update --- watched literals. -bcpLit :: MAssignment s - -> Lit -- ^ Assigned literal which might propagate. - -> DPLLMonad s (Maybe (Lit, Clause)) -bcpLit m l = do - ws <- gets watches ; ls <- gets learnt - clauses <- liftST $ readArray ws l - learnts <- liftST $ readArray ls l - liftST $ do writeArray ws l [] ; writeArray ls l [] - - -- Update wather lists for normal & learnt clauses; if conflict is found, - -- return that and don't update anything else. - (`catchError` return . Just) $ do - {-# SCC "bcpWatches" #-} forM_ (tails clauses) (updateWatches - (\ f l -> liftST $ modifyArray ws l (const f))) - {-# SCC "bcpLearnts" #-} forM_ (tails learnts) (updateWatches - (\ f l -> liftST $ modifyArray ls l (const f))) - return Nothing -- no conflict - where - -- updateWatches: `l' has been assigned, so we look at the clauses in - -- which contain @negate l@, namely the watcher list for l. For each - -- annotated clause, find the status of its watched literals. If a - -- conflict is found, the at-fault clause is returned through Left, and - -- the unprocessed clauses are placed back into the appropriate watcher - -- list. - {-# INLINE updateWatches #-} - updateWatches _ [] = return () - updateWatches alter (annCl@(watchRef, c) : restClauses) = do - mFr <- unsafeFreezeAss m - q <- liftST $ do (x, y) <- readSTRef watchRef - return $ if x == l then y else x - -- l,q are the (negated) literals being watched for clause c. - if negate q `isTrueUnder` mFr -- if other true, clause already sat - then alter (annCl:) l - else - case find (\x -> x /= negate q && x /= negate l - && not (x `isFalseUnder` mFr)) c of - Just l' -> do -- found unassigned literal, negate l', to watch - liftST $ writeSTRef watchRef (q, negate l') - alter (annCl:) (negate l') - - Nothing -> do -- all other lits false, clause is unit - modify $ \s -> s{ numImpl = numImpl s + 1 } - alter (annCl:) l - isConsistent <- enqueue m (negate q) (Just c) - when (not isConsistent) $ do -- unit literal is conflicting - alter (restClauses ++) l - clearQueue - throwError (negate q, c) - --- | Boolean constraint propagation of all literals in `propQ'. If a conflict --- is found it is returned exactly as described for `bcpLit'. -bcp :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause)) -bcp m = do - q <- gets propQ - if Seq.null q then return Nothing - else do - p <- dequeue - bcpLit m p >>= maybe (bcp m) (return . Just) - -bcpDumb :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause)) -bcpDumb m = do - mFr <- liftST $ freezeAss m - s <- get - let candidates = Set.filter (not . (`isTrueUnder` mFr)) (clauses . cnf $ s) - case find (`isFalseUnder` mFr) candidates of - Just fClause -> return $ Just (head fClause, fClause) - Nothing -> - case find (`isUnitUnder` mFr) candidates of - Nothing -> return Nothing - Just clause -> do - let unitLit = getUnit clause mFr - modify $ \s -> s{ numImpl = numImpl s + 1 } - isConsistent <- assert (unitLit `isUndefUnder` mFr) $ - enqueue m unitLit (Just clause) - clearQueue - if not isConsistent - then return $ Just (unitLit, clause) - else bcpDumb m - - --- *** Decisions - --- | Find and return a decision variable. A /decision variable/ must be (1) --- undefined under the assignment and (2) it or its negation occur in the --- formula. --- --- Select a decision variable, if possible, and return it and the adjusted --- `VarOrder'. -select :: IAssignment -> FrozenVarOrder -> Maybe Var -{-# INLINE select #-} -select = varOrderGet - -selectStatic :: IAssignment -> a -> Maybe Var -{-# INLINE selectStatic #-} -selectStatic m _ = find (`isUndefUnder` m) (range . bounds $ m) - --- | Assign given decision variable. Records the current assignment before --- deciding on the decision variable indexing the assignment. -decide :: MAssignment s -> Var -> DPLLMonad s (Maybe (MAssignment s)) -decide m v = do - let ld = L (unVar v) - (SC{dl=dl}) <- get --- trace ("decide " ++ show ld) $ return () - modify $ \s -> s{ dl = ld:dl - , numDecisions = numDecisions s + 1 } - enqueue m ld Nothing - return $ Just m - - - --- *** Backtracking - --- | Non-chronological backtracking. The current returns the learned clause --- implied by the first unique implication point cut of the conflict graph. -backJump :: MAssignment s - -> (Lit, Clause) - -- ^ @(l, c)@, where attempting to assign @l@ conflicted with - -- clause @c@. - -> DPLLMonad s (Maybe (MAssignment s)) -backJump m c@(_, _conflict) = get >>= \(SC{dl=dl, reason=_reason}) -> do - _theTrail <- gets trail --- trace ("********** conflict = " ++ show c) $ return () --- trace ("trail = " ++ show _theTrail) $ return () --- trace ("dlits (" ++ show (length dl) ++ ") = " ++ show dl) $ return () --- ++ "reason: " ++ Map.showTree _reason --- ) ( - modify $ \s -> s{ numConfl = numConfl s + 1 - , numConflTotal = numConflTotal s + 1 } - levelArr :: FrozenLevelArray <- do s <- get - liftST $ unsafeFreeze (level s) - (learntCl, newLevel) <- - do mFr <- unsafeFreezeAss m - useLearning <- configUseLearning `liftM` gets dpllConfig - if useLearning then analyse mFr levelArr dl c - else analyseDecision mFr levelArr dl c - s <- get - let numDecisionsToUndo = length dl - newLevel - dl' = drop numDecisionsToUndo dl - undoneLits = takeWhile (\lit -> levelArr ! (var lit) > newLevel) (trail s) - forM_ undoneLits $ const (undoOne m) -- backtrack - mFr <- unsafeFreezeAss m - assert (numDecisionsToUndo > 0) $ - assert (not (null learntCl)) $ - assert (learntCl `isUnitUnder` mFr) $ - modify $ \s -> s{ dl = dl' } -- undo decisions - mFr <- unsafeFreezeAss m --- trace ("new mFr: " ++ showAssignment mFr) $ return () - -- TODO once I'm sure this works I don't need getUnit, I can just use the - -- uip of the cut. - enqueue m (getUnit learntCl mFr) (Just learntCl) -- learntCl is asserting - watchClause m learntCl True - return $ Just m - - - --- Use the Decision first UIP clause, i.e, the crappiest one. -analyseDecision :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause) - -> DPLLMonad s (Clause, Int) -analyseDecision mFr levelArr dlits c@(cLit, _cClause) = do - st <- get - let decisionCut = uipCut dlits levelArr conflGraph (unLit cLit) - (decisionUIP conflGraph) - conflGraph = mkConflGraph mFr levelArr (reason st) dlits c - :: Gr CGNodeAnnot () - return $ cutLearn mFr levelArr decisionCut - where - decisionUIP :: (Graph gr) => gr CGNodeAnnot () -> Graph.Node - decisionUIP _ = abs . unLit $ head dlits - --- | @doWhile cmd test@ first runs @cmd@, then loops testing @test@ and --- executing @cmd@. The traditional @do-while@ semantics, in other words. -doWhile :: (Monad m) => m () -> m Bool -> m () -doWhile body test = do - body - shouldContinue <- test - when shouldContinue $ doWhile body test - --- | Analyse a the conflict graph and produce a learned clause. We use the --- First UIP cut of the conflict graph. --- --- May undo part of the trail, but not past the current decision level. -analyse :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause) - -> DPLLMonad s (Clause, Int) -- ^ learned clause and new decision - -- level -analyse mFr levelArr dlits (cLit, cClause) = do - st <- get --- trace ("mFr: " ++ showAssignment mFr) $ assert True (return ()) --- let (learntCl, newLevel) = cutLearn mFr levelArr firstUIPCut --- firstUIPCut = uipCut dlits levelArr conflGraph (unLit cLit) --- (firstUIP conflGraph) --- conflGraph = mkConflGraph mFr levelArr (reason st) dlits c --- :: Gr CGNodeAnnot () --- trace ("graphviz graph:\n" ++ graphviz' conflGraph) $ return () --- trace ("cut: " ++ show firstUIPCut) $ return () --- trace ("topSort: " ++ show topSortNodes) $ return () --- trace ("dlits (" ++ show (length dlits) ++ "): " ++ show dlits) $ return () --- trace ("learnt: " ++ show (map (\l -> (l, levelArr!(var l))) learntCl, newLevel)) $ return () --- outputConflict "conflict.dot" (graphviz' conflGraph) $ return () --- return $ (learntCl, newLevel) - m <- liftST $ unsafeThawAss mFr - a <- firstUIPBFS m (numVars . cnf $ st) (reason st) --- trace ("firstUIPBFS learned: " ++ show a) $ return () - return a - where - -- BFS by undoing the trail backward. From Minisat paper. - firstUIPBFS :: MAssignment s -> Int -> Map Var Clause -> DPLLMonad s (Clause, Int) - firstUIPBFS m nVars reasonMap = do - -- Literals we should process. - seenArr <- liftST $ newSTUArray (V 1, V nVars) False - counterR <- liftST $ newSTRef 0 -- Number of unprocessed current-level - -- lits we know about. - pR <- liftST $ newSTRef cLit -- Invariant: literal from current dec. lev. - out_learnedR <- liftST $ newSTRef [] - out_btlevelR <- liftST $ newSTRef 0 - let reasonL l = (if l == cLit then cClause - else Map.findWithDefault [] (var l) reasonMap - `without` l) - - (`doWhile` (liftST (readSTRef counterR) >>= return . (> 0))) $ - do p <- liftST $ readSTRef pR - forM_ (reasonL p) (bump . var) - -- For each unseen reason, - -- > from the current level, bump counter - -- > from lower level, put in learned clause - liftST . forM_ (reasonL p) $ \q -> do - seenq <- readArray seenArr (var q) - when (not seenq) $ - do writeArray seenArr (var q) True - if levelL q == currentLevel - then modifySTRef counterR (+ 1) - else if levelL q > 0 - then do modifySTRef out_learnedR (q:) - modifySTRef out_btlevelR $ max (levelL q) - else return () - -- Select next literal to look at: - (`doWhile` (liftST (readSTRef pR >>= readArray seenArr . var) - >>= return . not)) $ do - p <- head `liftM` gets trail -- a dec. var. only if the counter = - -- 1, i.e., loop terminates now - liftST $ writeSTRef pR p - undoOne m - -- Invariant states p is from current level, so when we're done - -- with it, we've thrown away one lit. from counting toward - -- counter. - liftST $ modifySTRef counterR (\c -> c - 1) - p <- liftST $ readSTRef pR - liftST $ modifySTRef out_learnedR (negate p:) - bump . var $ p - out_learned <- liftST $ readSTRef out_learnedR - out_btlevel <- liftST $ readSTRef out_btlevelR - return (out_learned, out_btlevel) - - firstUIP conflGraph = -- trace ("--> uips = " ++ show uips) $ --- trace ("--> dom " ++ show conflNode --- ++ " = " ++ show domConfl) $ --- trace ("--> dom " ++ show (negate conflNode) --- ++ " = " ++ show domAssigned) $ - argminimum distanceFromConfl uips :: Graph.Node - where - uips = domConfl `intersect` domAssigned :: [Graph.Node] - -- `domConfl' never gives us vacuous dominators since there is by - -- construction a path on the current decision level to the implied, - -- conflicting node. OTOH, there might be no path from dec. var. to - -- the assigned literal which is conflicting (negate conflNode). - domConfl = filter (\i -> levelN i == currentLevel && i /= conflNode) $ - fromJust $ lookup conflNode domFromLastd - domAssigned = - -- if assigned conflict node is not implied by the current-level - -- dec var, then the only dominator we should list of it should - -- be the dec var. - if negate conflNode `elem` DFS.reachable (abs $ unLit lastd) conflGraph - then - filter (\i -> levelN i == currentLevel && i /= conflNode) $ - fromJust $ lookup (negate conflNode) domFromLastd - else [(abs $ unLit lastd)] - domFromLastd = Dom.dom conflGraph (abs $ unLit lastd) - distanceFromConfl x = length $ BFS.esp x conflNode conflGraph - - -- helpers - lastd = head dlits - conflNode = unLit cLit - currentLevel = length dlits - levelL l = levelArr!(var l) - levelN i = if i == unLit cLit then currentLevel else ((levelArr!) . V . abs) i - --- | 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 - - --- | Delete the assignment to last-assigned literal. Undoes the trail, the --- assignment, sets `noLevel', undoes reason. --- --- Does /not/ touch `dl'. -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) } - --- | Increase the recorded activity of given variable. -bump :: Var -> DPLLMonad s () -{-# INLINE bump #-} -bump v = varOrderMod v (+ varInc) - -varInc :: Double -varInc = 1.0 - - - --- *** Impossible to satisfy - --- | /O(1)/. Test for unsatisfiability. --- --- The DPLL paper says, ''A problem is unsatisfiable if there is a conflicting --- clause and there are no decision literals in @m@.'' But we were deciding --- on all literals *without* creating a conflicting clause. So now we also --- test whether we've made all possible decisions, too. -unsat :: Maybe a -> DPLLStateContents s -> Bool -{-# INLINE unsat #-} -unsat maybeConflict (SC{dl=dl}) = isUnsat - where isUnsat = (null dl && isJust maybeConflict) - -- or BitSet.size bad == numVars cnf - - - --- ** Helpers - --- *** Clause compaction - --- | 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 . snd)) clauses - liftST $ forM_ clauses' - (\ wCl@(r, _) -> do - (x, y) <- readSTRef r - modifyArray lArr x $ const (wCl:) - modifyArray lArr y $ const (wCl:)) - --- *** Unit propagation - --- | Add clause to the watcher lists, unless clause is a singleton; if clause --- is a singleton, `enqueue's fact and returns `False' if fact is in conflict, --- `True' otherwise. This function should be called exactly once per clause, --- per run. It should not be called to reconstruct the watcher list when --- propagating. --- --- Currently the watched literals in each clause are the first two. -watchClause :: MAssignment s - -> Clause - -> Bool -- ^ Is this clause learned? - -> DPLLMonad s Bool -{-# INLINE watchClause #-} -watchClause m c isLearnt = do - conf <- gets dpllConfig - case c of - [] -> return True - [l] -> do result <- enqueue m l (Just c) - levelArr <- gets level - liftST $ writeArray levelArr (var l) 0 - return result - _ -> if configUseWatchedLiterals conf then - do let p = (negate (c !! 0), negate (c !! 1)) - insert annCl@(_, cl) list -- avoid watching dup clauses - | any (\(_, c) -> cl == c) list = list - | otherwise = annCl:list - r <- liftST $ newSTRef p - let annCl = (r, c) - addCl arr = do modifyArray arr (fst p) $ const (annCl:) - modifyArray arr (snd p) $ const (annCl:) - get >>= liftST . addCl . (if isLearnt then learnt else watches) - return True - else do modify $ \s -> - let cs = c `Set.insert` (clauses . cnf) s - in s{ cnf = (cnf s){ clauses = cs - , numClauses = Set.size cs } } - return True - --- | Enqueue literal in the `propQ' and place it in the current assignment. --- If this conflicts with an existing assignment, returns @False@; otherwise --- returns @True@. In case there is a conflict, the assignment is /not/ --- altered. --- --- Also records decision level, modifies trail, and records reason for --- assignment. -enqueue :: MAssignment s - -> Lit -- ^ The literal that has been assigned true. - -> Maybe Clause -- ^ The reason for enqueuing the literal. Including - -- a non-@Nothing@ value here adjusts the `reason' - -- map. - -> DPLLMonad s Bool -{-# 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 - --- | 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 - --- | Clear the `propQ'. -clearQueue :: DPLLMonad s () -{-# INLINE clearQueue #-} -clearQueue = modify $ \s -> s{propQ = Seq.empty} - --- *** Dynamic variable ordering - --- | Modify priority of variable; takes care of @Double@ overflow. -varOrderMod :: Var -> (Double -> Double) -> DPLLMonad s () -varOrderMod v f = do - vo <- varOrderArr `liftM` gets varOrder - vActivity <- liftST $ readArray vo v - when (f vActivity > 1e100) $ rescaleActivities vo - liftST $ writeArray vo v (f vActivity) - where - rescaleActivities vo = liftST $ do - indices <- range `liftM` getBounds vo - forM_ indices (\i -> modifyArray vo i $ const (* 1e-100)) - - --- | Retrieve the maximum-priority variable from the variable order. -varOrderGet :: IAssignment -> FrozenVarOrder -> Maybe Var -{-# INLINE varOrderGet #-} -varOrderGet mFr (FrozenVarOrder voFr) = - -- find highest var undef under mFr, then find one with highest activity - (`fmap` goUndef highestIndex) $ \start -> goActivity start start - where - highestIndex = snd . bounds $ voFr - maxActivity v v' = if voFr!v > voFr!v' then v else v' - - -- @goActivity current highest@ returns highest-activity var - goActivity !(V 0) !h = h - goActivity !v@(V n) !h = if v `isUndefUnder` mFr - then goActivity (V $! n-1) (v `maxActivity` h) - else goActivity (V $! n-1) h - - -- returns highest var that is undef under mFr - goUndef !(V 0) = Nothing - goUndef !v@(V n) | v `isUndefUnder` mFr = Just v - | otherwise = goUndef (V $! n-1) - - --- *** Generic state transition notation - --- | 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) -(==>) b amb = guard b >> return amb - -infixr 6 ==> - --- | @flip fmap@. -(>=>) :: (Monad m) => Maybe a -> (a -> m b) -> Maybe (m b) -{-# INLINE (>=>) #-} -(>=>) = flip fmap - -infixr 6 >=> - - --- | Choice of state transitions. Choose the leftmost action that isn't --- @Nothing@, or return @Nothing@ otherwise. -(><) :: (Monad m) => Maybe (m a) -> Maybe (m a) -> Maybe (m a) -a1 >< a2 = - case (a1, a2) of - (Nothing, Nothing) -> Nothing - (Just _, _) -> a1 - _ -> a2 - -infixl 5 >< - --- *** Misc - -showAssignment a = intercalate " " ([show (a!i) | i <- range . bounds $ a, - (a!i) /= 0]) - -initialActivity :: Double -initialActivity = 1.0 - -instance Error (Lit, Clause) where - noMsg = (L 0, []) - -instance Error () where - noMsg = () - - -data Stats = Stats - { statsNumConfl :: Int64 - , statsNumConflTotal :: Int64 - , statsNumLearnt :: Int64 - , statsAvgLearntLen :: Double - , statsNumDecisions :: Int64 - , statsNumImpl :: Int64 } - --- the show instance uses the wrapped string. -newtype NonStupidString = Stupid { stupefy :: String } -instance Show NonStupidString where - show = stupefy - -instance Show Stats where - show = show . statTable - -statTable :: Stats -> Tabular.T NonStupidString -statTable s = - Tabular.mkTable - [ [Stupid "Num. Conflicts" - ,Stupid $ show (statsNumConflTotal s)] - , [Stupid "Num. Learned Clauses" - ,Stupid $ show (statsNumLearnt s)] - , [Stupid " --> Avg. Lits/Clause" - ,Stupid $ show (statsAvgLearntLen s)] - , [Stupid "Num. Decisions" - ,Stupid $ show (statsNumDecisions s)] - , [Stupid "Num. Propagations" - ,Stupid $ show (statsNumImpl s)] ] - -statSummary :: Stats -> String -statSummary s = - show (Tabular.mkTable - [[Stupid $ show (statsNumConflTotal s) ++ " Conflicts" - ,Stupid $ "| " ++ show (statsNumLearnt s) ++ " Learned Clauses" - ++ " (avg " ++ printf "%.2f" (statsAvgLearntLen s) - ++ " lits/clause)"]]) - - -extractStats :: DPLLMonad s Stats -extractStats = do - s <- get - learntArr <- liftST $ unsafeFreezeWatchArray (learnt s) - let learnts = (nub . Fl.concat) - [ map (sort . snd) (learntArr!i) - | i <- (range . bounds) learntArr ] :: [Clause] - stats = - Stats { statsNumConfl = numConfl s - , statsNumConflTotal = numConflTotal s - , statsNumLearnt = fromIntegral $ length learnts - , statsAvgLearntLen = - fromIntegral (foldl' (+) 0 (map length learnts)) - / fromIntegral (statsNumLearnt stats) - , statsNumDecisions = numDecisions s - , statsNumImpl = numImpl s } - return stats - -unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s]) -unsafeFreezeWatchArray = freeze - --- | The assignment as a list of signed literals. -litAssignment :: IAssignment -> [Lit] -litAssignment mFr = map (L . (mFr!)) (range . bounds $ mFr) - ----------- TESTING ---------- - - --- | Verify the assigment is well-formed and satisfies the CNF problem. This --- function is run after a solution is discovered, just to be safe. --- --- Makes sure each slot in the assignment is either 0 or contains its --- (possibly negated) corresponding literal, and verifies that each clause is --- made true by the assignment. -verify :: IAssignment -> CNF -> Maybe [(Clause, Either () Bool)] -verify m cnf = - -- m is well-formed --- Fl.all (\l -> m!(V l) == l || m!(V l) == negate l || m!(V l) == 0) [1..numVars cnf] - let unsatClauses = toList $ - Set.filter (not . isTrue . snd) $ - Set.map (\c -> (c, c `statusUnder` m)) (clauses cnf) - in if null unsatClauses - then Nothing - else Just unsatClauses - where isTrue (Right True) = True - isTrue _ = False +Funsat aims to be a reasonably efficient modern SAT solver that is easy to +integrate as a backend to other projects. SAT is NP-complete, and thus has +reductions from many other interesting problems. We hope this implementation +is efficient enough to make it useful to solve medium-size, real-world problem +mapped from another space. We also aim to test the solver rigorously to +encourage confidence in its output. + +One particular nicetie facilitating integration of Funsat into other projects +is the efficient calculation of an /unsatisfiable core/ for unsatisfiable +problems (see the "Funsat.Resolution" module). In the case a problem is +unsatisfiable, as a by-product of checking the proof of unsatisfiability, +Funsat will generate a minimal set of input clauses that are also +unsatisfiable. + +* 07 Jun 2008 21:43:42: N.B. because of the use of mutable arrays in the ST +monad, the solver will actually give _wrong_ answers if you compile without +optimisation. Which is okay, 'cause that's really slow anyway. + +[@Bibliography@] + + * ''Abstract DPLL and DPLL Modulo Theories'' + + * ''Chaff: Engineering an Efficient SAT solver'' + + * ''An Extensible SAT-solver'' by Niklas Een, Niklas Sorensson + + * ''Efficient Conflict Driven Learning in a Boolean Satisfiability Solver'' +by Zhang, Madigan, Moskewicz, Malik + + * ''SAT-MICRO: petit mais costaud!'' by Conchon, Kanig, and Lescuyer + +-} +module Funsat.Solver +#ifndef TESTING + ( -- * Interface + solve + , solve1 + , Solution(..) + -- ** Verification + , verify + , VerifyError(..) + -- ** Configuration + , DPLLConfig(..) + , defaultConfig + -- * Solver statistics + , Stats(..) + , ShowWrapped(..) + , statTable + , statSummary + ) +#endif + where + +{- + This file is part of funsat. + + 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. + + 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 funsat. If not, see . + + Copyright 2008 Denis Bueno +-} + + +import Control.Arrow ((&&&)) +import Control.Exception (assert) +import Control.Monad.Error hiding ((>=>), forM_, runErrorT) +import Control.Monad.MonadST( MonadST(..) ) +import Control.Monad.ST.Strict +import Control.Monad.State.Lazy hiding ((>=>), forM_) +import Data.Array.ST +import Data.Array.Unboxed +import Data.Foldable hiding (sequence_) +import Data.Graph.Inductive.Graph( DynGraph, Graph ) +-- import Data.Graph.Inductive.Graphviz +import Data.Int (Int64) +import Data.List (intercalate, nub, tails, sortBy, intersect, sort) +import Data.Map (Map) +import Data.Maybe +import Data.Ord (comparing) +import Data.STRef +import Data.Sequence (Seq) +import Data.Set (Set) +import Debug.Trace (trace) +import Funsat.Monad +import Funsat.Utils +import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace ) +import Funsat.Types +import Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum) +import Funsat.Resolution( ResolutionError(..) ) +import Text.Printf( printf ) +import qualified Data.Graph.Inductive.Graph as Graph +import qualified Data.Graph.Inductive.Query.DFS as DFS +import qualified Data.Foldable as Fl +import qualified Data.List as List +import qualified Data.Map as Map +import qualified Data.Sequence as Seq +import qualified Data.Set as Set +import qualified Funsat.Resolution as Resolution +import qualified Text.Tabular as Tabular + +-- * Interface + +-- | 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. +solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace) +solve cfg fIn = + -- To solve, we simply take baby steps toward the solution using solveStep, + -- starting with an initial assignment. +-- trace ("input " ++ show f) $ + either (error "no solution") id $ + runST $ + evalSSTErrMonad + (do sol <- stepToSolution $ do + initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0 + (a, isUnsat) <- initialState initialAssignment + if isUnsat then return (Right (Unsat a)) + else solveStep initialAssignment + stats <- extractStats + case sol of + Sat _ -> return (sol, stats, Nothing) + Unsat _ -> do resTrace <- constructResTrace sol + return (sol, stats, Just resTrace)) + SC{ cnf=f{clauses = Set.empty}, dl=[] + , watches=undefined, learnt=undefined, propQ=Seq.empty + , trail=[], numConfl=0, level=undefined, numConflTotal=0 + , numDecisions=0, numImpl=0 + , reason=Map.empty, varOrder=undefined + , resolutionTrace=PartialResolutionTrace 1 [] [] Map.empty + , dpllConfig=cfg } + where + f = preprocessCNF fIn + -- 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} + initialWatches <- liftST $ newSTArray (L (- (numVars f)), L (numVars f)) [] + modify $ \s -> s{ watches = initialWatches } + initialLearnts <- liftST $ newSTArray (L (- (numVars f)), L (numVars f)) [] + modify $ \s -> s{ learnt = initialLearnts } + initialVarOrder <- liftST $ newSTUArray (V 1, V (numVars f)) initialActivity + modify $ \s -> s{ varOrder = VarOrder initialVarOrder } + + (`catchError` (const $ liftST (unsafeFreezeAss m) >>= \a -> return (a,True))) $ do + forM_ (clauses f) + (\c -> do cid <- nextTraceId + isConsistent <- watchClause m (c, cid) False + when (not isConsistent) + -- 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 + +-- | Configuration parameters for the solver. +data DPLLConfig = Cfg + { configRestart :: !Int64 -- ^ Number of conflicts before a restart. + , configRestartBump :: !Double -- ^ `configRestart' is altered after each + -- restart by multiplying it by this value. + , configUseVSIDS :: !Bool -- ^ If true, use dynamic variable ordering. + , configUseRestarts :: !Bool } + deriving Show + +-- | A default configuration based on the formula to solve. +-- +-- * restarts every 100 conflicts +-- +-- * requires 1.5 as many restarts after restarting as before, each time +-- +-- * VSIDS to be enabled +-- +-- * restarts to be enabled +defaultConfig :: CNF -> DPLLConfig +defaultConfig _f = Cfg { configRestart = 100 -- fromIntegral $ max (numVars f `div` 10) 100 + , configRestartBump = 1.5 + , configUseVSIDS = True + , configUseRestarts = True } + +-- * Preprocessing + +-- | Some kind of preprocessing. +-- +-- * remove duplicates +preprocessCNF :: CNF -> CNF +preprocessCNF f = f{clauses = simpClauses (clauses f)} + where simpClauses = Set.map nub -- rm dups + +-- | Simplify the clause database. Eventually should supersede, probably, +-- `preprocessCNF'. +-- +-- Precondition: decision level 0. +simplifyDB :: IAssignment -> DPLLMonad s () +simplifyDB mFr = do + -- For each clause in the database, remove it if satisfied; if it contains a + -- literal whose negation is assigned, delete that literal. + n <- numVars `liftM` gets cnf + s <- get + liftST . forM_ [V 1 .. V n] $ \i -> when (mFr!i /= 0) $ do + let l = L (mFr!i) + filterL _i = map (\(p, c, cid) -> (p, filter (/= negate l) c, cid)) + -- Remove unsat literal `negate l' from clauses. +-- modifyArray (watches s) l filterL + modifyArray (learnt s) l filterL + -- Clauses containing `l' are Sat. +-- writeArray (watches s) (negate l) [] + writeArray (learnt s) (negate l) [] + +-- * Internals + +-- | The DPLL procedure is modeled as a state transition system. This +-- 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 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 $ + -- Check if unsat. + unsat maybeConfl s ==> postProcessUnsat maybeConfl + -- Unit propagation may reveal conflicts; check. + >< maybeConfl >=> backJump m + -- No conflicts. Decide. + >< 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) + +-- | /Precondition:/ problem determined to be unsat. +-- +-- Records id of conflicting clause in trace. +postProcessUnsat :: Maybe (Lit, Clause, ClauseId) -> DPLLMonad s (Maybe a) +postProcessUnsat maybeConfl = do + traceClauseId $ (thd . fromJust) maybeConfl + return Nothing + where + thd (_,_,i) = i + +-- | Check data structure invariants. Unless @-fno-ignore-asserts@ is passed, +-- this should be optimised away to nothing. +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 () + + +-- | 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. +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 + +-- | 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 + +-- | 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 + { cnf :: CNF -- ^ The problem. + , dl :: [Lit] + -- ^ The decision level (last decided literal on front). + + , watches :: WatchArray s + -- ^ Invariant: if @l@ maps to @((x, y), c)@, then @x == l || y == l@. + + , learnt :: WatchArray s + -- ^ Same invariant as `watches', but only contains learned conflict + -- clauses. + + , propQ :: Seq Lit + -- ^ A FIFO queue of literals to propagate. This should not be + -- manipulated directly; see `enqueue' and `dequeue'. + + , level :: LevelArray s + + , trail :: [Lit] + -- ^ Chronological trail of assignments, last-assignment-at-head. + + , reason :: ReasonMap + -- ^ For each variable, the clause that (was unit and) implied its value. + + , numConfl :: !Int64 + -- ^ The number of conflicts that have occurred since the last restart. + + , numConflTotal :: !Int64 + -- ^ The total number of conflicts. + + , numDecisions :: !Int64 + -- ^ The total number of decisions. + + , numImpl :: !Int64 + -- ^ The total number of implications (propagations). + + , varOrder :: VarOrder s + + , 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 "" + +-- | 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 +-- `FunsatState' and is not mutable. +type DPLLMonad s = SSTErrMonad (Lit, Clause, ClauseId) (FunsatState s) s + + +-- *** Boolean constraint propagation + +-- | Assign a new literal, and enqueue any implied assignments. If a conflict +-- is detected, return @Just (impliedLit, conflictingClause)@; otherwise +-- return @Nothing@. The @impliedLit@ is implied by the clause, but conflicts +-- with the assignment. +-- +-- If no new clauses are unit (i.e. no implied assignments), simply update +-- watched literals. +bcpLit :: MAssignment s + -> Lit -- ^ Assigned literal which might propagate. + -> DPLLMonad s (Maybe (Lit, Clause, ClauseId)) +bcpLit m l = do + ws <- gets watches ; ls <- gets learnt + clauses <- liftST $ readArray ws l + learnts <- liftST $ readArray ls l + liftST $ do writeArray ws l [] ; writeArray ls l [] + + -- Update wather lists for normal & learnt clauses; if conflict is found, + -- return that and don't update anything else. + (`catchError` return . Just) $ do + {-# SCC "bcpWatches" #-} forM_ (tails clauses) (updateWatches + (\ f l -> liftST $ modifyArray ws l (const f))) + {-# SCC "bcpLearnts" #-} forM_ (tails learnts) (updateWatches + (\ f l -> liftST $ modifyArray ls l (const f))) + return Nothing -- no conflict + where + -- updateWatches: `l' has been assigned, so we look at the clauses in + -- which contain @negate l@, namely the watcher list for l. For each + -- annotated clause, find the status of its watched literals. If a + -- conflict is found, the at-fault clause is returned through Left, and + -- the unprocessed clauses are placed back into the appropriate watcher + -- list. + {-# INLINE updateWatches #-} + updateWatches _ [] = return () + updateWatches alter (annCl@(watchRef, c, cid) : restClauses) = do + mFr <- unsafeFreezeAss m + q <- liftST $ do (x, y) <- readSTRef watchRef + return $ if x == l then y else x + -- l,q are the (negated) literals being watched for clause c. + if negate q `isTrueUnder` mFr -- if other true, clause already sat + then alter (annCl:) l + else + case find (\x -> x /= negate q && x /= negate l + && not (x `isFalseUnder` mFr)) c of + Just l' -> do -- found unassigned literal, negate l', to watch + liftST $ writeSTRef watchRef (q, negate l') + alter (annCl:) (negate l') + + Nothing -> do -- all other lits false, clause is unit + modify $ \s -> s{ numImpl = numImpl s + 1 } + alter (annCl:) l + isConsistent <- enqueue m (negate q) (Just (c, cid)) + when (not isConsistent) $ do -- unit literal is conflicting + alter (restClauses ++) l + clearQueue + throwError (negate q, c, cid) + +-- | Boolean constraint propagation of all literals in `propQ'. If a conflict +-- is found it is returned exactly as described for `bcpLit'. +bcp :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause, ClauseId)) +bcp m = do + q <- gets propQ + if Seq.null q then return Nothing + else do + p <- dequeue + bcpLit m p >>= maybe (bcp m) (return . Just) + + + +-- *** Decisions + +-- | Find and return a decision variable. A /decision variable/ must be (1) +-- undefined under the assignment and (2) it or its negation occur in the +-- formula. +-- +-- Select a decision variable, if possible, and return it and the adjusted +-- `VarOrder'. +select :: IAssignment -> FrozenVarOrder -> Maybe Var +{-# INLINE select #-} +select = varOrderGet + +selectStatic :: IAssignment -> a -> Maybe Var +{-# INLINE selectStatic #-} +selectStatic m _ = find (`isUndefUnder` m) (range . bounds $ m) + +-- | Assign given decision variable. Records the current assignment before +-- deciding on the decision variable indexing the assignment. +decide :: MAssignment s -> Var -> DPLLMonad s (Maybe (MAssignment s)) +decide m v = do + let ld = L (unVar v) + (SC{dl=dl}) <- get +-- trace ("decide " ++ show ld) $ return () + modify $ \s -> s{ dl = ld:dl + , numDecisions = numDecisions s + 1 } + enqueue m ld Nothing + return $ Just m + + + +-- *** Backtracking + +-- | Non-chronological backtracking. The current returns the learned clause +-- implied by the first unique implication point cut of the conflict graph. +backJump :: MAssignment s + -> (Lit, Clause, ClauseId) + -- ^ @(l, c)@, where attempting to assign @l@ conflicted with + -- clause @c@. + -> DPLLMonad s (Maybe (MAssignment s)) +backJump m c@(_, _conflict, _) = get >>= \(SC{dl=dl, reason=_reason}) -> do + _theTrail <- gets trail +-- trace ("********** conflict = " ++ show c) $ return () +-- trace ("trail = " ++ show _theTrail) $ return () +-- trace ("dlits (" ++ show (length dl) ++ ") = " ++ show dl) $ return () +-- ++ "reason: " ++ Map.showTree _reason +-- ) ( + modify $ \s -> s{ numConfl = numConfl s + 1 + , numConflTotal = numConflTotal s + 1 } + levelArr :: FrozenLevelArray <- do s <- get + liftST $ unsafeFreeze (level s) + (learntCl, learntClId, newLevel) <- + do mFr <- unsafeFreezeAss m + analyse mFr levelArr dl c + s <- get + let numDecisionsToUndo = length dl - newLevel + dl' = drop numDecisionsToUndo dl + undoneLits = takeWhile (\lit -> levelArr ! (var lit) > newLevel) (trail s) + forM_ undoneLits $ const (undoOne m) -- backtrack + mFr <- unsafeFreezeAss m + assert (numDecisionsToUndo > 0) $ + assert (not (null learntCl)) $ + assert (learntCl `isUnitUnder` mFr) $ + modify $ \s -> s{ dl = dl' } -- undo decisions + mFr <- unsafeFreezeAss m +-- trace ("new mFr: " ++ showAssignment mFr) $ return () + -- TODO once I'm sure this works I don't need getUnit, I can just use the + -- uip of the cut. + watchClause m (learntCl, learntClId) True + enqueue m (getUnit learntCl mFr) (Just (learntCl, learntClId)) + -- learntCl is asserting + return $ Just m + + + +-- | @doWhile cmd test@ first runs @cmd@, then loops testing @test@ and +-- executing @cmd@. The traditional @do-while@ semantics, in other words. +doWhile :: (Monad m) => m () -> m Bool -> m () +doWhile body test = do + body + shouldContinue <- test + when shouldContinue $ doWhile body test + +-- | Analyse a the conflict graph and produce a learned clause. We use the +-- First UIP cut of the conflict graph. +-- +-- May undo part of the trail, but not past the current decision level. +analyse :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause, ClauseId) + -> DPLLMonad s (Clause, ClauseId, Int) + -- ^ learned clause and new decision level +analyse mFr levelArr dlits (cLit, cClause, cCid) = do + st <- get +-- trace ("mFr: " ++ showAssignment mFr) $ assert True (return ()) +-- let (learntCl, newLevel) = cutLearn mFr levelArr firstUIPCut +-- firstUIPCut = uipCut dlits levelArr conflGraph (unLit cLit) +-- (firstUIP conflGraph) +-- conflGraph = mkConflGraph mFr levelArr (reason st) dlits c +-- :: Gr CGNodeAnnot () +-- trace ("graphviz graph:\n" ++ graphviz' conflGraph) $ return () +-- trace ("cut: " ++ show firstUIPCut) $ return () +-- trace ("topSort: " ++ show topSortNodes) $ return () +-- trace ("dlits (" ++ show (length dlits) ++ "): " ++ show dlits) $ return () +-- trace ("learnt: " ++ show (map (\l -> (l, levelArr!(var l))) learntCl, newLevel)) $ return () +-- outputConflict "conflict.dot" (graphviz' conflGraph) $ return () +-- return $ (learntCl, newLevel) + m <- liftST $ unsafeThawAss mFr + a <- firstUIPBFS m (numVars . cnf $ st) (reason st) +-- trace ("firstUIPBFS learned: " ++ show a) $ return () + return a + where + -- BFS by undoing the trail backward. From Minisat paper. Returns + -- conflict clause and backtrack level. + firstUIPBFS :: MAssignment s -> Int -> ReasonMap + -> DPLLMonad s (Clause, ClauseId, Int) + firstUIPBFS m nVars reasonMap = do + resolveSourcesR <- liftST $ newSTRef [] -- trace sources + let addResolveSource clauseId = + liftST $ modifySTRef resolveSourcesR (clauseId:) + -- Literals we should process. + seenArr <- liftST $ newSTUArray (V 1, V nVars) False + counterR <- liftST $ newSTRef 0 -- Number of unprocessed current-level + -- lits we know about. + pR <- liftST $ newSTRef cLit -- Invariant: literal from current dec. lev. + out_learnedR <- liftST $ newSTRef [] + out_btlevelR <- liftST $ newSTRef 0 + let reasonL l = if l == cLit then (cClause, cCid) + else + let (r, rid) = + Map.findWithDefault (error "analyse: reasonL") + (var l) reasonMap + in (r `without` l, rid) + + + (`doWhile` (liftM (> 0) (liftST $ readSTRef counterR))) $ + do p <- liftST $ readSTRef pR + let (p_reason, p_rid) = reasonL p + traceClauseId p_rid + addResolveSource p_rid + forM_ p_reason (bump . var) + -- For each unseen reason, + -- > from the current level, bump counter + -- > from lower level, put in learned clause + liftST . forM_ p_reason $ \q -> do + seenq <- readArray seenArr (var q) + when (not seenq) $ + do writeArray seenArr (var q) True + if levelL q == currentLevel + then modifySTRef counterR (+ 1) + else if levelL q > 0 + then do modifySTRef out_learnedR (q:) + modifySTRef out_btlevelR $ max (levelL q) + else return () + -- Select next literal to look at: + (`doWhile` (liftST (readSTRef pR >>= readArray seenArr . var) + >>= return . not)) $ do + p <- head `liftM` gets trail -- a dec. var. only if the counter = + -- 1, i.e., loop terminates now + liftST $ writeSTRef pR p + undoOne m + -- Invariant states p is from current level, so when we're done + -- with it, we've thrown away one lit. from counting toward + -- counter. + liftST $ modifySTRef counterR (\c -> c - 1) + p <- liftST $ readSTRef pR + liftST $ modifySTRef out_learnedR (negate p:) + bump . var $ p + out_learned <- liftST $ readSTRef out_learnedR + out_btlevel <- liftST $ readSTRef out_btlevelR + learnedClauseId <- nextTraceId + storeResolvedSources resolveSourcesR learnedClauseId + traceClauseId learnedClauseId + return (out_learned, learnedClauseId, out_btlevel) + + -- helpers + currentLevel = length dlits + levelL l = levelArr!(var l) + storeResolvedSources rsR clauseId = do + rsReversed <- liftST $ readSTRef rsR + modifySlot resolutionTrace $ \s rt -> + s{resolutionTrace = + rt{resSourceMap = + Map.insert clauseId (reverse rsReversed) (resSourceMap rt)}} + + +-- | Delete the assignment to last-assigned literal. Undoes the trail, the +-- assignment, sets `noLevel', undoes reason. +-- +-- Does /not/ touch `dl'. +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) } + +-- | Increase the recorded activity of given variable. +bump :: Var -> DPLLMonad s () +{-# INLINE bump #-} +bump v = varOrderMod v (+ varInc) + +-- | Constant amount by which a variable is `bump'ed. +varInc :: Double +varInc = 1.0 + + + +-- *** Impossible to satisfy + +-- | /O(1)/. Test for unsatisfiability. +-- +-- The DPLL paper says, ''A problem is unsatisfiable if there is a conflicting +-- clause and there are no decision literals in @m@.'' But we were deciding +-- on all literals *without* creating a conflicting clause. So now we also +-- test whether we've made all possible decisions, too. +unsat :: Maybe a -> FunsatState s -> Bool +{-# INLINE unsat #-} +unsat maybeConflict (SC{dl=dl}) = isUnsat + where isUnsat = (null dl && isJust maybeConflict) + -- or BitSet.size bad == numVars cnf + + + +-- ** Helpers + +-- *** Clause compaction + +-- | 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:)) + +-- *** Unit propagation + +-- | Add clause to the watcher lists, unless clause is a singleton; if clause +-- is a singleton, `enqueue's fact and returns `False' if fact is in conflict, +-- `True' otherwise. This function should be called exactly once per clause, +-- per run. It should not be called to reconstruct the watcher list when +-- propagating. +-- +-- Currently the watched literals in each clause are the first two. +-- +-- Also adds unique clause ids to trace. +watchClause :: MAssignment s + -> (Clause, ClauseId) + -> Bool -- ^ Is this clause learned? + -> 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 + +-- | Enqueue literal in the `propQ' and place it in the current assignment. +-- If this conflicts with an existing assignment, returns @False@; otherwise +-- returns @True@. In case there is a conflict, the assignment is /not/ +-- altered. +-- +-- Also records decision level, modifies trail, and records reason for +-- assignment. +enqueue :: MAssignment s + -> Lit + -- ^ The literal that has been assigned true. + -> Maybe (Clause, ClauseId) + -- ^ The reason for enqueuing the literal. Including a + -- non-@Nothing@ value here adjusts the `reason' map. + -> DPLLMonad s Bool +{-# 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 + +-- | 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 + +-- | Clear the `propQ'. +clearQueue :: DPLLMonad s () +{-# INLINE clearQueue #-} +clearQueue = modify $ \s -> s{propQ = Seq.empty} + +-- *** Dynamic variable ordering + +-- | Modify priority of variable; takes care of @Double@ overflow. +varOrderMod :: Var -> (Double -> Double) -> DPLLMonad s () +varOrderMod v f = do + vo <- varOrderArr `liftM` gets varOrder + vActivity <- liftST $ readArray vo v + when (f vActivity > 1e100) $ rescaleActivities vo + liftST $ writeArray vo v (f vActivity) + where + rescaleActivities vo = liftST $ do + indices <- range `liftM` getBounds vo + forM_ indices (\i -> modifyArray vo i $ const (* 1e-100)) + + +-- | Retrieve the maximum-priority variable from the variable order. +varOrderGet :: IAssignment -> FrozenVarOrder -> Maybe Var +{-# INLINE varOrderGet #-} +varOrderGet mFr (FrozenVarOrder voFr) = + -- find highest var undef under mFr, then find one with highest activity + (`fmap` goUndef highestIndex) $ \start -> goActivity start start + where + highestIndex = snd . bounds $ voFr + maxActivity v v' = if voFr!v > voFr!v' then v else v' + + -- @goActivity current highest@ returns highest-activity var + goActivity !(V 0) !h = h + goActivity !v@(V n) !h = if v `isUndefUnder` mFr + then goActivity (V $! n-1) (v `maxActivity` h) + else goActivity (V $! n-1) h + + -- returns highest var that is undef under mFr + goUndef !(V 0) = Nothing + goUndef !v@(V n) | v `isUndefUnder` mFr = Just v + | otherwise = goUndef (V $! n-1) + + +-- | Generate a new clause identifier (always unique). +nextTraceId :: DPLLMonad s Int +nextTraceId = do + counter <- gets (resTraceIdCount . resolutionTrace) + modifySlot resolutionTrace $ \s rt -> + s{ resolutionTrace = rt{ resTraceIdCount = succ counter }} + return $! counter + +-- | Add the given clause id to the trace. +traceClauseId :: ClauseId -> DPLLMonad s () +traceClauseId cid = do + modifySlot resolutionTrace $ \s rt -> + s{resolutionTrace = rt{ resTrace = [cid] }} + + +-- *** Generic state transition notation + +-- | 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) +(==>) b amb = guard b >> return amb + +infixr 6 ==> + +-- | @flip fmap@. +(>=>) :: (Monad m) => Maybe a -> (a -> m b) -> Maybe (m b) +{-# INLINE (>=>) #-} +(>=>) = flip fmap + +infixr 6 >=> + + +-- | Choice of state transitions. Choose the leftmost action that isn't +-- @Nothing@, or return @Nothing@ otherwise. +(><) :: (Monad m) => Maybe (m a) -> Maybe (m a) -> Maybe (m a) +a1 >< a2 = + case (a1, a2) of + (Nothing, Nothing) -> Nothing + (Just _, _) -> a1 + _ -> a2 + +infixl 5 >< + +-- *** 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 = () + + +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. + + deriving (Show) + +-- | Verify the solution. In case of `Sat', checks that the assignment is +-- well-formed and satisfies the CNF problem. In case of `Unsat', runs a +-- resolution-based checker on a trace of the SAT solver. +verify :: Solution -> Maybe ResolutionTrace -> CNF -> Maybe VerifyError +verify sol maybeRT cnf = + -- m is well-formed +-- Fl.all (\l -> m!(V l) == l || m!(V l) == negate l || m!(V l) == 0) [1..numVars cnf] + case sol of + Sat m -> + let unsatClauses = toList $ + Set.filter (not . isTrue . snd) $ + Set.map (\c -> (c, c `statusUnder` m)) (clauses cnf) + in if null unsatClauses + then Nothing + else Just . SatError $ unsatClauses + Unsat m -> + case Resolution.checkDepthFirst (fromJust maybeRT) of + Left er -> Just . UnsatError $ er + Right _ -> Nothing + where isTrue (Right True) = True + isTrue _ = False + +--------------------------------------- +-- Statistics & trace + + +data Stats = Stats + { statsNumConfl :: Int64 + -- ^ Number of conflicts since last restart. + + , statsNumConflTotal :: Int64 + -- ^ Number of conflicts since beginning of solving. + + , statsNumLearnt :: Int64 + -- ^ Number of learned clauses currently in DB (fluctuates because DB is + -- compacted every restart). + + , statsAvgLearntLen :: Double + -- ^ Avg. number of literals per learnt clause. + + , statsNumDecisions :: Int64 + -- ^ Total number of decisions since beginning of solving. + + , statsNumImpl :: Int64 + -- ^ Total number of unit implications since beginning of solving. + } + +-- | The show instance uses the wrapped string. +newtype ShowWrapped = WrapString { unwrapString :: String } +instance Show ShowWrapped where + show = unwrapString + +instance Show Stats where + show = show . statTable + +-- | Convert statistics to a nice-to-display tabular form. +statTable :: Stats -> Tabular.Table ShowWrapped +statTable s = + Tabular.mkTable + [ [WrapString "Num. Conflicts" + ,WrapString $ show (statsNumConflTotal s)] + , [WrapString "Num. Learned Clauses" + ,WrapString $ show (statsNumLearnt s)] + , [WrapString " --> Avg. Lits/Clause" + ,WrapString $ show (statsAvgLearntLen s)] + , [WrapString "Num. Decisions" + ,WrapString $ show (statsNumDecisions s)] + , [WrapString "Num. Propagations" + ,WrapString $ show (statsNumImpl s)] ] + +-- | Converts statistics into a tabular, human-readable summary. +statSummary :: Stats -> String +statSummary s = + show (Tabular.mkTable + [[WrapString $ show (statsNumConflTotal s) ++ " Conflicts" + ,WrapString $ "| " ++ show (statsNumLearnt s) ++ " Learned Clauses" + ++ " (avg " ++ printf "%.2f" (statsAvgLearntLen s) + ++ " lits/clause)"]]) + + +extractStats :: DPLLMonad s Stats +extractStats = do + s <- get + learntArr <- liftST $ unsafeFreezeWatchArray (learnt s) + let learnts = (nub . Fl.concat) + [ map (sort . (\(_,c,_) -> c)) (learntArr!i) + | i <- (range . bounds) learntArr ] :: [Clause] + stats = + Stats { statsNumConfl = numConfl s + , statsNumConflTotal = numConflTotal s + , statsNumLearnt = fromIntegral $ length learnts + , statsAvgLearntLen = + fromIntegral (foldl' (+) 0 (map length learnts)) + / fromIntegral (statsNumLearnt stats) + , statsNumDecisions = numDecisions s + , statsNumImpl = numImpl s } + return stats + +unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s]) +unsafeFreezeWatchArray = freeze + + +constructResTrace :: Solution -> DPLLMonad s ResolutionTrace +constructResTrace sol = do + s <- get + watchesIndices <- range `liftM` liftST (getBounds (watches s)) + origClauseMap <- + foldM (\origMap i -> do + clauses <- liftST $ readArray (watches s) i + return $ + foldr (\(_, clause, clauseId) origMap -> + Map.insert clauseId clause origMap) + origMap + clauses) + Map.empty + watchesIndices + let singleClauseMap = + foldr (\(clause, clauseId) m -> Map.insert clauseId clause m) + Map.empty + (resTraceOriginalSingles . resolutionTrace $ s) + anteMap = + foldr (\l anteMap -> Map.insert (var l) (getAnteId s (var l)) anteMap) + Map.empty + (litAssignment . finalAssignment $ sol) + return + (initResolutionTrace + (head (resTrace . resolutionTrace $ s)) + (finalAssignment sol)) + { traceSources = resSourceMap . resolutionTrace $ s + , traceOriginalClauses = origClauseMap `Map.union` singleClauseMap + , traceAntecedents = anteMap } + where + getAnteId s v = snd $ + Map.findWithDefault (error $ "no reason for assigned var " ++ show v) + v (reason s) diff --git a/Funsat/Types.hs b/Funsat/Types.hs new file mode 100644 --- /dev/null +++ b/Funsat/Types.hs @@ -0,0 +1,300 @@ +{-# LANGUAGE PatternSignatures + ,MultiParamTypeClasses + ,FunctionalDependencies + ,FlexibleInstances + ,FlexibleContexts + ,GeneralizedNewtypeDeriving + ,TypeSynonymInstances + ,TypeOperators + ,ParallelListComp + ,BangPatterns + #-} + +{- + This file is part of funsat. + + 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. + + 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 funsat. If not, see . + + Copyright 2008 Denis Bueno +-} + + + +-- | Data types used when dealing with SAT problems in funsat. +module Funsat.Types where + + +import Control.Monad.MonadST( MonadST(..) ) +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 Funsat.Monad +import Funsat.Utils +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.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) + +instance Show Var where + show (V i) = show i ++ "v" + +instance Num Var where + _ + _ = error "+ doesn't make sense for variables" + _ - _ = error "- doesn't make sense for variables" + _ * _ = error "* doesn't make sense for variables" + signum _ = error "signum doesn't make sense for variables" + negate = error "negate doesn't make sense for variables" + abs = id + fromInteger l | l <= 0 = error $ show l ++ " is not a variable" + | otherwise = V $ fromInteger l + +newtype Lit = L {unLit :: Int} deriving (Eq, Ord, Enum, Ix) +inLit f = L . f . unLit + +-- | 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" + _ * _ = error "* doesn't make sense for literals" + signum _ = error "signum doesn't make sense for literals" + negate = inLit negate + abs = inLit abs + fromInteger l | l == 0 = error "0 is not a literal" + | otherwise = L $ fromInteger l + +type Clause = [Lit] + +-- | ''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) + +type CNF = GenCNF Clause + +instance Foldable GenCNF where + -- TODO it might be easy to make this instance more efficient. + foldMap toM cnf = foldMap toM (clauses cnf) + + +-- | Represents a container of type @t@ storing elements of type @a@ that +-- support membership, insertion, and deletion. +-- +-- There are various data structures used in funsat which are essentially used +-- as ''set-like'' objects. I've distilled their interface into three +-- methods. These methods are used extensively in the implementation of the +-- solver. +class Ord a => Setlike t a where + -- | The set-like object with an element removed. + without :: t -> a -> t + -- | The set-like object with an element included. + with :: t -> a -> t + -- | Whether the set-like object contains a certain element. + contains :: t -> a -> Bool + +instance Ord a => Setlike (Set a) a where + without = flip Set.delete + with = flip Set.insert + contains = flip Set.member + +instance Ord a => Setlike [a] a where + without = flip List.delete + with = flip (:) + contains = flip List.elem + +instance Setlike IAssignment Lit where + without a l = a // [(var l, 0)] + with a l = a // [(var l, unLit l)] + contains a l = unLit l == a ! (var l) + +instance (Ord k, Ord a) => Setlike (Map k a) (k, a) where + with m (k,v) = Map.insert k v m + without m (k,_) = Map.delete k m + contains = error "no contains for Setlike (Map k a) (k, a)" + +instance (Ord a, BitSet.Hash a) => Setlike (BitSet a) a where + with = flip BitSet.insert + without = flip BitSet.delete + contains = flip BitSet.member + + +instance (BitSet.Hash Lit) where + hash l = if li > 0 then 2 * vi else (2 * vi) + 1 + where li = unLit l + vi = abs li + +instance (BitSet.Hash Var) where + hash = unVar + +-- * Assignments + + +-- | An ''immutable assignment''. Stores the current assignment according to +-- the following convention. A literal @L i@ is in the assignment if in +-- location @(abs i)@ in the array, @i@ is present. Literal @L i@ is absent +-- if in location @(abs i)@ there is 0. It is an error if the location @(abs +-- i)@ is any value other than @0@ or @i@ or @negate i@. +-- +-- Note that the `Model' instance for `Lit' and `IAssignment' takes constant +-- time to execute because of this representation for assignments. Also +-- updating an assignment with newly-assigned literals takes constant time, +-- and can be done destructively, but safely. +type IAssignment = UArray Var Int + +-- | Mutable array corresponding to the `IAssignment' representation. +type MAssignment s = STUArray s Var Int + +-- | Same as @freeze@, but at the right type so GHC doesn't yell at me. +freezeAss :: MAssignment s -> ST s IAssignment +{-# INLINE freezeAss #-} +freezeAss = freeze +-- | See `freezeAss'. +unsafeFreezeAss :: (MonadST s m) => MAssignment s -> m IAssignment +{-# INLINE unsafeFreezeAss #-} +unsafeFreezeAss = liftST . unsafeFreeze + +thawAss :: IAssignment -> ST s (MAssignment s) +{-# INLINE thawAss #-} +thawAss = thaw +unsafeThawAss :: IAssignment -> ST s (MAssignment s) +{-# INLINE unsafeThawAss #-} +unsafeThawAss = unsafeThaw + +-- | Destructively update the assignment with the given literal. +assign :: MAssignment s -> Lit -> ST s (MAssignment s) +assign a l = writeArray a (var l) (unLit l) >> return a + +-- | Destructively undo the assignment to the given literal. +unassign :: MAssignment s -> Lit -> ST s (MAssignment s) +unassign a l = writeArray a (var l) 0 >> return a + +-- | The assignment as a list of signed literals. +litAssignment :: IAssignment -> [Lit] +litAssignment mFr = foldr (\i ass -> if mFr!i == 0 then ass + else (L . (mFr!) $ i) : ass) + [] + (range . bounds $ mFr) + +-- * Model + + +-- | An instance of this class is able to answer the question, Is a +-- truth-functional object @x@ true under the model @m@? Or is @m@ a model +-- for @x@? There are three possible answers for this question: `True' (''the +-- object is true under @m@''), `False' (''the object is false under @m@''), +-- and undefined, meaning its status is uncertain or unknown (as is the case +-- with a partial assignment). +-- +-- The only method in this class is so named so it reads well when used infix. +-- Also see: `isTrueUnder', `isFalseUnder', `isUndefUnder'. +class Model a m where + -- | @x ``statusUnder`` m@ should use @Right@ if the status of @x@ is + -- defined, and @Left@ otherwise. + statusUnder :: a -> m -> Either () Bool + +-- /O(1)/. +instance Model Lit IAssignment where + statusUnder l a | a `contains` l = Right True + | a `contains` negate l = Right False + | otherwise = Left () +instance Model Var IAssignment where + statusUnder v a | a `contains` pos = Right True + | a `contains` neg = Right False + | otherwise = Left () + where pos = L (unVar v) + neg = negate pos +instance Model Clause IAssignment where + statusUnder c m + -- true if c intersect m is not null == a member of c in m + | Fl.any (\e -> m `contains` e) c = Right True + -- 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 + +-- | `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 + + + diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -28,14 +28,12 @@ import Data.Set ( Set ) import Funsat.Solver ( solve + , verify , DPLLConfig(..) , defaultConfig - , CNF - , GenCNF(..) - , Solution(..) - , verify - , NonStupidString(..) + , ShowWrapped(..) , statTable ) +import Funsat.Types( CNF, GenCNF(..) ) import Prelude hiding ( elem ) import System.Console.GetOpt import System.Environment ( getArgs ) @@ -67,13 +65,9 @@ validOptions :: [OptDescr RunOptions] validOptions = --- [ Option [] ["no-clause-learning"] (NoArg $ disableF ClauseLearning) --- "Use naivest clause learning." --- , Option [] ["no-watched-literals"] (NoArg $ disableF WatchedLiterals) --- "Just traverse the formula to find unit clauses." --- , Option [] ["no-vsids"] (NoArg $ disableF VSIDS) --- "Use static variable ordering." - [ Option [] ["no-restarts"] (NoArg $ disableF Restarts) + [ Option [] ["no-vsids"] (NoArg $ disableF VSIDS) + "Use static variable ordering." + , Option [] ["no-restarts"] (NoArg $ disableF Restarts) "Never restart." , Option [] ["verify"] (NoArg RunTests) "Run quickcheck properties and unit tests." @@ -131,30 +125,20 @@ let cfg = (defaultConfig cnf) { configUseVSIDS = not $ VSIDS `elem` features - , configUseWatchedLiterals = not $ WatchedLiterals `elem` features - , configUseRestarts = not $ Restarts `elem` features - , configUseLearning = not $ ClauseLearning `elem` features } - (solution, stats) = solve cfg cnf + , configUseRestarts = not $ Restarts `elem` features } + (solution, stats, rt) = solve cfg cnf endingTime <- solution `seq` getCurrentTime print solution print $ statTable stats `Tabular.combine` Tabular.mkTable - [[ Stupid "Real time " - , Stupid $ show (diffUTCTime endingTime startingTime)]] - case solution of - Sat m -> do - putStrLn "Verifying..." - case verify m cnf of - Just problemClauses -> - do putStrLn "VERIFICATION ERROR!" - print problemClauses - Nothing -> return () -#ifdef TESTING --- putStrLn $ --- "Minimal erroneous CNF:\n" --- ++ show (Properties.minimalError cnf) -#endif TESTING - Unsat -> return () + [[ WrapString "Real time " + , WrapString $ show (diffUTCTime endingTime startingTime)]] + putStr "Verifying solution..." + case verify solution rt cnf of + Just errorWitness -> + do putStrLn "\n--> VERIFICATION ERROR!" + print errorWitness + Nothing -> putStrLn "succeeded." usageHeader = "Usage: funsat [options] ... " diff --git a/Text/Tabular.hs b/Text/Tabular.hs --- a/Text/Tabular.hs +++ b/Text/Tabular.hs @@ -29,11 +29,11 @@ chosen. That is, elements along too-long dimensions are chopped off. -} -module Text.Tabular( T(..), mkTable, combine, unTable ) where +module Text.Tabular( Table(..), mkTable, combine, unTable ) where import Data.List( intercalate ) -newtype T a = T [Row a] -- table is a list of rows +newtype Table a = Table [Row a] -- table is a list of rows newtype Row a = Row [Cell a] data Cell a = Cell { cellWidth :: !Int -- the width of a cell is the max of the widths of the @@ -41,17 +41,17 @@ -- in which this cell occurs , cellData :: !a } -- element printed in box of colWidth -mkTable :: (Show a) => [[a]] -> T a -mkTable rows = T $ mkRows rows +mkTable :: (Show a) => [[a]] -> Table a +mkTable rows = Table $ mkRows rows where widths = colWidths rows mkRows rows = [ Row (map mkCell (zip widths row)) | row <- rows ] mkCell = uncurry Cell -unTable :: T a -> [[a]] -unTable (T rows) = [ map cellData r | (Row r) <- rows ] +unTable :: Table a -> [[a]] +unTable (Table rows) = [ map cellData r | (Row r) <- rows ] -combine :: (Show a) => T a -> T a -> T a +combine :: (Show a) => Table a -> Table a -> Table a -- slow impl but works combine t t' = mkTable (unTable t ++ unTable t') @@ -60,8 +60,8 @@ colWidths = map (maximum . map (length . show)) . zipn -- Pretty, columnar output. -instance (Show a) => Show (T a) where - show (T rows) = intercalate "\n" $ map showRow rows +instance (Show a) => Show (Table a) where + show (Table rows) = intercalate "\n" $ map showRow rows where showRow (Row cols) = intercalate " " $ colStrings where diff --git a/funsat.cabal b/funsat.cabal --- a/funsat.cabal +++ b/funsat.cabal @@ -1,14 +1,19 @@ Name: funsat -Version: 0.4 +Version: 0.5 Cabal-Version: >= 1.2 Description: 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. It is possible to use funsat - both as a library and as a standalone executable. + 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"). + Synopsis: A modern DPLL-style SAT solver Category: Algorithms Stability: alpha @@ -22,16 +27,18 @@ Executable funsat Main-is: Main.hs - Ghc-options: -W + Ghc-options: -W -funbox-strict-fields Extensions: CPP CPP-options: -DTESTING Hs-source-dirs: . tests Other-modules: Funsat.Solver + Funsat.Types + Funsat.Resolution Funsat.FastDom Funsat.Utils + Funsat.Monad Text.Tabular - DPLL.Monad Control.Monad.MonadST Properties @@ -53,7 +60,12 @@ Library - Exposed-modules: Funsat.Solver DPLL.Monad Control.Monad.MonadST Text.Tabular + Exposed-modules: Funsat.Solver + Funsat.Types + Funsat.Resolution + Funsat.Monad + Control.Monad.MonadST + Text.Tabular Other-modules: Funsat.FastDom Funsat.Utils Ghc-options: -W -funbox-strict-fields Extensions: CPP diff --git a/tests/Properties.hs b/tests/Properties.hs --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -20,7 +20,7 @@ Copyright 2008 Denis Bueno -} -import Funsat.Solver hiding ( (==>) ) +import Funsat.Solver hiding ((==>)) import Control.Monad (replicateM) import Data.Array.Unboxed @@ -31,17 +31,21 @@ import Data.Maybe import Data.Ord( comparing ) import Debug.Trace +import Funsat.Solver( verify ) +import Funsat.Types +import Funsat.Utils( count, argmin ) import Language.CNF.Parse.ParseDIMACS( parseCNF ) import Prelude hiding ( or, and, all, any, elem, minimum, foldr, splitAt, concatMap , sum, concat ) +import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace ) import System.Random import Test.QuickCheck hiding (defaultConfig) -import Funsat.Utils( count, argmin ) import qualified Data.Foldable as Foldable import qualified Data.List as List import qualified Data.Set as Set -import qualified Test.QuickCheck as QC +import qualified Funsat.Resolution as Resolution import qualified Language.CNF.Parse.ParseDIMACS as ParseCNF +import qualified Test.QuickCheck as QC main :: IO () @@ -74,10 +78,14 @@ setStdGen (mkStdGen 42) check solveConfig prop_solveCorrect + setStdGen (mkStdGen 42) + check resChkConfig prop_resolutionChecker + config = QC.defaultConfig { configMaxTest = 1000 } -- Special configuration for the "solve this random instance" tests. solveConfig = QC.defaultConfig { configMaxTest = 2000 } +resChkConfig = QC.defaultConfig{ configMaxTest = 1200 } myConfigEvery testnum args = show testnum ++ ": " ++ show args ++ "\n\n" @@ -89,9 +97,26 @@ classify (numClauses cnf > 30 || numVars cnf > 20) "c>30, v>20" $ classify (numVars cnf > 20) "c>30, v>30" $ case solve (defaultConfig cnf) cnf of - (Sat m,_) -> label "SAT" $ verifyBool m cnf - (Unsat,_) -> label "UNSAT-unverified" $ True + (Sat m,_,rt) -> label "SAT" $ verifyBool (Sat m) rt cnf + (Unsat _,_,rt) -> label "UNSAT" $ + case Resolution.checkDepthFirst (fromJust rt) of + Left e -> + trace ("rt = " ++ show rt ++ "\n" + ++ "Resolution checker error: " ++ show e) + $ False + Right _ -> True +prop_resolutionChecker (cnf :: UnsatCNF) = + label "prop_resolutionChecker" $ + case solve1 (unUnsatCNF cnf) of + (Sat _,_,_) -> label "SAT" True + (Unsat _,_,rt) -> label "UNSAT" $ + case Resolution.checkDepthFirst (fromJust rt) of + Left e -> False + Right unsatCore -> + case solve1 ((unUnsatCNF cnf){ clauses = Set.fromList unsatCore}) of + (Sat _,_,_) -> False + (Unsat _,_,_) -> True prop_allIsTrueUnderA (m :: IAssignment) = label "prop_allIsTrueUnderA"$ @@ -234,8 +259,9 @@ - +------------------------------------------------------------------------------ -- * Helpers +------------------------------------------------------------------------------ @@ -298,7 +324,9 @@ (x:xs) /\/ ys = x : (ys /\/ xs) +------------------------------------------------------------------------------ -- * Generators +------------------------------------------------------------------------------ instance Arbitrary Var where arbitrary = sized $ \n -> V `fmap` choose (1, n) @@ -307,24 +335,30 @@ -- Generates assignment that never has a subset {l, -l}. instance Arbitrary IAssignment where - arbitrary = sized $ assign' + arbitrary = sized assign' where assign' n = do lits :: [Lit] <- vector n return $ array (V 1, V n) $ map (\i -> (var i, unLit i)) (nub lits) instance Arbitrary CNF where - arbitrary = sized genRandom3SAT + arbitrary = sized (genRandom3SAT 3.0) sizedLit n = do v <- choose (1, n) t <- oneof [return id, return negate] return $ L (t v) -genRandom3SAT :: Int -> Gen CNF -genRandom3SAT n = - do let clausesPerVar = 3.0 - nClauses = ceiling (fromIntegral nVars * clausesPerVar) +-- Generate a random 3SAT problem with the given ratio of clauses/variable. +-- +-- Current research suggests: +-- +-- * ~ 4.3: hardest instances +-- * < 4.3: SAT & easy +-- * > 4.3: UNSAT & easy +genRandom3SAT :: Double -> Int -> Gen CNF +genRandom3SAT clausesPerVar n = + do let nClauses = ceiling (fromIntegral nVars * clausesPerVar) clauseList <- replicateM nClauses arbClause return $ CNF { numVars = nVars , numClauses = nClauses @@ -339,32 +373,6 @@ return [a,b,c] -genCNF2 n = gen (fromIntegral n) - where - gen n = - let _g = n `div` 4 - lits :: [Lit] = map L [1..n] - genClause1 [a,b,c,d] = - map (map negate) [[a,b,c], [a,b,d], [a,c,d], [b,c,d]] - genClause1 _ = error "genClause1: bad arg" - genClause2 [a,b,c,d] = [[a,b,c], [a,b,d], [a,c,d], [b,c,c]] - genClause2 _ = error "genClause2: bad arg" - _genUnsat [a,b,c,d,e] = - map (map negate) - [[a,b,c,d] - ,[a,b,c,e] - ,[a,b,d,e] - ,[a,c,d, negate e] - ,[b,c,d, negate e]] - _genUnsat _ = error "genUnsat: bad arg" - in do groups1 <- return $ concatMap genClause1 $ windows 4 lits - lits' <- permute lits - groups2 <- return $ concatMap genClause2 $ windows 4 lits' - return $ - CNF {numVars = n - ,numClauses = length groups1 + length groups1 - ,clauses = Set.fromList $ groups1 ++ groups2} - windows :: Int -> [a] -> [[a]] windows n xs = if length xs < n then [] @@ -379,7 +387,18 @@ _ -> error "permute: bug" +newtype UnsatCNF = UnsatCNF { unUnsatCNF :: CNF } deriving (Show) +instance Arbitrary UnsatCNF where + arbitrary = do + f <- sized (genRandom3SAT 5.19) + return (UnsatCNF f) + + + + +------------------------------------------------------------------------------ -- ** Simplification +------------------------------------------------------------------------------ class WellFoundedSimplifier a where -- | If the argument can be made simpler, a list of one-step simpler @@ -438,8 +457,8 @@ where satAndWrong f_inner = trace (show (numVars f_inner) ++ "/" ++ show (numClauses f_inner)) $ case solve1 f_inner of - (Unsat,_) -> False - (Sat assignment,_) -> not (verifyBool assignment f_inner) + (Unsat _,_,_) -> False + (Sat a,_,rt) -> not (verifyBool (Sat a) rt f_inner) -- last (takeWhile p xs) in the common case. -- mnemonic: "last Such That" @@ -483,6 +502,6 @@ -- return $ B.unpack bs -- lazy unpack into String -verifyBool :: IAssignment -> CNF -> Bool -verifyBool m problem = isNothing $ verify m problem +verifyBool :: Solution -> Maybe ResolutionTrace -> CNF -> Bool +verifyBool sol maybeRT formula = isNothing $ verify sol maybeRT formula