funsat 0.4 → 0.5
raw patch · 9 files changed
+2001/−1565 lines, 9 files
Files
- DPLL/Monad.hs +0/−82
- Funsat/Monad.hs +102/−0
- Funsat/Resolution.hs +278/−0
- Funsat/Solver.hs +1217/−1394
- Funsat/Types.hs +300/−0
- Main.hs +16/−32
- Text/Tabular.hs +9/−9
- funsat.cabal +18/−6
- tests/Properties.hs +61/−42
− DPLL/Monad.hs
@@ -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--- <http://haskell.org/haskellwiki/Performance/Monads>.-newtype SSTErrMonad e st s a =- SSTErrMonad { unSSTErrMonad :: forall r. (a -> (st -> ST s (Either e r, st)))- -> (st -> ST s (Either e r, st)) }--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')
+ Funsat/Monad.hs view
@@ -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 <http://www.gnu.org/licenses/>.++ 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+-- <http://haskell.org/haskellwiki/Performance/Monads>.+newtype SSTErrMonad e st s a =+ SSTErrMonad { unSSTErrMonad :: forall r. (a -> (st -> ST s (Either e r, st)))+ -> (st -> ST s (Either e r, st)) }++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')
+ Funsat/Resolution.hs view
@@ -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 <http://www.gnu.org/licenses/>.++ 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)
Funsat/Solver.hs view
@@ -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 <http://www.gnu.org/licenses/>.-- 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 "<STRef>"-instance Show (STUArray s Var Int) where- show = const "<STUArray Var Int>"-instance Show (STUArray s Var Double) where- show = const "<STUArray Var Double>"-instance Show (STArray s a b) where- show = const "<STArray>"---- | 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 <http://www.gnu.org/licenses/>.++ 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 "<STRef>"+instance Show (STUArray s Var Int) where+ show = const "<STUArray Var Int>"+instance Show (STUArray s Var Double) where+ show = const "<STUArray Var Double>"+instance Show (STArray s a b) where+ show = const "<STArray>"++-- | 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)
+ Funsat/Types.hs view
@@ -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 <http://www.gnu.org/licenses/>.++ 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+++
Main.hs view
@@ -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] <cnf-filename> ... <cnf-filename>"
Text/Tabular.hs view
@@ -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
funsat.cabal view
@@ -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
tests/Properties.hs view
@@ -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