{-# LANGUAGE PatternSignatures ,MultiParamTypeClasses ,FunctionalDependencies ,FlexibleInstances ,FlexibleContexts ,GeneralizedNewtypeDeriving ,TypeSynonymInstances ,TypeOperators ,ParallelListComp ,BangPatterns #-} {-# OPTIONS -cpp #-} {-| 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