-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A modern DPLL-style SAT solver -- -- Funsat is a native Haskell SAT solver that uses modern techniques for -- solving SAT instances. Current features include two-watched literals, -- conflict-directed learning, non-chronological backtracking, a -- VSIDS-like dynamic variable ordering, and restarts. Our goal is to -- facilitate convenient embedding of a reasonably fast SAT solver as a -- constraint solving backend in other applications. Currently along this -- theme we provide unsatisfiable core generation, giving -- (hopefully) small unsatisfiable sub-problems of unsatisfiable input -- problems (see Funsat.Resolution). @package funsat @version 0.5.2 -- | Tabular output. -- -- Converting any matrix of showable data types into a tabular form for -- which the layout is automatically done properly. Currently there is no -- maximum row width, just a dynamically-calculated column width. -- -- If the input matrix is mal-formed, the largest well-formed submatrix -- is chosen. That is, elements along too-long dimensions are chopped -- off. module Text.Tabular newtype Table a Table :: [Row a] -> Table a mkTable :: (Show a) => [[a]] -> Table a combine :: (Show a) => Table a -> Table a -> Table a unTable :: Table a -> [[a]] instance (Show a) => Show (Table a) -- | Idea from -- http://haskell.org/pipermail/libraries/2003-September/001411.html module Control.Monad.MonadST -- | A type class for monads that are able to perform ST actions. class (Monad m) => MonadST s m | m -> s liftST :: (MonadST s m) => ST s a -> m a readSTRef :: (MonadST s m) => STRef s a -> m a writeSTRef :: (MonadST s m) => STRef s a -> a -> m () newSTRef :: (MonadST s m) => a -> m (STRef s a) modifySTRef :: (MonadST s m) => STRef s a -> (a -> a) -> m () instance MonadST s (ST s) -- | The main SAT solver monad. Embeds ST. See type -- SSTErrMonad, which stands for ''State ST Error Monad''. module Funsat.Monad liftST :: (MonadST s m) => ST s a -> m a -- | 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)) evalSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> st -> ST s (Either e a) -- | 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. data SSTErrMonad e st s a instance (Error e) => MonadPlus (SSTErrMonad e st s) instance (Error e) => MonadError e (SSTErrMonad e st s) instance MonadState st (SSTErrMonad e st s) instance Monad (SSTErrMonad e st s) instance MonadST s (SSTErrMonad e st s) -- | Data types used when dealing with SAT problems in funsat. module Funsat.Types newtype Var V :: Int -> Var unVar :: Var -> Int newtype Lit L :: Int -> Lit unLit :: Lit -> Int inLit :: (Int -> Int) -> Lit -> Lit -- | The polarity of the literal. Negative literals are false; positive -- literals are true. The 0-literal is an error. litSign :: Lit -> Bool -- | The variable for the given literal. var :: Lit -> Var type Clause = [Lit] data CNF CNF :: Int -> Int -> Set Clause -> CNF numVars :: CNF -> Int numClauses :: CNF -> Int clauses :: CNF -> Set Clause -- | 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 without :: (Setlike t a) => t -> a -> t with :: (Setlike t a) => t -> a -> t contains :: (Setlike t a) => t -> a -> Bool -- | 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 -- | See freezeAss. unsafeFreezeAss :: (MonadST s m) => MAssignment s -> m IAssignment thawAss :: IAssignment -> ST s (MAssignment s) unsafeThawAss :: IAssignment -> ST s (MAssignment s) -- | Destructively update the assignment with the given literal. assign :: MAssignment s -> Lit -> ST s (MAssignment s) -- | Destructively undo the assignment to the given literal. unassign :: MAssignment s -> Lit -> ST s (MAssignment s) -- | The assignment as a list of signed literals. litAssignment :: IAssignment -> [Lit] -- | 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 :: f Node -> f Node -> Node -> gr a b -> Cut f gr a b -- | The reason side contains at least the decision variables. reasonSide :: Cut f gr a b -> f Node -- | The conflict side contains the conflicting literal. conflictSide :: Cut f gr a b -> f Node cutUIP :: Cut f gr a b -> Node cutGraph :: Cut f gr a b -> gr a b -- | Annotate each variable in the conflict graph with literal (indicating -- its assignment) and decision level. The only reason we make a new -- datatype for this is for its Show instance. data CGNodeAnnot CGNA :: Lit -> Int -> CGNodeAnnot -- | 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 statusUnder :: (Model a m) => a -> m -> Either () Bool 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 -- | The VSIDS-like dynamic variable ordering. newtype VarOrder s VarOrder :: STUArray s Var Double -> VarOrder s varOrderArr :: VarOrder s -> STUArray s Var Double newtype FrozenVarOrder FrozenVarOrder :: (UArray Var Double) -> FrozenVarOrder -- | 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 :: !Int -> ![Int] -> ![(Clause, ClauseId)] -> Map ClauseId [ClauseId] -> PartialResolutionTrace resTraceIdCount :: PartialResolutionTrace -> !Int resTrace :: PartialResolutionTrace -> ![Int] resTraceOriginalSingles :: PartialResolutionTrace -> ![(Clause, ClauseId)] resSourceMap :: PartialResolutionTrace -> Map ClauseId [ClauseId] type ReasonMap = Map Var (Clause, ClauseId) type ClauseId = Int instance Show PartialResolutionTrace instance Show FrozenVarOrder instance Show (VarOrder s) instance Show CNF instance Read CNF instance Eq CNF instance Eq Lit instance Ord Lit instance Enum Lit instance Ix Lit instance Eq Var instance Ord Var instance Enum Var instance Ix Var instance Show (STArray s a b) instance Show (STUArray s Var Double) instance Show (STUArray s Var Int) instance Show (STRef s a) instance Model Clause IAssignment instance Model Var IAssignment instance Model Lit IAssignment instance Show CGNodeAnnot instance (Show (f Node), Show (gr a b)) => Show (Cut f gr a b) instance Hash Var instance Hash Lit instance (Ord a, Hash a) => Setlike (BitSet a) a instance (Ord k, Ord a) => Setlike (Map k a) (k, a) instance Setlike IAssignment Lit instance (Ord a) => Setlike [a] a instance (Ord a) => Setlike (Set a) a instance Read Lit instance Show Lit instance Num Lit instance Num Var instance Show Var -- | 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 -- | The depth-first method. checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore data ResolutionTrace ResolutionTrace :: ClauseId -> IAssignment -> Map ClauseId [ClauseId] -> Map ClauseId Clause -> Map Var ClauseId -> ResolutionTrace -- | The id of the last, conflicting clause in the solving process. traceFinalClauseId :: ResolutionTrace -> ClauseId -- | Final assignment. -- -- Precondition: All variables assigned at decision level zero. traceFinalAssignment :: ResolutionTrace -> IAssignment -- | 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.) traceSources :: ResolutionTrace -> Map ClauseId [ClauseId] -- | Original clauses of the CNF input formula. traceOriginalClauses :: ResolutionTrace -> Map ClauseId Clause traceAntecedents :: ResolutionTrace -> Map Var ClauseId initResolutionTrace :: ClauseId -> IAssignment -> ResolutionTrace -- | 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 -- | Indicates that the clauses do not properly resolve on the variable. ResolveError :: Var -> Clause -> Clause -> ResolutionError -- | Indicates that the clauses do not have complementary variables or have -- too many. The complementary variables (if any) are in the list. CannotResolve :: [Var] -> Clause -> Clause -> ResolutionError -- | Indicates that the constructed antecedent clause not unit under -- traceFinalAssignment. AntecedentNotUnit :: Clause -> ResolutionError -- | Indicates that in the clause-lit pair, the unit literal of clause is -- the literal, but it ought to be the variable. AntecedentImplication :: (Clause, Lit) -> Var -> ResolutionError -- | Indicates that the variable has no antecedent mapping, in which case -- it should never have been assigned/encountered in the first place. AntecedentMissing :: Var -> ResolutionError -- | Indicates that the clause id has an entry in traceSources but -- no resolution sources. EmptySource :: ClauseId -> ResolutionError -- | Indicates that the clause id is referenced but has no entry in -- traceSources. OrphanSource :: ClauseId -> ResolutionError -- | Unsatisfiable cores are not unique. type UnsatisfiableCore = [Clause] instance Show ResolutionError instance Show ResolutionTrace instance Error ResolutionError -- | 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. -- -- -- -- -- -- module Funsat.Solver -- | 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 when the result is Unsat. solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace) -- | Solve with the default configuration defaultConfig. solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace) -- | The solution to a SAT problem. In each case we return an assignment, -- which is obviously right in the Sat case; in the Unsat -- case, the reason is to assist in the generation of an unsatisfiable -- core. data Solution Sat :: IAssignment -> Solution Unsat :: IAssignment -> Solution -- | 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 data VerifyError -- | Indicates a unsatisfactory assignment that was claimed satisfactory. -- Each clause is tagged with its status using -- Model.statusUnder. SatError :: [(Clause, Either () Bool)] -> VerifyError -- | Indicates an error in the resultion checking process. UnsatError :: ResolutionError -> VerifyError -- | Configuration parameters for the solver. data DPLLConfig Cfg :: !Int64 -> !Double -> !Bool -> !Bool -> DPLLConfig -- | Number of conflicts before a restart. configRestart :: DPLLConfig -> !Int64 -- | configRestart is altered after each restart by multiplying it -- by this value. configRestartBump :: DPLLConfig -> !Double -- | If true, use dynamic variable ordering. configUseVSIDS :: DPLLConfig -> !Bool configUseRestarts :: DPLLConfig -> !Bool -- | A default configuration based on the formula to solve. -- -- defaultConfig :: CNF -> DPLLConfig data Stats Stats :: Int64 -> Int64 -> Int64 -> Double -> Int64 -> Int64 -> Stats -- | Number of conflicts since last restart. statsNumConfl :: Stats -> Int64 -- | Number of conflicts since beginning of solving. statsNumConflTotal :: Stats -> Int64 -- | Number of learned clauses currently in DB (fluctuates because DB is -- compacted every restart). statsNumLearnt :: Stats -> Int64 -- | Avg. number of literals per learnt clause. statsAvgLearntLen :: Stats -> Double -- | Total number of decisions since beginning of solving. statsNumDecisions :: Stats -> Int64 -- | Total number of unit implications since beginning of solving. statsNumImpl :: Stats -> Int64 -- | The show instance uses the wrapped string. newtype ShowWrapped WrapString :: String -> ShowWrapped unwrapString :: ShowWrapped -> String -- | Convert statistics to a nice-to-display tabular form. statTable :: Stats -> Table ShowWrapped -- | Converts statistics into a tabular, human-readable summary. statSummary :: Stats -> String instance Show VerifyError instance Show (FunsatState s) instance Eq Solution instance Show DPLLConfig instance Show Stats instance Show ShowWrapped instance Error () instance Error (Lit, Clause, ClauseId) instance Show Solution