diff --git a/CHANGES b/CHANGES --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,9 @@ -*- mode: outline -*- +* 0.6.0 +- Logical circuit representation added. +- License is now BSD3, which is apparently happier for some people. + * 0.5.2 Maintenance update because a new (incompatible) version of bitset, version 1.0, was released. Funsat should again compile via cabal-install. diff --git a/Control/Monad/MonadST.hs b/Control/Monad/MonadST.hs deleted file mode 100644 --- a/Control/Monad/MonadST.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-# LANGUAGE MultiParamTypeClasses - ,FunctionalDependencies - ,FlexibleInstances - #-} - - -{- - This file is part of funsat. - - funsat is free software: you can redistribute it and/or modify - it under the terms of the GNU Lesser General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - funsat is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public License - along with funsat. If not, see . - - Copyright 2008 Denis Bueno --} - - --- | Idea from -module Control.Monad.MonadST where - -import Control.Monad.ST -import Data.STRef - --- | A type class for monads that are able to perform `ST' actions. -class (Monad m) => MonadST s m | m -> s where - liftST :: ST s a -> m a - -instance MonadST s (Control.Monad.ST.ST s) where - liftST = id - -readSTRef :: MonadST s m => STRef s a -> m a -readSTRef = liftST . Data.STRef.readSTRef - -writeSTRef :: MonadST s m => STRef s a -> a -> m () -writeSTRef r x = liftST (Data.STRef.writeSTRef r x) - -newSTRef :: MonadST s m => a -> m (STRef s a) -newSTRef = liftST . Data.STRef.newSTRef - -modifySTRef :: MonadST s m => STRef s a -> (a -> a) -> m () -modifySTRef r f = liftST (Data.STRef.modifySTRef r f) - diff --git a/Funsat/FastDom.hs b/Funsat/FastDom.hs deleted file mode 100644 --- a/Funsat/FastDom.hs +++ /dev/null @@ -1,122 +0,0 @@ - --- From a patch to the dominators lib on ghc's trac; should be incorporated --- into fgl in GHC sooner or later. - --- | Find Dominators of a graph. --- --- Author: Bertram Felgenhauer --- --- Implementation based on --- Keith D. Cooper, Timothy J. Harvey, Ken Kennedy, --- ''A Simple, Fast Dominance Algorithm'', --- (http://citeseer.ist.psu.edu/cooper01simple.html) -module Funsat.FastDom - ( dom - , iDom ) where - -import Data.Graph.Inductive.Graph -import Data.Graph.Inductive.Query.DFS -import Data.Tree (Tree(..)) -import qualified Data.Tree as T -import Data.Array -import Data.IntMap (IntMap) -import qualified Data.IntMap as I - --- | return immediate dominators for each node of a graph, given a root -iDom :: Graph gr => gr a b -> Node -> [(Node,Node)] -iDom g root = let (result, toNode, _) = idomWork g root - in map (\(a, b) -> (toNode ! a, toNode ! b)) (assocs result) - - --- | return the set of dominators of the nodes of a graph, given a root -dom :: Graph gr => gr a b -> Node -> [(Node,[Node])] -dom g root = let - (iDom, toNode, fromNode) = idomWork g root - dom' = getDom toNode iDom - nodes' = nodes g - rest = I.keys (I.filter (-1 ==) fromNode) - in - [(toNode ! i, dom' ! i) | i <- range (bounds dom')] ++ - [(n, nodes') | n <- rest] - --- internal node type -type Node' = Int --- array containing the immediate dominator of each node, or an approximation --- thereof. the dominance set of a node can be found by taking the union of --- {node} and the dominance set of its immediate dominator. -type IDom = Array Node' Node' --- array containing the list of predecessors of each node -type Preds = Array Node' [Node'] --- arrays for translating internal nodes back to graph nodes and back -type ToNode = Array Node' Node -type FromNode = IntMap Node' - -idomWork :: Graph gr => gr a b -> Node -> (IDom, ToNode, FromNode) -idomWork g root = let - -- use depth first tree from root do build the first approximation - trees@(~[tree]) = dff [root] g - -- relabel the tree so that paths from the root have increasing nodes - (s, ntree) = numberTree 0 tree - -- the approximation iDom0 just maps each node to its parent - iDom0 = array (1, s-1) (tail $ treeEdges (-1) ntree) - -- fromNode translates graph nodes to relabeled (internal) nodes - fromNode = I.unionWith const (I.fromList (zip (T.flatten tree) (T.flatten ntree))) (I.fromList (zip (nodes g) (repeat (-1)))) - -- toNode translates internal nodes to graph nodes - toNode = array (0, s-1) (zip (T.flatten ntree) (T.flatten tree)) - preds = array (1, s-1) [(i, filter (/= -1) (map (fromNode I.!) - (pre g (toNode ! i)))) | i <- [1..s-1]] - -- iteratively improve the approximation to find iDom. - iDom = fixEq (refineIDom preds) iDom0 - in - if null trees then error "Dominators.idomWork: root not in graph" - else (iDom, toNode, fromNode) --- for each node in iDom, find the intersection of all its predecessor's --- dominating sets, and update iDom accordingly. -refineIDom :: Preds -> IDom -> IDom -refineIDom preds iDom = fmap (foldl1 (intersect iDom)) preds - --- find the intersection of the two given dominance sets. -intersect :: IDom -> Node' -> Node' -> Node' -intersect iDom a b = case a `compare` b of - LT -> intersect iDom a (iDom ! b) - EQ -> a - GT -> intersect iDom (iDom ! a) b - --- convert an IDom to dominance sets. we translate to graph nodes here --- because mapping later would be more expensive and lose sharing. -getDom :: ToNode -> IDom -> Array Node' [Node] -getDom toNode iDom = let - res = array (0, snd (bounds iDom)) ((0, [toNode ! 0]) : - [(i, toNode ! i : res ! (iDom ! i)) | i <- range (bounds iDom)]) - in - res --- relabel tree, labeling vertices with consecutive numbers in depth first order -numberTree :: Node' -> Tree a -> (Node', Tree Node') -numberTree n (Node _ ts) = let (n', ts') = numberForest (n+1) ts - in (n', Node n ts') - --- same as numberTree, for forests. -numberForest :: Node' -> [Tree a] -> (Node', [Tree Node']) -numberForest n [] = (n, []) -numberForest n (t:ts) = let (n', t') = numberTree n t - (n'', ts') = numberForest n' ts - in (n'', t':ts') - --- return the edges of the tree, with an added dummy root node. -treeEdges :: a -> Tree a -> [(a,a)] -treeEdges a (Node b ts) = (b,a) : concatMap (treeEdges b) ts - --- find a fixed point of f, iteratively -fixEq :: Eq a => (a -> a) -> a -> a -fixEq f v | v' == v = v - | otherwise = fixEq f v' - where v' = f v - -{- -:m +Data.Graph.Inductive -let g0 = mkGraph [(i,()) | i <- [0..4]] [(a,b,()) | (a,b) <- [(0,1),(1,2),(0,3),(3,2),(4,0)]] :: Gr () () -let g1 = mkGraph [(i,()) | i <- [0..4]] [(a,b,()) | (a,b) <- [(0,1),(1,2),(2,3),(1,3),(3,4)]] :: Gr () () -let g2,g3,g4 :: Int -> Gr () (); g2 n = mkGraph [(i,()) | i <- [0..n-1]] ([(a,a+1,()) | a <- [0..n-2]] ++ [(a,a+2,()) | a <- [0..n-3]]); g3 n =mkGraph [(i,()) | i <- [0..n-1]] ([(a,a+2,()) | a <- [0..n-3]] ++ [(a,a+1,()) | a <- [0..n-2]]); g4 n =mkGraph [(i,()) | i <- [0..n-1]] ([(a+2,a,()) | a <- [0..n-3]] ++ [(a+1,a,()) | a <- [0..n-2]]) -:m -Data.Graph.Inductive --} - diff --git a/Funsat/Monad.hs b/Funsat/Monad.hs deleted file mode 100644 --- a/Funsat/Monad.hs +++ /dev/null @@ -1,103 +0,0 @@ -{-# LANGUAGE PolymorphicComponents - ,MultiParamTypeClasses - ,FunctionalDependencies - ,FlexibleInstances - #-} - -{- - This file is part of funsat. - - funsat is free software: you can redistribute it and/or modify - it under the terms of the GNU Lesser General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - funsat is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public License - along with funsat. If not, see . - - Copyright 2008 Denis Bueno --} - - -{-| - -The main SAT solver monad. Embeds `ST'. See type `SSTErrMonad', which stands -for ''State ST Error Monad''. - --} -module Funsat.Monad - ( liftST - , runSSTErrMonad - , evalSSTErrMonad - , SSTErrMonad ) - where -import Control.Monad.Error -import Control.Monad.ST.Strict -import Control.Monad.State.Class -import Control.Monad.MonadST - - -instance MonadST s (SSTErrMonad e st s) where - liftST = dpllST - --- | Perform an @ST@ action in the DPLL monad. -dpllST :: ST s a -> SSTErrMonad e st s a -{-# INLINE dpllST #-} -dpllST st = SSTErrMonad (\k s -> st >>= \x -> k x s) - --- | @runSSTErrMonad m s@ executes a `SSTErrMonad' action with initial state @s@ --- until an error occurs or a result is returned. -runSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> (st -> ST s (Either e a, st)) -runSSTErrMonad m = unSSTErrMonad m (\x s -> return (return x, s)) - -evalSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> st -> ST s (Either e a) -evalSSTErrMonad m s = do (result, _) <- runSSTErrMonad m s - return result - --- | @SSTErrMonad e st s a@: the error type @e@, state type @st@, @ST@ thread --- @s@ and result type @a@. --- --- This is a monad embedding @ST@ and supporting error handling and state --- threading. It uses CPS to avoid checking `Left' and `Right' for every --- `>>='; instead only checks on `catchError'. Idea adapted from --- . -newtype SSTErrMonad e st s a = - SSTErrMonad { unSSTErrMonad :: forall r. (a -> (st -> ST s (Either e r, st))) - -> (st -> ST s (Either e r, st)) } - -instance Monad (SSTErrMonad e st s) where - return x = SSTErrMonad ($ x) - (>>=) = bindSSTErrMonad - -bindSSTErrMonad :: SSTErrMonad e st s a -> (a -> SSTErrMonad e st s b) - -> SSTErrMonad e st s b -{-# INLINE bindSSTErrMonad #-} -bindSSTErrMonad m f = - {-# SCC "bindSSTErrMonad" #-} - SSTErrMonad (\k -> unSSTErrMonad m (\a -> unSSTErrMonad (f a) k)) - -instance MonadState st (SSTErrMonad e st s) where - get = SSTErrMonad (\k s -> k s s) - put s' = SSTErrMonad (\k _ -> k () s') - -instance (Error e) => MonadError e (SSTErrMonad e st s) where - throwError err = -- throw away continuation - SSTErrMonad (\_ s -> return (Left err, s)) - catchError action handler = {-# SCC "catchErrorSSTErrMonad" #-} SSTErrMonad - (\k s -> do (x, s') <- runSSTErrMonad action s - case x of - Left error -> unSSTErrMonad (handler error) k s' - Right result -> k result s') - -instance (Error e) => MonadPlus (SSTErrMonad e st s) where - mzero = SSTErrMonad (\_ s -> return (Left noMsg, s)) - mplus m n = SSTErrMonad (\k s -> - do (r, s') <- runSSTErrMonad m s - case r of - Left _ -> unSSTErrMonad n k s' - Right x -> k x s') diff --git a/Funsat/Resolution.hs b/Funsat/Resolution.hs deleted file mode 100644 --- a/Funsat/Resolution.hs +++ /dev/null @@ -1,274 +0,0 @@ - -{- - This file is part of funsat. - - funsat is free software: you can redistribute it and/or modify - it under the terms of the GNU Lesser General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - funsat is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public License - along with funsat. If not, see . - - Copyright 2008 Denis Bueno --} - --- | Generates and checks a resolution proof of UNSAT from a resolution trace --- of a SAT solver (Funsat in particular will generate this trace). This is --- based on the implementation discussed in the paper ''Validating SAT Solvers --- Using an Independent Resolution-Based Checker: Practical Implementations --- and Other Applications'' by Lintao Zhang and Sharad Malik. --- --- As a side effect of this process an /unsatisfiable core/ is generated from --- the resolution trace, as discussed in the paper ''Extracting Small --- Unsatisfiable Cores from Unsatisfiable Boolean Formula'' by Zhang and --- Malik. -module Funsat.Resolution - ( -- * Interface - checkDepthFirst - -- * Data Types - , ResolutionTrace(..) - , initResolutionTrace - , ResolutionError(..) - , UnsatisfiableCore ) - 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, getUnit, isFalseUnder ) - - --- 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 } - --- | 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 = do - maybeClause <- getClause - case maybeClause of - Just clause -> return clause - Nothing -> do - sourcesMap <- asks traceSources - case Map.lookup clauseId sourcesMap of - Nothing -> throwError (OrphanSource clauseId) - Just [] -> throwError (EmptySource clauseId) - Just (firstSourceId:ids) -> recursiveBuildIds clauseId firstSourceId ids - where - -- If clause is an *original* clause, stash it as part of the UNSAT core. - getClause = do - origMap <- asks traceOriginalClauses - case Map.lookup clauseId origMap of - Just origClause -> withClauseInCore $ return (Just origClause) - Nothing -> Map.lookup clauseId `liftM` gets clauseIdMap - - withClauseInCore = - (modify (\s -> s{ unsatCore = IntSet.insert clauseId (unsatCore s) }) >>) - -recursiveBuildIds clauseId firstSourceId sourceIds = do - rc <- recursiveBuild firstSourceId -- recursive_build(id) - clause <- foldM buildAndResolve rc sourceIds - storeClauseId clauseId clause - return clause - - where - -- This is the body of the while loop inside the recursiveBuild - -- procedure in the paper. - buildAndResolve :: Clause -> ClauseId -> ResM (Clause) - buildAndResolve clause1 clauseId = - recursiveBuild clauseId >>= resolve Nothing clause1 - - -- Maps ClauseId to built Clause. - storeClauseId :: ClauseId -> Clause -> ResM () - storeClauseId clauseId clause = modify $ \s -> - s{ clauseIdMap = Map.insert clauseId clause (clauseIdMap s) } - - ------------------------------------------------------------------------------- --- HELPERS ------------------------------------------------------------------------------- - - --- | Resolve both clauses on the given variable, and throw a resolution error --- if anything is amiss. Specifically, it checks that there is exactly one --- occurrence of a literal with the given variable (if variable given) in each --- clause and they are opposite in polarity. --- --- If no variable specified, finds resolving variable, and ensures there's --- only one such variable. -resolve :: Maybe Var -> Clause -> Clause -> ResM Clause -resolve maybeV c1 c2 = - -- Find complementary literals: - case filter ((`elem` c2) . negate) c1 of - [l] -> case maybeV of - Nothing -> resolveVar (var l) - Just v -> if v == var l - then resolveVar v - else throwError $ ResolveError v c1 c2 - vs -> throwError $ CannotResolve (nub . map var $ vs) c1 c2 - where - resolveVar v = return . nub $ deleteVar v c1 ++ deleteVar v c2 - - deleteVar v c = c `without` lit v `without` negate (lit v) - lit (V i) = L i - --- | Get the antecedent (reason) for a variable. Every variable encountered --- ought to have a reason. -getAntecedentId :: Var -> ResM ClauseId -getAntecedentId v = do - anteMap <- asks traceAntecedents - case Map.lookup v anteMap of - Nothing -> throwError (AntecedentMissing v) - Just ante -> return ante - -chooseLiteral :: Clause -> ResM Lit -chooseLiteral (l:_) = return l -chooseLiteral _ = error "chooseLiteral: empty clause" - -checkAnteClause :: Var -> Clause -> ResM () -checkAnteClause v anteClause = do - a <- asks traceFinalAssignment - when (not (anteClause `hasUnitUnder` a)) - (throwError $ AntecedentNotUnit anteClause) - let unitLit = getUnit anteClause a - when (not $ var unitLit == v) - (throwError $ AntecedentImplication (anteClause, unitLit) v) - where - hasUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) diff --git a/Funsat/Solver.hs b/Funsat/Solver.hs deleted file mode 100644 --- a/Funsat/Solver.hs +++ /dev/null @@ -1,1040 +0,0 @@ -{-# LANGUAGE PatternSignatures - ,MultiParamTypeClasses - ,FunctionalDependencies - ,FlexibleInstances - ,FlexibleContexts - ,GeneralizedNewtypeDeriving - ,TypeSynonymInstances - ,TypeOperators - ,ParallelListComp - ,BangPatterns - #-} -{-# OPTIONS -cpp #-} - - - - - - -{-| - -Funsat aims to be a reasonably efficient modern SAT solver that is easy to -integrate as a backend to other projects. SAT is NP-complete, and thus has -reductions from many other interesting problems. We hope this implementation -is efficient enough to make it useful to solve medium-size, real-world problem -mapped from another space. We also aim to test the solver rigorously to -encourage confidence in its output. - -One particular nicetie facilitating integration of Funsat into other projects -is the efficient calculation of an /unsatisfiable core/ for unsatisfiable -problems (see the "Funsat.Resolution" module). In the case a problem is -unsatisfiable, as a by-product of checking the proof of unsatisfiability, -Funsat will generate a minimal set of input clauses that are also -unsatisfiable. - -* 07 Jun 2008 21:43:42: N.B. because of the use of mutable arrays in the ST -monad, the solver will actually give _wrong_ answers if you compile without -optimisation. Which is okay, 'cause that's really slow anyway. - -[@Bibliography@] - - * ''Abstract DPLL and DPLL Modulo Theories'' - - * ''Chaff: Engineering an Efficient SAT solver'' - - * ''An Extensible SAT-solver'' by Niklas Een, Niklas Sorensson - - * ''Efficient Conflict Driven Learning in a Boolean Satisfiability Solver'' -by Zhang, Madigan, Moskewicz, Malik - - * ''SAT-MICRO: petit mais costaud!'' by Conchon, Kanig, and Lescuyer - --} -module Funsat.Solver -#ifndef TESTING - ( -- * Interface - solve - , solve1 - , Solution(..) - -- ** Verification - , verify - , VerifyError(..) - -- ** Configuration - , DPLLConfig(..) - , defaultConfig - -- * Solver statistics - , Stats(..) - , ShowWrapped(..) - , statTable - , statSummary - ) -#endif - where - -{- - This file is part of funsat. - - funsat is free software: you can redistribute it and/or modify - it under the terms of the GNU Lesser General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - funsat is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public License - along with funsat. If not, see . - - Copyright 2008 Denis Bueno --} - - -import Control.Arrow( (&&&) ) -import Control.Exception( assert ) -import Control.Monad.Error hiding ( (>=>), forM_, runErrorT ) -import Control.Monad.MonadST( MonadST(..) ) -import Control.Monad.ST.Strict -import Control.Monad.State.Lazy hiding ( (>=>), forM_ ) -import Data.Array.ST -import Data.Array.Unboxed -import Data.Foldable hiding ( sequence_ ) -import Data.Int( Int64 ) -import Data.List( intercalate, nub, tails, sortBy, sort ) -import Data.Maybe -import Data.Ord( comparing ) -import Data.STRef -import Data.Sequence( Seq ) --- import Debug.Trace (trace) -import Funsat.Monad -import Funsat.Utils -import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace ) -import Funsat.Types -import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) -import Funsat.Resolution( ResolutionError(..) ) -import Text.Printf( printf ) -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 when the result is `Unsat'. -solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace) -solve cfg fIn = - -- To solve, we simply take baby steps toward the solution using solveStep, - -- starting with an initial assignment. --- trace ("input " ++ show f) $ - either (error "no solution") id $ - runST $ - evalSSTErrMonad - (do initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0 - (a, isUnsat) <- initialState initialAssignment - if isUnsat then reportSolution (Unsat a) - else stepToSolution initialAssignment >>= reportSolution) - SC{ cnf = f{ clauses = Set.empty }, dl = [] - , watches = undefined, learnt = undefined - , propQ = Seq.empty, trail = [], numConfl = 0, level = undefined - , numConflTotal = 0, numDecisions = 0, numImpl = 0 - , reason = Map.empty, varOrder = undefined - , resolutionTrace = PartialResolutionTrace 1 [] [] Map.empty - , dpllConfig = cfg } - where - f = preprocessCNF fIn - -- If returns True, then problem is unsat. - initialState :: MAssignment s -> DPLLMonad s (IAssignment, Bool) - initialState m = do - initialLevel <- liftST $ newSTUArray (V 1, V (numVars f)) noLevel - modify $ \s -> s{ level = initialLevel } - 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 } - - -- Watch each clause, making sure to bork if we find a contradiction. - (`catchError` - (const $ liftST (unsafeFreezeAss m) >>= \a -> return (a,True))) $ do - forM_ (clauses f) - (\c -> do cid <- nextTraceId - isConsistent <- watchClause m (c, cid) False - when (not isConsistent) - -- conflict data is ignored here, so safe to fake - (do traceClauseId cid ; throwError (L 0, [], 0))) - a <- liftST (unsafeFreezeAss m) - return (a, False) - - --- | Solve with the default configuration `defaultConfig'. -solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace) -solve1 f = solve (defaultConfig f) f - --- | This function applies `solveStep' recursively until SAT instance is --- solved, starting with the given initial assignment. It also implements the --- conflict-based restarting (see `DPLLConfig'). -stepToSolution :: MAssignment s -> DPLLMonad s Solution -stepToSolution assignment = do - step <- solveStep assignment - useRestarts <- gets (configUseRestarts . dpllConfig) - isTimeToRestart <- uncurry ((>=)) `liftM` - gets (numConfl &&& (configRestart . dpllConfig)) - case step of - Left m -> do when (useRestarts && isTimeToRestart) - (do _stats <- extractStats --- trace ("Restarting...") $ --- trace (statSummary stats) $ - resetState m) - stepToSolution m - Right s -> return s - where - resetState m = do - modify $ \s -> s{ numConfl = 0 } - -- Require more conflicts before next restart. - modifySlot dpllConfig $ \s c -> - s{ dpllConfig = c{ configRestart = ceiling (configRestartBump c - * fromIntegral (configRestart c)) - } } - lvl :: FrozenLevelArray <- gets level >>= liftST . unsafeFreeze - undoneLits <- takeWhile (\l -> lvl ! (var l) > 0) `liftM` gets trail - forM_ undoneLits $ const (undoOne m) - modify $ \s -> s{ dl = [], propQ = Seq.empty } - compactDB - unsafeFreezeAss m >>= simplifyDB - -reportSolution :: Solution -> DPLLMonad s (Solution, Stats, Maybe ResolutionTrace) -reportSolution s = do - stats <- extractStats - case s of - Sat _ -> return (s, stats, Nothing) - Unsat _ -> do - resTrace <- constructResTrace s - return (s, stats, Just resTrace) - - --- | Configuration parameters for the solver. -data DPLLConfig = Cfg - { configRestart :: !Int64 -- ^ Number of conflicts before a restart. - , 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 (Either (MAssignment s) Solution) -solveStep m = do - unsafeFreezeAss m >>= solveStepInvariants - conf <- gets dpllConfig - let selector = if configUseVSIDS conf then select else selectStatic - maybeConfl <- bcp m - mFr <- unsafeFreezeAss m - voArr <- gets (varOrderArr . varOrder) - voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze voArr) - s <- get - stepForward $ - -- Check if unsat. - unsat maybeConfl s ==> postProcessUnsat maybeConfl - -- Unit propagation may reveal conflicts; check. - >< maybeConfl >=> backJump m - -- No conflicts. Decide. - >< selector mFr voFr >=> decide m - where - -- Take the step chosen by the transition guards above. - stepForward Nothing = (Right . Sat) `liftM` unsafeFreezeAss m - stepForward (Just step) = do - r <- step - case r of - Nothing -> (Right . Unsat) `liftM` liftST (unsafeFreezeAss m) - Just m -> return . Left $ m - --- | /Precondition:/ problem determined to be unsat. --- --- Records id of conflicting clause in trace before failing. Always returns --- `Nothing'. -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 () - - --- | The solution to a SAT problem. In each case we return an assignment, --- which is obviously right in the `Sat' case; in the `Unsat' case, the reason --- is to assist in the generation of an unsatisfiable core. -data Solution = Sat IAssignment | Unsat IAssignment deriving (Eq) - -instance Show Solution where - show (Sat a) = "satisfiable: " ++ showAssignment a - show (Unsat _) = "unsatisfiable" - -finalAssignment :: Solution -> IAssignment -finalAssignment (Sat a) = a -finalAssignment (Unsat a) = a - --- ** Internals - --- | Value of the `level' array if corresponding variable unassigned. Had --- better be less that 0. -noLevel :: Level -noLevel = -1 - --- ** 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 - --- | 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) -{-# INLINE (==>) #-} -(==>) 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, 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 _ -> - case Resolution.checkDepthFirst (fromJust maybeRT) of - Left er -> Just . UnsatError $ er - Right _ -> Nothing - where isTrue (Right True) = True - isTrue _ = False - ---------------------------------------- --- Statistics & trace - - -data Stats = Stats - { statsNumConfl :: Int64 - -- ^ Number of conflicts since last restart. - - , statsNumConflTotal :: Int64 - -- ^ Number of conflicts since beginning of solving. - - , statsNumLearnt :: Int64 - -- ^ Number of learned clauses currently in DB (fluctuates because DB is - -- compacted every restart). - - , statsAvgLearntLen :: Double - -- ^ Avg. number of literals per learnt clause. - - , statsNumDecisions :: Int64 - -- ^ Total number of decisions since beginning of solving. - - , statsNumImpl :: Int64 - -- ^ Total number of unit implications since beginning of solving. - } - --- | The show instance uses the wrapped string. -newtype ShowWrapped = WrapString { unwrapString :: String } -instance Show ShowWrapped where show = unwrapString - -instance Show Stats where show = show . statTable - --- | Convert statistics to a nice-to-display tabular form. -statTable :: Stats -> Tabular.Table ShowWrapped -statTable s = - Tabular.mkTable - [ [WrapString "Num. Conflicts" - ,WrapString $ show (statsNumConflTotal s)] - , [WrapString "Num. Learned Clauses" - ,WrapString $ show (statsNumLearnt s)] - , [WrapString " --> Avg. Lits/Clause" - ,WrapString $ show (statsAvgLearntLen s)] - , [WrapString "Num. Decisions" - ,WrapString $ show (statsNumDecisions s)] - , [WrapString "Num. Propagations" - ,WrapString $ show (statsNumImpl s)] ] - --- | Converts statistics into a tabular, human-readable summary. -statSummary :: Stats -> String -statSummary s = - show (Tabular.mkTable - [[WrapString $ show (statsNumConflTotal s) ++ " Conflicts" - ,WrapString $ "| " ++ show (statsNumLearnt s) ++ " Learned Clauses" - ++ " (avg " ++ printf "%.2f" (statsAvgLearntLen s) - ++ " lits/clause)"]]) - - -extractStats :: DPLLMonad s Stats -extractStats = do - s <- get - learntArr <- liftST $ unsafeFreezeWatchArray (learnt s) - let learnts = (nub . Fl.concat) - [ map (sort . (\(_,c,_) -> c)) (learntArr!i) - | i <- (range . bounds) learntArr ] :: [Clause] - stats = - Stats { statsNumConfl = numConfl s - , statsNumConflTotal = numConflTotal s - , statsNumLearnt = fromIntegral $ length learnts - , statsAvgLearntLen = - fromIntegral (foldl' (+) 0 (map length learnts)) - / fromIntegral (statsNumLearnt stats) - , statsNumDecisions = numDecisions s - , statsNumImpl = numImpl s } - return stats - -unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s]) -unsafeFreezeWatchArray = freeze - - -constructResTrace :: Solution -> DPLLMonad s ResolutionTrace -constructResTrace sol = do - s <- get - watchesIndices <- range `liftM` liftST (getBounds (watches s)) - origClauseMap <- - foldM (\origMap i -> do - clauses <- liftST $ readArray (watches s) i - return $ - foldr (\(_, clause, clauseId) origMap -> - Map.insert clauseId clause origMap) - origMap - clauses) - Map.empty - watchesIndices - let singleClauseMap = - foldr (\(clause, clauseId) m -> Map.insert clauseId clause m) - Map.empty - (resTraceOriginalSingles . resolutionTrace $ s) - anteMap = - foldr (\l anteMap -> Map.insert (var l) (getAnteId s (var l)) anteMap) - Map.empty - (litAssignment . finalAssignment $ sol) - return - (initResolutionTrace - (head (resTrace . resolutionTrace $ s)) - (finalAssignment sol)) - { traceSources = resSourceMap . resolutionTrace $ s - , traceOriginalClauses = origClauseMap `Map.union` singleClauseMap - , traceAntecedents = anteMap } - where - getAnteId s v = snd $ - Map.findWithDefault (error $ "no reason for assigned var " ++ show v) - v (reason s) diff --git a/Funsat/Types.hs b/Funsat/Types.hs deleted file mode 100644 --- a/Funsat/Types.hs +++ /dev/null @@ -1,317 +0,0 @@ -{-# LANGUAGE PatternSignatures - ,MultiParamTypeClasses - ,FunctionalDependencies - ,FlexibleInstances - ,FlexibleContexts - ,GeneralizedNewtypeDeriving - ,TypeSynonymInstances - ,TypeOperators - ,ParallelListComp - ,BangPatterns - #-} - -{- - This file is part of funsat. - - funsat is free software: you can redistribute it and/or modify - it under the terms of the GNU Lesser General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - funsat is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public License - along with funsat. If not, see . - - Copyright 2008 Denis Bueno --} - - - --- | Data types used when dealing with SAT problems in funsat. -module Funsat.Types where - - -import Control.Monad.MonadST( MonadST(..) ) -import Control.Monad.ST.Strict -import Data.Array.ST -import Data.Array.Unboxed -import Data.BitSet ( BitSet ) -import Data.Foldable hiding ( sequence_ ) -import Data.Map ( Map ) -import Data.Set ( Set ) -import Data.STRef -import Funsat.Monad -import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) -import qualified Data.BitSet as BitSet -import qualified Data.Foldable as Fl -import qualified Data.Graph.Inductive.Graph as Graph -import qualified Data.List as List -import qualified Data.Map as Map -import qualified Data.Set as Set - - - --- * Basic Types - -newtype Var = V {unVar :: Int} deriving (Eq, Ord, Enum, Ix) - -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) - -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 - -inLit :: (Int -> Int) -> Lit -> Lit -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 - | otherwise = error "litSign of 0" - -instance Show Lit where show = show . unLit -instance Read Lit where - readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s) - --- | The variable for the given literal. -var :: Lit -> Var -var = V . abs . unLit - -type Clause = [Lit] - -data CNF = CNF - { numVars :: Int - , numClauses :: Int - , clauses :: Set Clause } deriving (Show, Read, Eq) - - --- | Represents a container of type @t@ storing elements of type @a@ that --- support membership, insertion, and deletion. --- --- 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) - --- | The union of the reason side and the conflict side are all the nodes in --- the `cutGraph' (excepting, perhaps, the nodes on the reason side at --- decision level 0, which should never be present in a learned clause). -data Cut f gr a b = - Cut { reasonSide :: f Graph.Node - -- ^ The reason side contains at least the decision variables. - , conflictSide :: f Graph.Node - -- ^ The conflict side contains the conflicting literal. - , cutUIP :: Graph.Node - , cutGraph :: gr a b } -instance (Show (f Graph.Node), Show (gr a b)) => Show (Cut f gr a b) where - show (Cut { conflictSide = c, cutUIP = uip }) = - "Cut (uip=" ++ show uip ++ ", cSide=" ++ show c ++ ")" - --- | Annotate each variable in the conflict graph with literal (indicating its --- assignment) and decision level. The only reason we make a new datatype for --- this is for its `Show' instance. -data CGNodeAnnot = CGNA Lit Int -instance Show CGNodeAnnot where - show (CGNA (L 0) _) = "lambda" - show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")" - - - --- * Model - - --- | 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 () - where - isFalseUnder x m = isFalse $ x `statusUnder` m - where isFalse (Right False) = True - isFalse _ = False - --- * 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 - - --- | 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 - -instance Show (STRef s a) where show = const "" -instance Show (STUArray s Var Int) where show = const "" -instance Show (STUArray s Var Double) where show = const "" -instance Show (STArray s a b) where show = const "" diff --git a/Funsat/Utils.hs b/Funsat/Utils.hs deleted file mode 100644 --- a/Funsat/Utils.hs +++ /dev/null @@ -1,281 +0,0 @@ -{-# LANGUAGE PatternSignatures - ,MultiParamTypeClasses - ,FunctionalDependencies - ,FlexibleInstances - ,FlexibleContexts #-} - -{- - This file is part of funsat. - - funsat is free software: you can redistribute it and/or modify - it under the terms of the GNU Lesser General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - funsat is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public License - along with funsat. If not, see . - - Copyright 2008 Denis Bueno --} - - -{-| - -Generic utilities that happen to be used in the SAT solver. In pretty much -every case, these functions will be useful for any number of manipulations, -and are not SAT-solver specific. - --} -module Funsat.Utils where - -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.List( foldl1' ) -import Data.Map (Map) -import Data.Set (Set) -import Debug.Trace( trace ) -import Funsat.Types -import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) -import System.IO.Unsafe( unsafePerformIO ) -import System.IO( hPutStr, stderr ) -import qualified Data.Foldable as Fl -import qualified Data.Graph.Inductive.Graph as Graph -import qualified Data.Graph.Inductive.Query.DFS as DFS -import qualified Data.List as List -import qualified Data.Map as Map -import qualified Data.Set as Set - - - --- | `True' if and only if the object is undefined in the model. -isUndefUnder :: Model a m => a -> m -> Bool -isUndefUnder x m = isUndef $ x `statusUnder` m - where isUndef (Left ()) = True - isUndef _ = False - --- | `True' if and only if the object is true in the model. -isTrueUnder :: Model a m => a -> m -> Bool -isTrueUnder x m = isTrue $ x `statusUnder` m - where isTrue (Right True) = True - isTrue _ = False - --- | `True' if and only if the object is false in the model. -isFalseUnder :: Model a m => a -> m -> Bool -isFalseUnder x m = isFalse $ x `statusUnder` m - where isFalse (Right False) = True - isFalse _ = False - --- * Helpers - - --- isUnitUnder c m | trace ("isUnitUnder " ++ show c ++ " " ++ showAssignment m) $ False = undefined - --- | Whether all the elements of the model in the list are false but one, and --- none is true, under the model. -isUnitUnder :: (Model a m) => [a] -> m -> Bool -{-# SPECIALISE INLINE isUnitUnder :: Clause -> IAssignment -> Bool #-} -isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) - && not (Fl.any (`isTrueUnder` m) c) - --- Precondition: clause is unit. --- getUnit :: (Model a m, Show a, Show m) => [a] -> m -> a --- getUnit c m | trace ("getUnit " ++ show c ++ " " ++ showAssignment m) $ False = undefined - --- | Get the element of the list which is not false under the model. If no --- such element, throws an error. -getUnit :: (Model a m, Show a) => [a] -> m -> a -{-# SPECIALISE INLINE getUnit :: Clause -> IAssignment -> Lit #-} -getUnit c m = case filter (not . (`isFalseUnder` m)) c of - [u] -> u - xs -> error $ "getUnit: not unit: " ++ show xs - - -{-# INLINE mytrace #-} -mytrace msg expr = unsafePerformIO $ do - hPutStr stderr msg - return expr - -outputConflict fn g x = unsafePerformIO $ do writeFile fn g - return x - - --- | /O(1)/ Whether a list contains a single element. -isSingle :: [a] -> Bool -{-# INLINE isSingle #-} -isSingle [_] = True -isSingle _ = False - --- | Modify a value inside the state. -modifySlot :: (MonadState s m) => (s -> a) -> (s -> a -> s) -> m () -{-# INLINE modifySlot #-} -modifySlot slot f = modify $ \s -> f s (slot s) - --- | @modifyArray arr i f@ applies the function @f@ to the index @i@ and the --- current value of the array at index @i@, then writes the result into @i@ in --- the array. -modifyArray :: (Monad m, MArray a e m, Ix i) => a i e -> i -> (i -> e -> e) -> m () -{-# INLINE modifyArray #-} -modifyArray arr i f = readArray arr i >>= writeArray arr i . (f i) - --- | Same as @newArray@, but helping along the type checker. -newSTUArray :: (MArray (STUArray s) e (ST s), Ix i) - => (i, i) -> e -> ST s (STUArray s i e) -newSTUArray = newArray - -newSTArray :: (MArray (STArray s) e (ST s), Ix i) - => (i, i) -> e -> ST s (STArray s i e) -newSTArray = newArray - - --- | Count the number of elements in the list that satisfy the predicate. -count :: (a -> Bool) -> [a] -> Int -count p = foldl' f 0 - where f x y | p y = x + 1 - | otherwise = x - --- | /O(1)/ @argmin f x y@ is the argument whose image is least under @f@; if --- the images are equal, returns the first. -argmin :: Ord b => (a -> b) -> a -> a -> a -argmin f x y = if f x <= f y then x else y - --- | /O(length xs)/ @argminimum f xs@ returns the value in @xs@ whose image --- is least under @f@; if @xs@ is empty, throws an error. -argminimum :: Ord b => (a -> b) -> [a] -> a -argminimum f = foldl1' (argmin f) - - --- | Show the value with trace, then return it. Useful because you can wrap --- it around any subexpression to print it when it is forced. -tracing :: (Show a) => a -> a -tracing x = trace (show x) x - --- | Returns a predicate which holds exactly when both of the given predicates --- hold. -p .&&. q = \x -> p x && q x - - --- | Generate a cut using the given UIP node. The cut generated contains --- exactly the (transitively) implied nodes starting with (but not including) --- the UIP on the conflict side, with the rest of the nodes on the reason --- side. -uipCut :: (Graph gr) => - [Lit] -- ^ decision literals - -> FrozenLevelArray - -> gr a b -- ^ conflict graph - -> Graph.Node -- ^ unassigned, implied conflicting node - -> Graph.Node -- ^ a UIP in the conflict graph - -> Cut Set gr a b -uipCut dlits levelArr conflGraph conflNode uip = - Cut { reasonSide = Set.filter (\i -> levelArr!(V $ abs i) > 0) $ - allNodes Set.\\ impliedByUIP - , conflictSide = impliedByUIP - , cutUIP = uip - , cutGraph = conflGraph } - where - -- Transitively implied, and not including the UIP. - impliedByUIP = Set.insert extraNode $ - Set.fromList $ tail $ DFS.reachable uip conflGraph - -- The UIP may not imply the assigned conflict variable which needs to - -- be on the conflict side, unless it's a decision variable or the UIP - -- itself. - extraNode = if L (negate conflNode) `elem` dlits || negate conflNode == uip - then conflNode -- idempotent addition - else negate conflNode - allNodes = Set.fromList $ Graph.nodes conflGraph - - --- | Generate a learned clause from a cut of the graph. Returns a pair of the --- learned clause and the decision level to which to backtrack. -cutLearn :: (Graph gr, Foldable f) => IAssignment -> FrozenLevelArray - -> Cut f gr a b -> (Clause, Int) -cutLearn a levelArr cut = - ( clause - -- The new decision level is the max level of all variables in the - -- clause, excluding the uip (which is always at the current decision - -- level). - , maximum0 (map (levelArr!) . (`without` V (abs $ cutUIP cut)) . map var $ clause) ) - where - -- The clause is composed of the variables on the reason side which have - -- at least one successor on the conflict side. The value of the variable - -- is the negation of its value under the current assignment. - clause = - foldl' (\ls i -> - if any (`elem` conflictSide cut) (Graph.suc (cutGraph cut) i) - then L (negate $ a!(V $ abs i)):ls - else ls) - [] (reasonSide cut) - maximum0 [] = 0 -- maximum0 has 0 as its max for the empty list - maximum0 xs = maximum xs - - --- | Creates the conflict graph, where each node is labeled by its literal and --- level. --- --- Useful for getting pretty graphviz output of a conflict. -mkConflGraph :: DynGraph gr => - IAssignment - -> FrozenLevelArray - -> Map Var Clause - -> [Lit] -- ^ decision lits, in rev. chron. order - -> (Lit, Clause) -- ^ conflict info - -> gr CGNodeAnnot () -mkConflGraph mFr lev reasonMap _dlits (cLit, confl) = - Graph.mkGraph nodes' edges' - where - -- we pick out all the variables from the conflict graph, specially adding - -- both literals of the conflict variable, so that that variable has two - -- nodes in the graph. - nodes' = - ((0, CGNA (L 0) (-1)) :) $ -- lambda node - ((unLit cLit, CGNA cLit (-1)) :) $ - ((negate (unLit cLit), CGNA (negate cLit) (lev!(var cLit))) :) $ - -- annotate each node with its literal and level - map (\v -> (unVar v, CGNA (varToLit v) (lev!v))) $ - filter (\v -> v /= var cLit) $ - toList nodeSet' - - -- node set includes all variables reachable from conflict. This node set - -- construction needs a `seen' set because it might infinite loop - -- otherwise. - (nodeSet', edges') = - mkGr Set.empty (Set.empty, [ (unLit cLit, 0, ()) - , ((negate . unLit) cLit, 0, ()) ]) - [negate cLit, cLit] - varToLit v = (if v `isTrueUnder` mFr then id else negate) $ L (unVar v) - - -- seed with both conflicting literals - mkGr _ ne [] = ne - mkGr (seen :: Set Graph.Node) ne@(nodes, edges) (lit:lits) = - if haveSeen - then mkGr seen ne lits - else newNodes `seq` newEdges `seq` - mkGr seen' (newNodes, newEdges) (lits ++ pred) - where - haveSeen = seen `contains` litNode lit - newNodes = var lit `Set.insert` nodes - newEdges = [ ( litNode (negate x) -- unimplied lits from reasons are - -- complemented - , litNode lit, () ) - | x <- pred ] ++ edges - pred = filterReason $ - if lit == cLit then confl else - Map.findWithDefault [] (var lit) reasonMap `without` lit - filterReason = filter ( ((var lit /=) . var) .&&. - ((<= litLevel lit) . litLevel) ) - seen' = seen `with` litNode lit - litLevel l = if l == cLit then length _dlits else lev!(var l) - litNode l = -- lit to node - if var l == var cLit -- preserve sign of conflicting lit - then unLit l - else (abs . unLit) l - - diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,165 +1,30 @@ - GNU LESSER GENERAL PUBLIC LICENSE - Version 3, 29 June 2007 - - Copyright (C) 2007 Free Software Foundation, Inc. - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - - This version of the GNU Lesser General Public License incorporates -the terms and conditions of version 3 of the GNU General Public -License, supplemented by the additional permissions listed below. - - 0. Additional Definitions. - - As used herein, "this License" refers to version 3 of the GNU Lesser -General Public License, and the "GNU GPL" refers to version 3 of the GNU -General Public License. - - "The Library" refers to a covered work governed by this License, -other than an Application or a Combined Work as defined below. - - An "Application" is any work that makes use of an interface provided -by the Library, but which is not otherwise based on the Library. -Defining a subclass of a class defined by the Library is deemed a mode -of using an interface provided by the Library. - - A "Combined Work" is a work produced by combining or linking an -Application with the Library. The particular version of the Library -with which the Combined Work was made is also called the "Linked -Version". - - The "Minimal Corresponding Source" for a Combined Work means the -Corresponding Source for the Combined Work, excluding any source code -for portions of the Combined Work that, considered in isolation, are -based on the Application, and not on the Linked Version. - - The "Corresponding Application Code" for a Combined Work means the -object code and/or source code for the Application, including any data -and utility programs needed for reproducing the Combined Work from the -Application, but excluding the System Libraries of the Combined Work. - - 1. Exception to Section 3 of the GNU GPL. - - You may convey a covered work under sections 3 and 4 of this License -without being bound by section 3 of the GNU GPL. - - 2. Conveying Modified Versions. - - If you modify a copy of the Library, and, in your modifications, a -facility refers to a function or data to be supplied by an Application -that uses the facility (other than as an argument passed when the -facility is invoked), then you may convey a copy of the modified -version: - - a) under this License, provided that you make a good faith effort to - ensure that, in the event an Application does not supply the - function or data, the facility still operates, and performs - whatever part of its purpose remains meaningful, or - - b) under the GNU GPL, with none of the additional permissions of - this License applicable to that copy. - - 3. Object Code Incorporating Material from Library Header Files. - - The object code form of an Application may incorporate material from -a header file that is part of the Library. You may convey such object -code under terms of your choice, provided that, if the incorporated -material is not limited to numerical parameters, data structure -layouts and accessors, or small macros, inline functions and templates -(ten or fewer lines in length), you do both of the following: - - a) Give prominent notice with each copy of the object code that the - Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the object code with a copy of the GNU GPL and this license - document. - - 4. Combined Works. - - You may convey a Combined Work under terms of your choice that, -taken together, effectively do not restrict modification of the -portions of the Library contained in the Combined Work and reverse -engineering for debugging such modifications, if you also do each of -the following: - - a) Give prominent notice with each copy of the Combined Work that - the Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the Combined Work with a copy of the GNU GPL and this license - document. - - c) For a Combined Work that displays copyright notices during - execution, include the copyright notice for the Library among - these notices, as well as a reference directing the user to the - copies of the GNU GPL and this license document. - - d) Do one of the following: - - 0) Convey the Minimal Corresponding Source under the terms of this - License, and the Corresponding Application Code in a form - suitable for, and under terms that permit, the user to - recombine or relink the Application with a modified version of - the Linked Version to produce a modified Combined Work, in the - manner specified by section 6 of the GNU GPL for conveying - Corresponding Source. - - 1) Use a suitable shared library mechanism for linking with the - Library. A suitable mechanism is one that (a) uses at run time - a copy of the Library already present on the user's computer - system, and (b) will operate properly with a modified version - of the Library that is interface-compatible with the Linked - Version. - - e) Provide Installation Information, but only if you would otherwise - be required to provide such information under section 6 of the - GNU GPL, and only to the extent that such information is - necessary to install and execute a modified version of the - Combined Work produced by recombining or relinking the - Application with a modified version of the Linked Version. (If - you use option 4d0, the Installation Information must accompany - the Minimal Corresponding Source and Corresponding Application - Code. If you use option 4d1, you must provide the Installation - Information in the manner specified by section 6 of the GNU GPL - for conveying Corresponding Source.) - - 5. Combined Libraries. - - You may place library facilities that are a work based on the -Library side by side in a single library together with other library -facilities that are not Applications and are not covered by this -License, and convey such a combined library under terms of your -choice, if you do both of the following: - - a) Accompany the combined library with a copy of the same work based - on the Library, uncombined with any other library facilities, - conveyed under the terms of this License. +Copyright (c) 2009 Denis Bueno +All rights reserved. - b) Give prominent notice with the combined library that part of it - is a work based on the Library, and explaining where to find the - accompanying uncombined form of the same work. +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: - 6. Revised Versions of the GNU Lesser General Public License. + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. - The Free Software Foundation may publish revised and/or new versions -of the GNU Lesser General Public License from time to time. Such new -versions will be similar in spirit to the present version, but may -differ in detail to address new problems or concerns. + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. - Each version is given a distinguishing version number. If the -Library as you received it specifies that a certain numbered version -of the GNU Lesser General Public License "or any later version" -applies to it, you have the option of following the terms and -conditions either of that published version or of any later version -published by the Free Software Foundation. If the Library as you -received it does not specify a version number of the GNU Lesser -General Public License, you may choose any version of the GNU Lesser -General Public License ever published by the Free Software Foundation. + * Neither the name of Denis Bueno nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. - If the Library as you received it specifies that a proxy can decide -whether future versions of the GNU Lesser General Public License shall -apply, that proxy's public statement of acceptance of any version is -permanent authorization for you to choose that version for the -Library. +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -5,18 +5,9 @@ {- 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 . + funsat is free software: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. Copyright 2008 Denis Bueno -} diff --git a/Text/Tabular.hs b/Text/Tabular.hs deleted file mode 100644 --- a/Text/Tabular.hs +++ /dev/null @@ -1,77 +0,0 @@ -{- - This file is part of funsat. - - funsat is free software: you can redistribute it and/or modify - it under the terms of the GNU Lesser General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - funsat is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public License - along with funsat. If not, see . - - Copyright 2008 Denis Bueno --} - -{-| - -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( Table(..), mkTable, combine, unTable ) where - -import Data.List( intercalate ) - -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 - -- string representations of all the elements in the column - -- in which this cell occurs - , cellData :: !a } -- element printed in box of colWidth - -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 :: Table a -> [[a]] -unTable (Table rows) = [ map cellData r | (Row r) <- rows ] - -combine :: (Show a) => Table a -> Table a -> Table a --- slow impl but works -combine t t' = mkTable (unTable t ++ unTable t') - --- returns a list of the widths of each column -colWidths :: (Show a) => [[a]] -> [Int] -colWidths = map (maximum . map (length . show)) . zipn - --- Pretty, columnar output. -instance (Show a) => Show (Table a) where - show (Table rows) = intercalate "\n" $ map showRow rows - where - showRow (Row cols) = intercalate " " $ colStrings - where - colStrings = [ padString (cellWidth c) (show d) - | c@(Cell {cellData=d}) <- cols ] - -padString maxWidth str = str ++ replicate padLen ' ' - where padLen = maxWidth - length str - -zipn xss | any null xss = [] -zipn xss = map head xss : zipn (map tail xss) - - diff --git a/bugs.org b/bugs.org deleted file mode 100644 --- a/bugs.org +++ /dev/null @@ -1,44 +0,0 @@ -#+STARTUP: content hidestars -#+TYP_TODO: DEFECT(d@) FEATURE(f@) VERIFY(v@) | FIXED(@/!) WONTFIX(@/!) POSTPONED(@/!) NOTREPRO(@/!) DUPLICATE(@/!) BYDESIGN(@/!) - - - Top-level headings are modules. - - Under each is a bug entry, initially classified as a defect or feature. - - The DONE states indicate the decision made on the bug. - -* Funsat - :PROPERTIES: - :CATEGORY: Funsat - :END: -** DEFECT resTrace field of resolution trace needn't be there - - State "DEFECT" [2008-10-10 Fri 16:30] \\ - I think it's just keeping around too much info. It doesn't affect the - correctness of the code. - -* fiblib -** FEATURE Implement ST-based fibonacci heap - - State "FEATURE" [2008-10-18 Sat 14:26] -* website - :PROPERTIES: - :CATEGORY: website - :END: - -* bitset - :PROPERTIES: - :CATEGORY: bitset - :END: - -* parse-dimacs - :PROPERTIES: - :CATEGORY: parse-dimacs - :END: -** FIXED Lazy or strict bytestrings? - - State "FIXED" [2008-10-18 Sat 14:18] \\ - Used lazy. - - State "DEFECT" [2008-10-10 Fri 16:25] \\ - I need to settle the question of whether to use lazy or strict bytestrings for - the parser. I need to benchmark it. - -* sat-micro - :PROPERTIES: - :CATEGORY: sat-micro - :END: diff --git a/funsat.cabal b/funsat.cabal --- a/funsat.cabal +++ b/funsat.cabal @@ -1,5 +1,5 @@ Name: funsat -Version: 0.5.2 +Version: 0.6.0 Cabal-Version: >= 1.2 Description: @@ -10,40 +10,41 @@ 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"). + Currently along this theme we provide unsatisfiable core generation (see + "Funsat.Resolution") and a logical circuit interface (see "Funsat.Circuit"). + New in 0.6: circuits and BSD3 license. + Synopsis: A modern DPLL-style SAT solver Homepage: http://github.com/dbueno/funsat Category: Algorithms Stability: beta -License: LGPL +License: BSD3 License-file: LICENSE Author: Denis Bueno Maintainer: Denis Bueno Build-type: Simple -Extra-source-files: README CHANGES bugs.org todo.org +Extra-source-files: README CHANGES Executable funsat Main-is: Main.hs Ghc-options: -funbox-strict-fields - -W - -fwarn-dodgy-imports -fwarn-incomplete-record-updates - -fwarn-unused-binds -fwarn-unused-imports - Extensions: CPP + -Wall -fwarn-tabs + -fno-warn-name-shadowing + -fno-warn-orphans + Extensions: CPP, ScopedTypeVariables CPP-options: -DTESTING - Hs-source-dirs: . tests + Hs-source-dirs: . src tests Other-modules: + Control.Monad.MonadST + Funsat.FastDom + Funsat.Monad + Funsat.Resolution Funsat.Solver Funsat.Types - Funsat.Resolution - Funsat.FastDom Funsat.Utils - Funsat.Monad Text.Tabular - Control.Monad.MonadST Properties Build-Depends: base, @@ -52,33 +53,35 @@ pretty, mtl, array, - QuickCheck, + QuickCheck < 2, parse-dimacs >= 1.2 && < 2, bitset < 1, + bimap >= 0.2 && < 0.3, fgl, time - Library - Exposed-modules: Funsat.Solver - Funsat.Types - Funsat.Resolution + Exposed-modules: Control.Monad.MonadST + Funsat.Circuit Funsat.Monad - Control.Monad.MonadST + Funsat.Resolution + Funsat.Solver + Funsat.Types Text.Tabular Other-modules: Funsat.FastDom Funsat.Utils Ghc-options: -funbox-strict-fields - -W - -fwarn-dodgy-imports -fwarn-incomplete-record-updates - -fwarn-unused-binds -fwarn-unused-imports - Extensions: CPP - Hs-source-dirs: . tests + -Wall -fwarn-tabs + -fno-warn-name-shadowing + -fno-warn-orphans + Extensions: CPP, ScopedTypeVariables + Hs-source-dirs: src Build-Depends: base, containers, pretty, mtl, array, - QuickCheck, + QuickCheck < 2, parse-dimacs >= 1.2 && < 2, bitset < 1, + bimap >= 0.2 && < 0.3, fgl diff --git a/src/Control/Monad/MonadST.hs b/src/Control/Monad/MonadST.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/MonadST.hs @@ -0,0 +1,42 @@ +{-# LANGUAGE MultiParamTypeClasses + ,FunctionalDependencies + ,FlexibleInstances + #-} + + +{- + This file is part of funsat. + + funsat is free software: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. + + Copyright 2008 Denis Bueno +-} + + +-- | Idea from +module Control.Monad.MonadST where + +import Control.Monad.ST +import Data.STRef + +-- | A type class for monads that are able to perform `ST' actions. +class (Monad m) => MonadST s m | m -> s where + liftST :: ST s a -> m a + +instance MonadST s (Control.Monad.ST.ST s) where + liftST = id + +readSTRef :: MonadST s m => STRef s a -> m a +readSTRef = liftST . Data.STRef.readSTRef + +writeSTRef :: MonadST s m => STRef s a -> a -> m () +writeSTRef r x = liftST (Data.STRef.writeSTRef r x) + +newSTRef :: MonadST s m => a -> m (STRef s a) +newSTRef = liftST . Data.STRef.newSTRef + +modifySTRef :: MonadST s m => STRef s a -> (a -> a) -> m () +modifySTRef r f = liftST (Data.STRef.modifySTRef r f) + diff --git a/src/Funsat/Circuit.hs b/src/Funsat/Circuit.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/Circuit.hs @@ -0,0 +1,814 @@ + + +-- | A circuit is a standard one of among many ways of representing a +-- propositional logic formula. This module provides a flexible circuit type +-- class and various representations that admit efficient conversion to funsat +-- CNF. +-- +-- The implementation for this module was adapted from +-- . +module Funsat.Circuit + ( + -- ** Circuit type class + Circuit(..) + , CastCircuit(..) + + -- ** Explicit sharing circuit + , Shared(..) + , FrozenShared(..) + , runShared + , CircuitHash + , falseHash + , trueHash + , CCode(..) + , CMaps(..) + , emptyCMaps + + -- ** Explicit tree circuit + , Tree(..) + , foldTree + + -- *** Circuit simplification + , simplifyTree + + -- ** Explicit graph circuit + , Graph + , runGraph + , shareGraph + , NodeType(..) + , EdgeType(..) + + -- ** Circuit evaluator + , BEnv + , Eval(..) + , runEval + + -- ** Convert circuit to CNF + , CircuitProblem(..) + , toCNF + , projectCircuitSolution + ) +where + +{- + This file is part of funsat. + + funsat is free software: you can redistribute it and/or modify + it under the terms of the GNU Lesser General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + funsat is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public License + along with funsat. If not, see . + + Copyright 2008 Denis Bueno +-} + + +import Control.Monad.Reader +import Control.Monad.State.Lazy hiding ((>=>), forM_) +import Data.Bimap( Bimap ) +import Data.List( nub ) +import Data.Map( Map ) +import Data.Maybe() +import Data.Ord() +import Data.Set( Set ) +import Funsat.Types( CNF(..), Lit(..), Var(..), var, lit, Solution(..), litSign, litAssignment ) +import Prelude hiding( not, and, or ) + +import qualified Data.Bimap as Bimap +import qualified Data.Foldable as Foldable +import qualified Data.Graph.Inductive.Graph as Graph +import qualified Data.Graph.Inductive.Graph as G +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Prelude as Prelude + + + +-- * Circuit representation + + +-- | A class representing a grammar for logical circuits. Default +-- implemenations are indicated. +class Circuit repr where + true :: (Ord var, Show var) => repr var + false :: (Ord var, Show var) => repr var + input :: (Ord var, Show var) => var -> repr var + not :: (Ord var, Show var) => repr var -> repr var + + -- | Defined as @`and' p q = not (not p `or` not q)@. + and :: (Ord var, Show var) => repr var -> repr var -> repr var + and p q = not (not p `or` not q) + + -- | Defined as @`or' p q = not (not p `and` not q)@. + or :: (Ord var, Show var) => repr var -> repr var -> repr var + or p q = not (not p `and` not q) + + -- | If-then-else circuit. @ite c t e@ returns a circuit that evaluates to + -- @t@ when @c@ evaluates to true, and @e@ otherwise. + -- + -- Defined as @(c `and` t) `or` (not c `and` f)@. + ite :: (Ord var, Show var) => repr var -> repr var -> repr var -> repr var + ite c t f = (c `and` t) `or` (not c `and` f) + + -- | Defined as @`onlyif' p q = not p `or` q@. + onlyif :: (Ord var, Show var) => repr var -> repr var -> repr var + onlyif p q = not p `or` q + + -- | Defined as @`iff' p q = (p `onlyif` q) `and` (q `onlyif` p)@. + iff :: (Ord var, Show var) => repr var -> repr var -> repr var + iff p q = (p `onlyif` q) `and` (q `onlyif` p) + + -- | Defined as @`xor' p q = (p `or` q) `and` not (p `and` q)@. + xor :: (Ord var, Show var) => repr var -> repr var -> repr var + xor p q = (p `or` q) `and` not (p `and` q) + +-- | Instances of `CastCircuit' admit converting one circuit representation to +-- another. +class CastCircuit c where + castCircuit :: (Circuit cOut, Ord var, Show var) => c var -> cOut var + + + +-- ** Explicit sharing circuit + +-- The following business is for elimination of common subexpressions from +-- boolean functions. Part of conversion to CNF. + +-- | A `Circuit' constructed using common-subexpression elimination. This is a +-- compact representation that facilitates converting to CNF. See `runShared'. +newtype Shared v = Shared { unShared :: State (CMaps v) CCode } + +-- | A shared circuit that has already been constructed. +data FrozenShared v = FrozenShared !CCode !(CMaps v) deriving (Eq, Show) + +-- | Reify a sharing circuit. +runShared :: Shared v -> FrozenShared v +runShared = uncurry FrozenShared . (`runState` emptyCMaps) . unShared + +instance CastCircuit Shared where + castCircuit = castCircuit . runShared + +instance CastCircuit FrozenShared where + castCircuit (FrozenShared code maps) = go code + where + go (CTrue{}) = true + go (CFalse{}) = false + go c@(CVar{}) = input $ getChildren c (varMap maps) + go c@(CAnd{}) = uncurry and . go2 $ getChildren c (andMap maps) + go c@(COr{}) = uncurry or . go2 $ getChildren c (orMap maps) + go c@(CNot{}) = not . go $ getChildren c (notMap maps) + go c@(CXor{}) = uncurry xor . go2 $ getChildren c (xorMap maps) + go c@(COnlyif{}) = uncurry onlyif . go2 $ getChildren c (onlyifMap maps) + go c@(CIff{}) = uncurry iff . go2 $ getChildren c (iffMap maps) + go c@(CIte{}) = uncurry3 ite . go3 $ getChildren c (iteMap maps) + + go2 = (go `onTup`) + go3 (x, y, z) = (go x, go y, go z) + uncurry3 f (x, y, z) = f x y z + +getChildren :: (Ord v) => CCode -> Bimap CircuitHash v -> v +getChildren code codeMap = + case Bimap.lookup (circuitHash code) codeMap of + Nothing -> findError + Just c -> c + where findError = error $ "getChildren: unknown code: " ++ show code + +-- | 0 is false, 1 is true. Any positive value labels a logical circuit node. +type CircuitHash = Int + +falseHash, trueHash :: CircuitHash +falseHash = 0 +trueHash = 1 + +-- | A `CCode' represents a circuit element for `Shared' circuits. A `CCode' is +-- a flattened tree node which has been assigned a unique number in the +-- corresponding map inside `CMaps', which indicates children, if any. +-- +-- For example, @CAnd i@ has the two children of the tuple @lookup i (andMap +-- cmaps)@ assuming @cmaps :: CMaps v@. +data CCode = CTrue { circuitHash :: !CircuitHash } + | CFalse { circuitHash :: !CircuitHash } + | CVar { circuitHash :: !CircuitHash } + | CAnd { circuitHash :: !CircuitHash } + | COr { circuitHash :: !CircuitHash } + | CNot { circuitHash :: !CircuitHash } + | CXor { circuitHash :: !CircuitHash } + | COnlyif { circuitHash :: !CircuitHash } + | CIff { circuitHash :: !CircuitHash } + | CIte { circuitHash :: !CircuitHash } + deriving (Eq, Ord, Show, Read) + +-- | Maps used to implement the common-subexpression sharing implementation of +-- the `Circuit' class. See `Shared'. +data CMaps v = CMaps + { hashCount :: [CircuitHash] + -- ^ Source of unique IDs used in `Shared' circuit generation. Should not + -- include 0 or 1. + + , varMap :: Bimap CircuitHash v + -- ^ Mapping of generated integer IDs to variables. + + , andMap :: Bimap CircuitHash (CCode, CCode) + , orMap :: Bimap CircuitHash (CCode, CCode) + , notMap :: Bimap CircuitHash CCode + , xorMap :: Bimap CircuitHash (CCode, CCode) + , onlyifMap :: Bimap CircuitHash (CCode, CCode) + , iffMap :: Bimap CircuitHash (CCode, CCode) + , iteMap :: Bimap CircuitHash (CCode, CCode, CCode) } + deriving (Eq, Show) + +-- | A `CMaps' with an initial `hashCount' of 2. +emptyCMaps :: CMaps v +emptyCMaps = CMaps + { hashCount = [2 ..] + , varMap = Bimap.empty + , andMap = Bimap.empty + , orMap = Bimap.empty + , notMap = Bimap.empty + , xorMap = Bimap.empty + , onlyifMap = Bimap.empty + , iffMap = Bimap.empty + , iteMap = Bimap.empty } + +-- | Find key mapping to given value. +lookupv :: Ord v => v -> Bimap Int v -> Maybe Int +lookupv = Bimap.lookupR + +-- prj: "projects relevant map out of state" +-- upd: "stores new map back in state" +recordC :: (Ord a) => + (CircuitHash -> b) + -> (CMaps v -> Bimap Int a) -- ^ prj + -> (CMaps v -> Bimap Int a -> CMaps v) -- ^ upd + -> a + -> State (CMaps v) b +recordC _ _ _ x | x `seq` False = undefined +recordC cons prj upd x = do + s <- get + c:cs <- gets hashCount + maybe (do let s' = upd (s{ hashCount = cs }) + (Bimap.insert c x (prj s)) + put s' + -- trace "updating map" (return ()) + return (cons c)) + (return . cons) $ lookupv x (prj s) + +instance Circuit Shared where + false = Shared . return $ CFalse falseHash + true = Shared . return $ CTrue trueHash + input v = Shared $ recordC CVar varMap (\s e -> s{ varMap = e }) v + and e1 e2 = Shared $ do + hl <- unShared e1 + hr <- unShared e2 + recordC CAnd andMap (\s e -> s{ andMap = e}) (hl, hr) + or e1 e2 = Shared $ do + hl <- unShared e1 + hr <- unShared e2 + recordC COr orMap (\s e -> s{ orMap = e }) (hl, hr) + not e = Shared $ do + h <- unShared e + recordC CNot notMap (\s e' -> s{ notMap = e' }) h + xor l r = Shared $ do + hl <- unShared l ; hr <- unShared r + recordC CXor xorMap (\s e' -> s{ xorMap = e' }) (hl, hr) + iff l r = Shared $ do + hl <- unShared l ; hr <- unShared r + recordC CIff iffMap (\s e' -> s{ iffMap = e' }) (hl, hr) + onlyif l r = Shared $ do + hl <- unShared l ; hr <- unShared r + recordC COnlyif onlyifMap (\s e' -> s{ onlyifMap = e' }) (hl, hr) + ite x t e = Shared $ do + hx <- unShared x + ht <- unShared t ; he <- unShared e + recordC CIte iteMap (\s e' -> s{ iteMap = e' }) (hx, ht, he) + + +{- +-- | An And-Inverter graph edge may complement its input. +data AIGEdge = AIGPos | AIGNeg +type AIGGr g v = g (Maybe v) AIGEdge +-- | * 0 is the output. +data AndInverterGraph gr v = AIG + { aigGraph :: AIGGr gr v + -- ^ Node 0 is the output node. Node 1 is hardwired with a 'true' input. + -- The edge from Node 1 to 0 may or may not be complemented. + + , aigInputs :: [G.Node] + -- ^ Node 1 is always an input set to true. + } + +instance (G.Graph gr, Show v, Ord v) => Monoid (AndInverterGraph gr v) where + mempty = true + mappend a1 a2 = + AIG{ aigGraph = mergedGraph + , aigInputs = nub (aigInputs a1 ++ aigInputs a2) } + where + mergedGraph = G.mkGraph + (G.labNodes (aigGraph a1) ++ G.labNodes (aigGraph a2)) + (G.labEdges (aigGraph a1) ++ G.labEdges (aigGraph a2)) + +instance (G.Graph gr) => Circuit (AndInverterGraph gr) where + true = AIG{ aigGraph = G.mkGraph [(0,Nothing), (1,Nothing)] [(1, 0, AIGPos)] + , aigInputs = [1] } + + false = AIG{ aigGraph = G.mkGraph [(0,Nothing), (1,Nothing)] [(1, 0, AIGNeg)] + , aigInputs = [1] } + + input v = let [n] = G.newNodes 1 true + in AIG{ aigGraph = G.insNode (n, Just v) true + , aigInputs `= [n, 1] } +-} + +-- and l r = let g' = l `mappend` r +-- [n] = G.newNodes 1 g' +-- in G.insNode (n, Nothing) + +-- ** Explicit tree circuit + +-- | Explicit tree representation, which is a generic description of a circuit. +-- This representation enables a conversion operation to any other type of +-- circuit. Trees evaluate from variable values at the leaves to the root. +data Tree v = TTrue + | TFalse + | TLeaf v + | TNot (Tree v) + | TAnd (Tree v) (Tree v) + | TOr (Tree v) (Tree v) + | TXor (Tree v) (Tree v) + | TIff (Tree v) (Tree v) + | TOnlyIf (Tree v) (Tree v) + | TIte (Tree v) (Tree v) (Tree v) + deriving (Show, Eq, Ord) + +foldTree :: (t -> v -> t) -> t -> Tree v -> t +foldTree _ i TTrue = i +foldTree _ i TFalse = i +foldTree f i (TLeaf v) = f i v +foldTree f i (TAnd t1 t2) = foldTree f (foldTree f i t1) t2 +foldTree f i (TOr t1 t2) = foldTree f (foldTree f i t1) t2 +foldTree f i (TNot t) = foldTree f i t +foldTree f i (TXor t1 t2) = foldTree f (foldTree f i t1) t2 +foldTree f i (TIff t1 t2) = foldTree f (foldTree f i t1) t2 +foldTree f i (TOnlyIf t1 t2) = foldTree f (foldTree f i t1) t2 +foldTree f i (TIte x t e) = foldTree f (foldTree f (foldTree f i x) t) e + +instance Circuit Tree where + true = TTrue + false = TFalse + input = TLeaf + and = TAnd + or = TOr + not = TNot + xor = TXor + iff = TIff + onlyif = TOnlyIf + ite = TIte + +instance CastCircuit Tree where + castCircuit TTrue = true + castCircuit TFalse = false + castCircuit (TLeaf l) = input l + castCircuit (TAnd t1 t2) = and (castCircuit t1) (castCircuit t2) + castCircuit (TOr t1 t2) = or (castCircuit t1) (castCircuit t2) + castCircuit (TXor t1 t2) = xor (castCircuit t1) (castCircuit t2) + castCircuit (TNot t) = not (castCircuit t) + castCircuit (TIff t1 t2) = iff (castCircuit t1) (castCircuit t2) + castCircuit (TOnlyIf t1 t2) = onlyif (castCircuit t1) (castCircuit t2) + castCircuit (TIte x t e) = ite (castCircuit x) (castCircuit t) (castCircuit e) + +-- ** Circuit evaluator + +type BEnv v = Map v Bool + +-- | A circuit evaluator, that is, a circuit represented as a function from +-- variable values to booleans. +newtype Eval v = Eval { unEval :: BEnv v -> Bool } + +-- | Evaluate a circuit given inputs. +runEval :: BEnv v -> Eval v -> Bool +runEval = flip unEval + +instance Circuit Eval where + true = Eval $ const True + false = Eval $ const False + input v = Eval $ \env -> + Map.findWithDefault + (error $ "Eval: no such var: " ++ show v + ++ " in " ++ show env) + v env + and c1 c2 = Eval (\env -> unEval c1 env && unEval c2 env) + or c1 c2 = Eval (\env -> unEval c1 env || unEval c2 env) + not c = Eval (\env -> Prelude.not $ unEval c env) + +-- ** Graph circuit + +-- | A circuit type that constructs a `G.Graph' representation. This is useful +-- for visualising circuits, for example using the @graphviz@ package. +newtype Graph v = Graph + { unGraph :: State Graph.Node (Graph.Node, + [Graph.LNode (NodeType v)], + [Graph.LEdge EdgeType]) } + +-- | Node type labels for graphs. +data NodeType v = NInput v + | NTrue + | NFalse + | NAnd + | NOr + | NNot + | NXor + | NIff + | NOnlyIf + | NIte + deriving (Eq, Ord, Show, Read) + +data EdgeType = ETest -- ^ the edge is the condition for an `ite' element + | EThen -- ^ the edge is the /then/ branch for an `ite' element + | EElse -- ^ the edge is the /else/ branch for an `ite' element + | EVoid -- ^ no special annotation + deriving (Eq, Ord, Show, Read) + +runGraph :: (G.DynGraph gr) => Graph v -> gr (NodeType v) EdgeType +runGraph graphBuilder = + let (_, nodes, edges) = evalState (unGraph graphBuilder) 1 + in Graph.mkGraph nodes edges + +instance Circuit Graph where + input v = Graph $ do + n <- newNode + return $ (n, [(n, NInput v)], []) + + true = Graph $ do + n <- newNode + return $ (n, [(n, NTrue)], []) + + false = Graph $ do + n <- newNode + return $ (n, [(n, NFalse)], []) + + not gs = Graph $ do + (node, nodes, edges) <- unGraph gs + n <- newNode + return (n, (n, NNot) : nodes, (node, n, EVoid) : edges) + + and = binaryNode NAnd + or = binaryNode NOr + xor = binaryNode NXor + iff = binaryNode NIff + onlyif = binaryNode NOnlyIf + ite x t e = Graph $ do + (xNode, xNodes, xEdges) <- unGraph x + (tNode, tNodes, tEdges) <- unGraph t + (eNode, eNodes, eEdges) <- unGraph e + n <- newNode + return (n, (n, NIte) : xNodes ++ tNodes ++ eNodes + , (xNode, n, ETest) : (tNode, n, EThen) : (eNode, n, EElse) + : xEdges ++ tEdges ++ eEdges) + +binaryNode :: NodeType v -> Graph v -> Graph v -> Graph v +{-# INLINE binaryNode #-} +binaryNode ty l r = Graph $ do + (lNode, lNodes, lEdges) <- unGraph l + (rNode, rNodes, rEdges) <- unGraph r + n <- newNode + return (n, (n, ty) : lNodes ++ rNodes, + (lNode, n, EVoid) : (rNode, n, EVoid) : lEdges ++ rEdges) + + +newNode :: State Graph.Node Graph.Node +newNode = do i <- get ; put (succ i) ; return i + + +{- +defaultNodeAnnotate :: (Show v) => LNode (FrozenShared v) -> [GraphViz.Attribute] +defaultNodeAnnotate (_, FrozenShared (output, cmaps)) = go output + where + go CTrue{} = "true" + go CFalse{} = "false" + go (CVar _ i) = show $ extract i varMap + go (CNot{}) = "NOT" + go (CAnd{hlc=h}) = maybe "AND" goHLC h + go (COr{hlc=h}) = maybe "OR" goHLC h + + goHLC (Xor{}) = "XOR" + goHLC (Onlyif{}) = go (output{ hlc=Nothing }) + goHLC (Iff{}) = "IFF" + + extract code f = + IntMap.findWithDefault (error $ "shareGraph: unknown code: " ++ show code) + code + (f cmaps) + +defaultEdgeAnnotate = undefined + +dotGraph :: (Graph gr) => gr (FrozenShared v) (FrozenShared v) -> DotGraph +dotGraph g = graphToDot g defaultNodeAnnotate defaultEdgeAnnotate + +-} + +-- | Given a frozen shared circuit, construct a `G.DynGraph' that exactly +-- represents it. Useful for debugging constraints generated as `Shared' +-- circuits. +shareGraph :: (G.DynGraph gr, Eq v, Show v) => + FrozenShared v -> gr (FrozenShared v) (FrozenShared v) +shareGraph (FrozenShared output cmaps) = + (`runReader` cmaps) $ do + (_, nodes, edges) <- go output + return $ Graph.mkGraph (nub nodes) (nub edges) + where + -- Invariant: The returned node is always a member of the returned list of + -- nodes. Returns: (node, node-list, edge-list). + go c@(CVar i) = return (i, [(i, frz c)], []) + go c@(CTrue i) = return (i, [(i, frz c)], []) + go c@(CFalse i) = return (i, [(i, frz c)], []) + go c@(CNot i) = do + (child, nodes, edges) <- extract i notMap >>= go + return (i, (i, frz c) : nodes, (child, i, frz c) : edges) + go c@(CAnd i) = extract i andMap >>= tupM2 go >>= addKids c + go c@(COr i) = extract i orMap >>= tupM2 go >>= addKids c + go c@(CXor i) = extract i xorMap >>= tupM2 go >>= addKids c + go c@(COnlyif i) = extract i onlyifMap >>= tupM2 go >>= addKids c + go c@(CIff i) = extract i iffMap >>= tupM2 go >>= addKids c + go c@(CIte i) = do (x, y, z) <- extract i iteMap + ( (cNode, cNodes, cEdges) + ,(tNode, tNodes, tEdges) + ,(eNode, eNodes, eEdges)) <- liftM3 (,,) (go x) (go y) (go z) + return (i, (i, frz c) : cNodes ++ tNodes ++ eNodes + ,(cNode, i, frz c) + : (tNode, i, frz c) + : (eNode, i, frz c) + : cEdges ++ tEdges ++ eEdges) + + + addKids ccode ((lNode, lNodes, lEdges), (rNode, rNodes, rEdges)) = + let i = circuitHash ccode + in return (i, (i, frz ccode) : lNodes ++ rNodes, + (lNode, i, frz ccode) : (rNode, i, frz ccode) : lEdges ++ rEdges) + tupM2 f (x, y) = liftM2 (,) (f x) (f y) + frz ccode = FrozenShared ccode cmaps + extract code f = do + maps <- ask + let lookupError = error $ "shareGraph: unknown code: " ++ show code + case Bimap.lookup code (f maps) of + Nothing -> lookupError + Just x -> return x + + +-- ** Circuit simplification + +-- | Performs obvious constant propagations. +simplifyTree :: Tree v -> Tree v +simplifyTree l@(TLeaf _) = l +simplifyTree TFalse = TFalse +simplifyTree TTrue = TTrue +simplifyTree (TNot t) = + let t' = simplifyTree t + in case t' of + TTrue -> TFalse + TFalse -> TTrue + _ -> TNot t' +simplifyTree (TAnd l r) = + let l' = simplifyTree l + r' = simplifyTree r + in case l' of + TFalse -> TFalse + TTrue -> case r' of + TTrue -> TTrue + TFalse -> TFalse + _ -> r' + _ -> case r' of + TTrue -> l' + TFalse -> TFalse + _ -> TAnd l' r' +simplifyTree (TOr l r) = + let l' = simplifyTree l + r' = simplifyTree r + in case l' of + TFalse -> r' + TTrue -> TTrue + _ -> case r' of + TTrue -> TTrue + TFalse -> l' + _ -> TOr l' r' +simplifyTree (TXor l r) = + let l' = simplifyTree l + r' = simplifyTree r + in case l' of + TFalse -> r' + TTrue -> case r' of + TFalse -> TTrue + TTrue -> TFalse + _ -> TNot r' + _ -> TXor l' r' +simplifyTree (TIff l r) = + let l' = simplifyTree l + r' = simplifyTree r + in case l' of + TFalse -> case r' of + TFalse -> TTrue + TTrue -> TFalse + _ -> l' `TIff` r' + TTrue -> case r' of + TTrue -> TTrue + TFalse -> TFalse + _ -> l' `TIff` r' + _ -> l' `TIff` r' +simplifyTree (l `TOnlyIf` r) = + let l' = simplifyTree l + r' = simplifyTree r + in case l' of + TFalse -> TTrue + TTrue -> r' + _ -> l' `TOnlyIf` r' +simplifyTree (TIte x t e) = + let x' = simplifyTree x + t' = simplifyTree t + e' = simplifyTree e + in case x' of + TTrue -> t' + TFalse -> e' + _ -> TIte x' t' e' + + +-- ** Convert circuit to CNF + +-- this data is private to toCNF. +data CNFResult = CP !Lit !(Set (Set Lit)) +data CNFState = CNFS{ toCnfVars :: [Var] + -- ^ infinite fresh var source, starting at 1 + , toCnfMap :: Bimap Var CCode + -- ^ record var mapping + } +emptyCNFState :: CNFState +emptyCNFState = CNFS{ toCnfVars = [V 1 ..] + , toCnfMap = Bimap.empty } + +-- retrieve and create (if necessary) a cnf variable for the given ccode. +--findVar :: (MonadState CNFState m) => CCode -> m Lit +findVar ccode = do + m <- gets toCnfMap + v:vs <- gets toCnfVars + case Bimap.lookupR ccode m of + Nothing -> do modify $ \s -> s{ toCnfMap = Bimap.insert v ccode m + , toCnfVars = vs } + return . lit $ v + Just v' -> return . lit $ v' + +-- | A circuit problem packages up the CNF corresponding to a given +-- `FrozenShared' circuit, and the mapping between the variables in the CNF and +-- the circuit elements of the circuit. +data CircuitProblem v = CircuitProblem + { problemCnf :: CNF + , problemCircuit :: FrozenShared v + , problemCodeMap :: Bimap Var CCode } + +-- | Produces a CNF formula that is satisfiable if and only if the input circuit +-- is satisfiable. /Note that it does not produce an equivalent CNF formula./ +-- It is not equivalent in general because the transformation introduces +-- variables into the CNF which were not present as circuit inputs. (Variables +-- in the CNF correspond to circuit elements.) Returns equisatisfiable CNF +-- along with the frozen input circuit, and the mapping between the variables of +-- the CNF and the circuit elements. +-- +-- The implementation uses the Tseitin transformation, to guarantee that the +-- output CNF formula is linear in the size of the circuit. Contrast this with +-- the naive DeMorgan-laws transformation which produces an exponential-size CNF +-- formula. +toCNF :: (Ord v, Show v) => FrozenShared v -> CircuitProblem v +toCNF cIn = + let c@(FrozenShared sharedCircuit circuitMaps) = + runShared . removeComplex $ cIn + (cnf, m) = ((`runReader` circuitMaps) . (`runStateT` emptyCNFState)) $ do + (CP l theClauses) <- toCNF' sharedCircuit + return $ Set.insert (Set.singleton l) theClauses + in CircuitProblem + { problemCnf = CNF { numVars = Set.fold max 1 + . Set.map (Set.fold max 1) + . Set.map (Set.map (unVar . var)) + $ cnf + , numClauses = Set.size cnf + , clauses = Set.map Foldable.toList cnf } + , problemCircuit = c + , problemCodeMap = toCnfMap m } + where + -- Returns (CP l c) where {l} U c is CNF equisatisfiable with the input + -- circuit. Note that CNF conversion only has cases for And, Or, Not, True, + -- False, and Var circuits. We therefore remove the complex circuit before + -- passing stuff to this function. + toCNF' c@(CVar{}) = do l <- findVar c + return (CP l Set.empty) + toCNF' c@(CTrue{}) = do + l <- findVar c + return (CP l (Set.singleton . Set.singleton $ l)) + toCNF' c@(CFalse{}) = do + l <- findVar c + return (CP l (Set.fromList [Set.singleton (negate l)])) + +-- -- x <-> -y +-- -- <-> (-x, -y) & (y, x) + toCNF' c@(CNot i) = do + notLit <- findVar c + eTree <- extract i notMap + (CP eLit eCnf) <- toCNF' eTree + return + (CP notLit + (Set.fromList [ Set.fromList [negate notLit, negate eLit] + , Set.fromList [eLit, notLit] ] + `Set.union` eCnf)) + +-- -- x <-> (y | z) +-- -- <-> (-y, x) & (-z, x) & (-x, y, z) + toCNF' c@(COr i) = do + orLit <- findVar c + (l, r) <- extract i orMap + (CP lLit lCnf) <- toCNF' l + (CP rLit rCnf) <- toCNF' r + return + (CP orLit + (Set.fromList [ Set.fromList [negate lLit, orLit] + , Set.fromList [negate rLit, orLit] + , Set.fromList [negate orLit, lLit, rLit] ] + `Set.union` lCnf `Set.union` rCnf)) + +-- -- x <-> (y & z) +-- -- <-> (-x, y), (-x, z) & (-y, -z, x) + toCNF' c@(CAnd i) = do + andLit <- findVar c + (l, r) <- extract i andMap + (CP lLit lCnf) <- toCNF' l + (CP rLit rCnf) <- toCNF' r + return + (CP andLit + (Set.fromList [ Set.fromList [negate andLit, lLit] + , Set.fromList [negate andLit, rLit] + , Set.fromList [negate lLit, negate rLit, andLit] ] + `Set.union` lCnf `Set.union` rCnf)) + + toCNF' c = do + m <- ask + error $ "toCNF' bug: unknown code: " ++ show c + ++ " with maps:\n" ++ show m + + + extract code f = do + m <- asks f + case Bimap.lookup code m of + Nothing -> error $ "toCNF: unknown code: " ++ show code + Just x -> return x + +-- | Returns an equivalent circuit with no iff, xor, onlyif, and ite nodes. +removeComplex :: (Ord v, Show v, Circuit c) => FrozenShared v -> c v +removeComplex (FrozenShared code maps) = go code + where + go (CTrue{}) = true + go (CFalse{}) = false + go c@(CVar{}) = input $ getChildren c (varMap maps) + go c@(COr{}) = uncurry or (go `onTup` getChildren c (orMap maps)) + go c@(CAnd{}) = uncurry and (go `onTup` getChildren c (andMap maps)) + go c@(CNot{}) = not . go $ getChildren c (notMap maps) + go c@(CXor{}) = + let (l, r) = go `onTup` getChildren c (xorMap maps) + in (l `or` r) `and` not (l `and` r) + go c@(COnlyif{}) = + let (p, q) = go `onTup` getChildren c (onlyifMap maps) + in not p `or` q + go c@(CIff{}) = + let (p, q) = go `onTup` getChildren c (iffMap maps) + in (not p `or` q) `and` (not q `or` p) + go c@(CIte{}) = + let (cc, tc, ec) = getChildren c (iteMap maps) + (cond, t, e) = (go cc, go tc, go ec) + in (cond `and` t) `or` (not cond `and` e) + +onTup :: (a -> b) -> (a, a) -> (b, b) +onTup f (x, y) = (f x, f y) + +-- | Projects a funsat `Solution' back into the original circuit space, +-- returning a boolean environment containing an assignment of all circuit +-- inputs to true and false. +projectCircuitSolution :: (Ord v) => Solution -> CircuitProblem v -> BEnv v +projectCircuitSolution sol pblm = case sol of + Sat lits -> projectLits lits + Unsat lits -> projectLits lits + where + projectLits lits = + -- only the lits whose vars are (varMap maps) go to benv + foldl (\m l -> case Bimap.lookup (litHash l) (varMap maps) of + Nothing -> m + Just v -> Map.insert v (litSign l) m) + Map.empty + (litAssignment lits) + where + (FrozenShared _ maps) = problemCircuit pblm + litHash l = case Bimap.lookup (var l) (problemCodeMap pblm) of + Nothing -> error $ "projectSolution: unknown lit: " ++ show l + Just code -> circuitHash code + + diff --git a/src/Funsat/FastDom.hs b/src/Funsat/FastDom.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/FastDom.hs @@ -0,0 +1,122 @@ + +-- From a patch to the dominators lib on ghc's trac; should be incorporated +-- into fgl in GHC sooner or later. + +-- | Find Dominators of a graph. +-- +-- Author: Bertram Felgenhauer +-- +-- Implementation based on +-- Keith D. Cooper, Timothy J. Harvey, Ken Kennedy, +-- ''A Simple, Fast Dominance Algorithm'', +-- (http://citeseer.ist.psu.edu/cooper01simple.html) +module Funsat.FastDom + ( dom + , iDom ) where + +import Data.Graph.Inductive.Graph +import Data.Graph.Inductive.Query.DFS +import Data.Tree (Tree(..)) +import qualified Data.Tree as T +import Data.Array +import Data.IntMap (IntMap) +import qualified Data.IntMap as I + +-- | return immediate dominators for each node of a graph, given a root +iDom :: Graph gr => gr a b -> Node -> [(Node,Node)] +iDom g root = let (result, toNode, _) = idomWork g root + in map (\(a, b) -> (toNode ! a, toNode ! b)) (assocs result) + + +-- | return the set of dominators of the nodes of a graph, given a root +dom :: Graph gr => gr a b -> Node -> [(Node,[Node])] +dom g root = let + (iDom, toNode, fromNode) = idomWork g root + dom' = getDom toNode iDom + nodes' = nodes g + rest = I.keys (I.filter (-1 ==) fromNode) + in + [(toNode ! i, dom' ! i) | i <- range (bounds dom')] ++ + [(n, nodes') | n <- rest] + +-- internal node type +type Node' = Int +-- array containing the immediate dominator of each node, or an approximation +-- thereof. the dominance set of a node can be found by taking the union of +-- {node} and the dominance set of its immediate dominator. +type IDom = Array Node' Node' +-- array containing the list of predecessors of each node +type Preds = Array Node' [Node'] +-- arrays for translating internal nodes back to graph nodes and back +type ToNode = Array Node' Node +type FromNode = IntMap Node' + +idomWork :: Graph gr => gr a b -> Node -> (IDom, ToNode, FromNode) +idomWork g root = let + -- use depth first tree from root do build the first approximation + trees@(~[tree]) = dff [root] g + -- relabel the tree so that paths from the root have increasing nodes + (s, ntree) = numberTree 0 tree + -- the approximation iDom0 just maps each node to its parent + iDom0 = array (1, s-1) (tail $ treeEdges (-1) ntree) + -- fromNode translates graph nodes to relabeled (internal) nodes + fromNode = I.unionWith const (I.fromList (zip (T.flatten tree) (T.flatten ntree))) (I.fromList (zip (nodes g) (repeat (-1)))) + -- toNode translates internal nodes to graph nodes + toNode = array (0, s-1) (zip (T.flatten ntree) (T.flatten tree)) + preds = array (1, s-1) [(i, filter (/= -1) (map (fromNode I.!) + (pre g (toNode ! i)))) | i <- [1..s-1]] + -- iteratively improve the approximation to find iDom. + iDom = fixEq (refineIDom preds) iDom0 + in + if null trees then error "Dominators.idomWork: root not in graph" + else (iDom, toNode, fromNode) +-- for each node in iDom, find the intersection of all its predecessor's +-- dominating sets, and update iDom accordingly. +refineIDom :: Preds -> IDom -> IDom +refineIDom preds iDom = fmap (foldl1 (intersect iDom)) preds + +-- find the intersection of the two given dominance sets. +intersect :: IDom -> Node' -> Node' -> Node' +intersect iDom a b = case a `compare` b of + LT -> intersect iDom a (iDom ! b) + EQ -> a + GT -> intersect iDom (iDom ! a) b + +-- convert an IDom to dominance sets. we translate to graph nodes here +-- because mapping later would be more expensive and lose sharing. +getDom :: ToNode -> IDom -> Array Node' [Node] +getDom toNode iDom = let + res = array (0, snd (bounds iDom)) ((0, [toNode ! 0]) : + [(i, toNode ! i : res ! (iDom ! i)) | i <- range (bounds iDom)]) + in + res +-- relabel tree, labeling vertices with consecutive numbers in depth first order +numberTree :: Node' -> Tree a -> (Node', Tree Node') +numberTree n (Node _ ts) = let (n', ts') = numberForest (n+1) ts + in (n', Node n ts') + +-- same as numberTree, for forests. +numberForest :: Node' -> [Tree a] -> (Node', [Tree Node']) +numberForest n [] = (n, []) +numberForest n (t:ts) = let (n', t') = numberTree n t + (n'', ts') = numberForest n' ts + in (n'', t':ts') + +-- return the edges of the tree, with an added dummy root node. +treeEdges :: a -> Tree a -> [(a,a)] +treeEdges a (Node b ts) = (b,a) : concatMap (treeEdges b) ts + +-- find a fixed point of f, iteratively +fixEq :: Eq a => (a -> a) -> a -> a +fixEq f v | v' == v = v + | otherwise = fixEq f v' + where v' = f v + +{- +:m +Data.Graph.Inductive +let g0 = mkGraph [(i,()) | i <- [0..4]] [(a,b,()) | (a,b) <- [(0,1),(1,2),(0,3),(3,2),(4,0)]] :: Gr () () +let g1 = mkGraph [(i,()) | i <- [0..4]] [(a,b,()) | (a,b) <- [(0,1),(1,2),(2,3),(1,3),(3,4)]] :: Gr () () +let g2,g3,g4 :: Int -> Gr () (); g2 n = mkGraph [(i,()) | i <- [0..n-1]] ([(a,a+1,()) | a <- [0..n-2]] ++ [(a,a+2,()) | a <- [0..n-3]]); g3 n =mkGraph [(i,()) | i <- [0..n-1]] ([(a,a+2,()) | a <- [0..n-3]] ++ [(a,a+1,()) | a <- [0..n-2]]); g4 n =mkGraph [(i,()) | i <- [0..n-1]] ([(a+2,a,()) | a <- [0..n-3]] ++ [(a+1,a,()) | a <- [0..n-2]]) +:m -Data.Graph.Inductive +-} + diff --git a/src/Funsat/Monad.hs b/src/Funsat/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/Monad.hs @@ -0,0 +1,94 @@ +{-# LANGUAGE PolymorphicComponents + ,MultiParamTypeClasses + ,FunctionalDependencies + ,FlexibleInstances + #-} + +{- + This file is part of funsat. + + funsat is free software: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. + + Copyright 2008 Denis Bueno +-} + + +{-| + +The main SAT solver monad. Embeds `ST'. See type `SSTErrMonad', which stands +for ''State ST Error Monad''. + +-} +module Funsat.Monad + ( liftST + , runSSTErrMonad + , evalSSTErrMonad + , SSTErrMonad ) + where +import Control.Monad.Error +import Control.Monad.ST.Strict +import Control.Monad.State.Class +import Control.Monad.MonadST + + +instance MonadST s (SSTErrMonad e st s) where + liftST = dpllST + +-- | Perform an @ST@ action in the DPLL monad. +dpllST :: ST s a -> SSTErrMonad e st s a +{-# INLINE dpllST #-} +dpllST st = SSTErrMonad (\k s -> st >>= \x -> k x s) + +-- | @runSSTErrMonad m s@ executes a `SSTErrMonad' action with initial state @s@ +-- until an error occurs or a result is returned. +runSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> (st -> ST s (Either e a, st)) +runSSTErrMonad m = unSSTErrMonad m (\x s -> return (return x, s)) + +evalSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> st -> ST s (Either e a) +evalSSTErrMonad m s = do (result, _) <- runSSTErrMonad m s + return result + +-- | @SSTErrMonad e st s a@: the error type @e@, state type @st@, @ST@ thread +-- @s@ and result type @a@. +-- +-- This is a monad embedding @ST@ and supporting error handling and state +-- threading. It uses CPS to avoid checking `Left' and `Right' for every +-- `>>='; instead only checks on `catchError'. Idea adapted from +-- . +newtype SSTErrMonad e st s a = + SSTErrMonad { unSSTErrMonad :: forall r. (a -> (st -> ST s (Either e r, st))) + -> (st -> ST s (Either e r, st)) } + +instance Monad (SSTErrMonad e st s) where + return x = SSTErrMonad ($ x) + (>>=) = bindSSTErrMonad + +bindSSTErrMonad :: SSTErrMonad e st s a -> (a -> SSTErrMonad e st s b) + -> SSTErrMonad e st s b +{-# INLINE bindSSTErrMonad #-} +bindSSTErrMonad m f = + {-# SCC "bindSSTErrMonad" #-} + SSTErrMonad (\k -> unSSTErrMonad m (\a -> unSSTErrMonad (f a) k)) + +instance MonadState st (SSTErrMonad e st s) where + get = SSTErrMonad (\k s -> k s s) + put s' = SSTErrMonad (\k _ -> k () s') + +instance (Error e) => MonadError e (SSTErrMonad e st s) where + throwError err = -- throw away continuation + SSTErrMonad (\_ s -> return (Left err, s)) + catchError action handler = {-# SCC "catchErrorSSTErrMonad" #-} SSTErrMonad + (\k s -> do (x, s') <- runSSTErrMonad action s + case x of + Left error -> unSSTErrMonad (handler error) k s' + Right result -> k result s') + +instance (Error e) => MonadPlus (SSTErrMonad e st s) where + mzero = SSTErrMonad (\_ s -> return (Left noMsg, s)) + mplus m n = SSTErrMonad (\k s -> + do (r, s') <- runSSTErrMonad m s + case r of + Left _ -> unSSTErrMonad n k s' + Right x -> k x s') diff --git a/src/Funsat/Resolution.hs b/src/Funsat/Resolution.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/Resolution.hs @@ -0,0 +1,284 @@ + +{- + This file is part of funsat. + + funsat is free software: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. + + Copyright 2008 Denis Bueno +-} + +-- | Generates and checks a resolution proof of `Funsat.Types.Unsat' from a +-- resolution trace of a SAT solver (`Funsat.Solver.solve' will generate this +-- trace). As a side effect of this process an /unsatisfiable core/ is +-- generated from the resolution trace. This core is a (hopefully small) subset +-- of the input clauses which is still unsatisfiable. Intuitively, it a concise +-- reason why the problem is unsatisfiable. +-- +-- The resolution trace checker is based on the implementation from the paper +-- ''Validating SAT Solvers Using an Independent Resolution-Based Checker: +-- Practical Implementations and Other Applications'' by Lintao Zhang and Sharad +-- Malik. Unsatisfiable cores are discussed in the paper ''Extracting Small +-- Unsatisfiable Cores from Unsatisfiable Boolean Formula'' by Zhang and Malik. +-- +-- +module Funsat.Resolution + ( -- * Interface + genUnsatCore + , checkDepthFirst + -- * Data Types + , ResolutionTrace(..) + , initResolutionTrace + , ResolutionError(..) + , UnsatisfiableCore ) + 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, getUnit, isFalseUnder ) + + +-- IDs = Ints +-- Lits = Lits + + +-- | A resolution trace records how the SAT solver proved the original CNF +-- formula unsatisfiable. +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 :: ClauseId -> IAssignment -> ResolutionTrace +initResolutionTrace finalClauseId finalAssignment = ResolutionTrace + { traceFinalClauseId = finalClauseId + , traceFinalAssignment = finalAssignment + , traceSources = Map.empty + , traceOriginalClauses = Map.empty + , traceAntecedents = Map.empty } + +-- | 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) + +-- | Check the given resolution trace of a (putatively) unsatisfiable formula. +-- If the result is `ResolutionError', the proof trace has failed to establish +-- the unsatisfiability of the formula. Otherwise, an unsatisfiable core of +-- clauses is returned. +-- +-- This function simply calls `checkDepthFirst'. +genUnsatCore :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore +genUnsatCore = checkDepthFirst + +-- | 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 = 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 -> ClauseId -> [ClauseId] -> ResM Clause +recursiveBuildIds clauseId firstSourceId sourceIds = do + rc <- recursiveBuild firstSourceId -- recursive_build(id) + clause <- foldM buildAndResolve rc sourceIds + storeClauseId clauseId clause + return clause + + where + -- This is the body of the while loop inside the recursiveBuild + -- procedure in the paper. + buildAndResolve :: Clause -> ClauseId -> ResM (Clause) + buildAndResolve clause1 clauseId = + recursiveBuild clauseId >>= resolve Nothing clause1 + + -- Maps ClauseId to built Clause. + storeClauseId :: ClauseId -> Clause -> ResM () + storeClauseId clauseId clause = modify $ \s -> + s{ clauseIdMap = Map.insert clauseId clause (clauseIdMap s) } + + +------------------------------------------------------------------------------ +-- HELPERS +------------------------------------------------------------------------------ + + +-- | Resolve both clauses on the given variable, and throw a resolution error +-- if anything is amiss. Specifically, it checks that there is exactly one +-- occurrence of a literal with the given variable (if variable given) in each +-- clause and they are opposite in polarity. +-- +-- If no variable specified, finds resolving variable, and ensures there's +-- only one such variable. +resolve :: Maybe Var -> Clause -> Clause -> ResM Clause +resolve maybeV c1 c2 = + -- Find complementary literals: + case filter ((`elem` c2) . negate) c1 of + [l] -> case maybeV of + Nothing -> resolveVar (var l) + Just v -> if v == var l + then resolveVar v + else throwError $ ResolveError v c1 c2 + vs -> throwError $ CannotResolve (nub . map var $ vs) c1 c2 + where + resolveVar v = return . nub $ deleteVar v c1 ++ deleteVar v c2 + + deleteVar v c = c `without` lit v `without` negate (lit v) + lit (V i) = L i + +-- | Get the antecedent (reason) for a variable. Every variable encountered +-- ought to have a reason. +getAntecedentId :: Var -> ResM ClauseId +getAntecedentId v = do + anteMap <- asks traceAntecedents + case Map.lookup v anteMap of + Nothing -> throwError (AntecedentMissing v) + Just ante -> return ante + +chooseLiteral :: Clause -> ResM Lit +chooseLiteral (l:_) = return l +chooseLiteral _ = error "chooseLiteral: empty clause" + +checkAnteClause :: Var -> Clause -> ResM () +checkAnteClause v anteClause = do + a <- asks traceFinalAssignment + when (not (anteClause `hasUnitUnder` a)) + (throwError $ AntecedentNotUnit anteClause) + let unitLit = getUnit anteClause a + when (not $ var unitLit == v) + (throwError $ AntecedentImplication (anteClause, unitLit) v) + where + hasUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) diff --git a/src/Funsat/Solver.hs b/src/Funsat/Solver.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/Solver.hs @@ -0,0 +1,1014 @@ +{-# LANGUAGE MultiParamTypeClasses + ,FunctionalDependencies + ,FlexibleInstances + ,FlexibleContexts + ,GeneralizedNewtypeDeriving + ,TypeSynonymInstances + ,TypeOperators + ,ParallelListComp + ,BangPatterns + #-} +{-# OPTIONS -cpp #-} + + + + + + +{-| + +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: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. + + 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.Int( Int64 ) +import Data.List( nub, tails, sortBy, sort ) +import Data.Maybe +import Data.Ord( comparing ) +import Data.STRef +import Data.Sequence( Seq ) +-- import Debug.Trace (trace) +import Funsat.Monad +import Funsat.Utils +import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace ) +import Funsat.Types +import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) +import Funsat.Resolution( ResolutionError(..) ) +import Text.Printf( printf ) +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 when the result is `Unsat'. +solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace) +solve cfg fIn = + -- To solve, we simply take baby steps toward the solution using solveStep, + -- starting with an initial assignment. +-- trace ("input " ++ show f) $ + either (error "solve: invariant violated") id $ + runST $ + evalSSTErrMonad + (do initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0 + (a, isUnsat) <- initialState initialAssignment + if isUnsat then reportSolution (Unsat a) + else stepToSolution initialAssignment >>= reportSolution) + SC{ cnf = f{ clauses = Set.empty }, dl = [] + , watches = undefined, learnt = undefined + , propQ = Seq.empty, trail = [], numConfl = 0, level = undefined + , numConflTotal = 0, numDecisions = 0, numImpl = 0 + , reason = Map.empty, varOrder = undefined + , resolutionTrace = PartialResolutionTrace 1 [] [] Map.empty + , dpllConfig = cfg } + where + f = preprocessCNF fIn + -- If returns True, then problem is unsat. + initialState :: MAssignment s -> DPLLMonad s (IAssignment, Bool) + initialState m = do + initialLevel <- liftST $ newSTUArray (V 1, V (numVars f)) noLevel + modify $ \s -> s{ level = initialLevel } + 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 } + + -- Watch each clause, making sure to bork if we find a contradiction. + (`catchError` + (const $ liftST (unsafeFreezeAss m) >>= \a -> return (a,True))) $ do + forM_ (clauses f) + (\c -> do cid <- nextTraceId + isConsistent <- watchClause m (c, cid) False + when (not isConsistent) + -- conflict data is ignored here, so safe to fake + (do traceClauseId cid ; throwError (L 0, [], 0))) + a <- liftST (unsafeFreezeAss m) + return (a, False) + + +-- | Solve with the default configuration `defaultConfig'. +solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace) +solve1 f = solve (defaultConfig f) f + +-- | This function applies `solveStep' recursively until SAT instance is +-- solved, starting with the given initial assignment. It also implements the +-- conflict-based restarting (see `DPLLConfig'). +stepToSolution :: MAssignment s -> DPLLMonad s Solution +stepToSolution assignment = do + step <- solveStep assignment + useRestarts <- gets (configUseRestarts . dpllConfig) + isTimeToRestart <- uncurry ((>=)) `liftM` + gets (numConfl &&& (configRestart . dpllConfig)) + case step of + Left m -> do when (useRestarts && isTimeToRestart) + (do _stats <- extractStats +-- trace ("Restarting...") $ +-- trace (statSummary stats) $ + resetState m) + stepToSolution m + Right s -> return s + where + resetState m = do + modify $ \s -> s{ numConfl = 0 } + -- Require more conflicts before next restart. + modifySlot dpllConfig $ \s c -> + s{ dpllConfig = c{ configRestart = ceiling (configRestartBump c + * fromIntegral (configRestart c)) + } } + lvl :: FrozenLevelArray <- gets level >>= liftST . unsafeFreeze + undoneLits <- takeWhile (\l -> lvl ! (var l) > 0) `liftM` gets trail + forM_ undoneLits $ const (undoOne m) + modify $ \s -> s{ dl = [], propQ = Seq.empty } + compactDB + unsafeFreezeAss m >>= simplifyDB + +reportSolution :: Solution -> DPLLMonad s (Solution, Stats, Maybe ResolutionTrace) +reportSolution s = do + stats <- extractStats + case s of + Sat _ -> return (s, stats, Nothing) + Unsat _ -> do + resTrace <- constructResTrace s + return (s, stats, Just resTrace) + + +-- | Configuration parameters for the solver. +data DPLLConfig = Cfg + { configRestart :: !Int64 -- ^ Number of conflicts before a restart. + , 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 (Either (MAssignment s) Solution) +solveStep m = do + unsafeFreezeAss m >>= solveStepInvariants + conf <- gets dpllConfig + let selector = if configUseVSIDS conf then select else selectStatic + maybeConfl <- bcp m + mFr <- unsafeFreezeAss m + voArr <- gets (varOrderArr . varOrder) + voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze voArr) + s <- get + stepForward $ + -- Check if unsat. + unsat maybeConfl s ==> postProcessUnsat maybeConfl + -- Unit propagation may reveal conflicts; check. + >< maybeConfl >=> backJump m + -- No conflicts. Decide. + >< selector mFr voFr >=> decide m + where + -- Take the step chosen by the transition guards above. + stepForward Nothing = (Right . Sat) `liftM` unsafeFreezeAss m + stepForward (Just step) = do + r <- step + case r of + Nothing -> (Right . Unsat) `liftM` liftST (unsafeFreezeAss m) + Just m -> return . Left $ m + +-- | /Precondition:/ problem determined to be unsat. +-- +-- Records id of conflicting clause in trace before failing. Always returns +-- `Nothing'. +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 () + +-- ** Internals + +-- | Value of the `level' array if corresponding variable unassigned. Had +-- better be less that 0. +noLevel :: Level +noLevel = -1 + +-- ** 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 + +-- | 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 :: Int) -- 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) +{-# INLINE (==>) #-} +(==>) 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 + +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 _ -> + case Resolution.checkDepthFirst (fromJust maybeRT) of + Left er -> Just . UnsatError $ er + Right _ -> Nothing + where isTrue (Right True) = True + isTrue _ = False + +--------------------------------------- +-- Statistics & trace + + +data Stats = Stats + { statsNumConfl :: Int64 + -- ^ Number of conflicts since last restart. + + , statsNumConflTotal :: Int64 + -- ^ Number of conflicts since beginning of solving. + + , statsNumLearnt :: Int64 + -- ^ Number of learned clauses currently in DB (fluctuates because DB is + -- compacted every restart). + + , statsAvgLearntLen :: Double + -- ^ Avg. number of literals per learnt clause. + + , statsNumDecisions :: Int64 + -- ^ Total number of decisions since beginning of solving. + + , statsNumImpl :: Int64 + -- ^ Total number of unit implications since beginning of solving. + } + +-- | The show instance uses the wrapped string. +newtype ShowWrapped = WrapString { unwrapString :: String } +instance Show ShowWrapped where show = unwrapString + +instance Show Stats where show = show . statTable + +-- | Convert statistics to a nice-to-display tabular form. +statTable :: Stats -> Tabular.Table ShowWrapped +statTable s = + Tabular.mkTable + [ [WrapString "Num. Conflicts" + ,WrapString $ show (statsNumConflTotal s)] + , [WrapString "Num. Learned Clauses" + ,WrapString $ show (statsNumLearnt s)] + , [WrapString " --> Avg. Lits/Clause" + ,WrapString $ show (statsAvgLearntLen s)] + , [WrapString "Num. Decisions" + ,WrapString $ show (statsNumDecisions s)] + , [WrapString "Num. Propagations" + ,WrapString $ show (statsNumImpl s)] ] + +-- | Converts statistics into a tabular, human-readable summary. +statSummary :: Stats -> String +statSummary s = + show (Tabular.mkTable + [[WrapString $ show (statsNumConflTotal s) ++ " Conflicts" + ,WrapString $ "| " ++ show (statsNumLearnt s) ++ " Learned Clauses" + ++ " (avg " ++ printf "%.2f" (statsAvgLearntLen s) + ++ " lits/clause)"]]) + + +extractStats :: DPLLMonad s Stats +extractStats = do + s <- get + learntArr <- liftST $ unsafeFreezeWatchArray (learnt s) + let learnts = (nub . Fl.concat) + [ map (sort . (\(_,c,_) -> c)) (learntArr!i) + | i <- (range . bounds) learntArr ] :: [Clause] + stats = + Stats { statsNumConfl = numConfl s + , statsNumConflTotal = numConflTotal s + , statsNumLearnt = fromIntegral $ length learnts + , statsAvgLearntLen = + fromIntegral (foldl' (+) 0 (map length learnts)) + / fromIntegral (statsNumLearnt stats) + , statsNumDecisions = numDecisions s + , statsNumImpl = numImpl s } + return stats + +unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s]) +unsafeFreezeWatchArray = freeze + + +constructResTrace :: Solution -> DPLLMonad s ResolutionTrace +constructResTrace sol = do + s <- get + watchesIndices <- range `liftM` liftST (getBounds (watches s)) + origClauseMap <- + foldM (\origMap i -> do + clauses <- liftST $ readArray (watches s) i + return $ + foldr (\(_, clause, clauseId) origMap -> + Map.insert clauseId clause origMap) + origMap + clauses) + Map.empty + watchesIndices + let singleClauseMap = + foldr (\(clause, clauseId) m -> Map.insert clauseId clause m) + Map.empty + (resTraceOriginalSingles . resolutionTrace $ s) + anteMap = + foldr (\l anteMap -> Map.insert (var l) (getAnteId s (var l)) anteMap) + Map.empty + (litAssignment . finalAssignment $ sol) + return + (initResolutionTrace + (head (resTrace . resolutionTrace $ s)) + (finalAssignment sol)) + { traceSources = resSourceMap . resolutionTrace $ s + , traceOriginalClauses = origClauseMap `Map.union` singleClauseMap + , traceAntecedents = anteMap } + where + getAnteId s v = snd $ + Map.findWithDefault (error $ "no reason for assigned var " ++ show v) + v (reason s) diff --git a/src/Funsat/Types.hs b/src/Funsat/Types.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/Types.hs @@ -0,0 +1,333 @@ +{-# LANGUAGE MultiParamTypeClasses + ,FunctionalDependencies + ,FlexibleInstances + ,FlexibleContexts + ,GeneralizedNewtypeDeriving + ,TypeSynonymInstances + ,TypeOperators + ,ParallelListComp + ,BangPatterns + #-} + +{- + This file is part of funsat. + + funsat is free software: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. + + 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.List( intercalate ) +import Data.Map ( Map ) +import Data.Set ( Set ) +import Data.STRef +import Funsat.Monad +import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) +import qualified Data.BitSet as BitSet +import qualified Data.Foldable as Fl +import qualified Data.Graph.Inductive.Graph as Graph +import qualified Data.List as List +import qualified Data.Map as Map +import qualified Data.Set as Set + + + +-- * Basic Types + +newtype Var = V {unVar :: Int} deriving (Eq, Ord, Enum, Ix) + +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) + +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 + +-- | Transform the number inside the literal. +inLit :: (Int -> Int) -> Lit -> Lit +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 + | otherwise = error "litSign of 0" + +instance Show Lit where show = show . unLit +instance Read Lit where + readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s) + +-- | The variable for the given literal. +var :: Lit -> Var +var = V . abs . unLit + +-- | The positive literal for the given variable. +lit :: Var -> Lit +lit = L . unVar + +type Clause = [Lit] + +data CNF = CNF + { numVars :: Int + , numClauses :: Int + , clauses :: Set Clause } deriving (Show, Read, Eq) + +-- | The solution to a SAT problem. In each case we return an assignment, +-- which is obviously right in the `Sat' case; in the `Unsat' case, the reason +-- is to assist in the generation of an unsatisfiable core. +data Solution = Sat IAssignment | Unsat IAssignment deriving (Eq) + +instance Show Solution where + show (Sat a) = "satisfiable: " ++ showAssignment a + show (Unsat _) = "unsatisfiable" + +finalAssignment :: Solution -> IAssignment +finalAssignment (Sat a) = a +finalAssignment (Unsat a) = a + + + + +-- | 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 + +showAssignment :: IAssignment -> String +showAssignment a = intercalate " " ([show (a!i) | i <- range . bounds $ a, + (a!i) /= 0]) + + +-- | 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) + +-- | The union of the reason side and the conflict side are all the nodes in +-- the `cutGraph' (excepting, perhaps, the nodes on the reason side at +-- decision level 0, which should never be present in a learned clause). +data Cut f gr a b = + Cut { reasonSide :: f Graph.Node + -- ^ The reason side contains at least the decision variables. + , conflictSide :: f Graph.Node + -- ^ The conflict side contains the conflicting literal. + , cutUIP :: Graph.Node + , cutGraph :: gr a b } +instance (Show (f Graph.Node), Show (gr a b)) => Show (Cut f gr a b) where + show (Cut { conflictSide = c, cutUIP = uip }) = + "Cut (uip=" ++ show uip ++ ", cSide=" ++ show c ++ ")" + +-- | Annotate each variable in the conflict graph with literal (indicating its +-- assignment) and decision level. The only reason we make a new datatype for +-- this is for its `Show' instance. +data CGNodeAnnot = CGNA Lit Int +instance Show CGNodeAnnot where + show (CGNA (L 0) _) = "lambda" + show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")" + + + +-- * Model + + +-- | 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 () + where + isFalseUnder x m = isFalse $ x `statusUnder` m + where isFalse (Right False) = True + isFalse _ = False + +-- * 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 + + +-- | 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 + +instance Show (STRef s a) where show = const "" +instance Show (STUArray s Var Int) where show = const "" +instance Show (STUArray s Var Double) where show = const "" +instance Show (STArray s a b) where show = const "" diff --git a/src/Funsat/Utils.hs b/src/Funsat/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/Utils.hs @@ -0,0 +1,272 @@ +{-# LANGUAGE MultiParamTypeClasses + ,FunctionalDependencies + ,FlexibleInstances + ,FlexibleContexts #-} + +{- + This file is part of funsat. + + funsat is free software: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. + + Copyright 2008 Denis Bueno +-} + + +{-| + +Generic utilities that happen to be used in the SAT solver. + +-} +module Funsat.Utils where + +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.List( foldl1' ) +import Data.Map (Map) +import Data.Set (Set) +import Debug.Trace( trace ) +import Funsat.Types +import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) +import System.IO.Unsafe( unsafePerformIO ) +import System.IO( hPutStr, stderr ) +import qualified Data.Foldable as Fl +import qualified Data.Graph.Inductive.Graph as Graph +import qualified Data.Graph.Inductive.Query.DFS as DFS +import qualified Data.List as List +import qualified Data.Map as Map +import qualified Data.Set as Set + + + +-- | `True' if and only if the object is undefined in the model. +isUndefUnder :: Model a m => a -> m -> Bool +isUndefUnder x m = isUndef $ x `statusUnder` m + where isUndef (Left ()) = True + isUndef _ = False + +-- | `True' if and only if the object is true in the model. +isTrueUnder :: Model a m => a -> m -> Bool +isTrueUnder x m = isTrue $ x `statusUnder` m + where isTrue (Right True) = True + isTrue _ = False + +-- | `True' if and only if the object is false in the model. +isFalseUnder :: Model a m => a -> m -> Bool +isFalseUnder x m = isFalse $ x `statusUnder` m + where isFalse (Right False) = True + isFalse _ = False + +-- * Helpers + + +-- isUnitUnder c m | trace ("isUnitUnder " ++ show c ++ " " ++ showAssignment m) $ False = undefined + +-- | Whether all the elements of the model in the list are false but one, and +-- none is true, under the model. +isUnitUnder :: (Model a m) => [a] -> m -> Bool +{-# SPECIALISE INLINE isUnitUnder :: Clause -> IAssignment -> Bool #-} +isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) + && not (Fl.any (`isTrueUnder` m) c) + +-- Precondition: clause is unit. +-- getUnit :: (Model a m, Show a, Show m) => [a] -> m -> a +-- getUnit c m | trace ("getUnit " ++ show c ++ " " ++ showAssignment m) $ False = undefined + +-- | Get the element of the list which is not false under the model. If no +-- such element, throws an error. +getUnit :: (Model a m, Show a) => [a] -> m -> a +{-# SPECIALISE INLINE getUnit :: Clause -> IAssignment -> Lit #-} +getUnit c m = case filter (not . (`isFalseUnder` m)) c of + [u] -> u + xs -> error $ "getUnit: not unit: " ++ show xs + + +{-# INLINE mytrace #-} +mytrace :: String -> a -> a +mytrace msg expr = unsafePerformIO $ do + hPutStr stderr msg + return expr + +outputConflict :: FilePath -> String -> a -> a +outputConflict fn g x = unsafePerformIO $ do writeFile fn g + return x + + +-- | /O(1)/ Whether a list contains a single element. +isSingle :: [a] -> Bool +{-# INLINE isSingle #-} +isSingle [_] = True +isSingle _ = False + +-- | Modify a value inside the state. +modifySlot :: (MonadState s m) => (s -> a) -> (s -> a -> s) -> m () +{-# INLINE modifySlot #-} +modifySlot slot f = modify $ \s -> f s (slot s) + +-- | @modifyArray arr i f@ applies the function @f@ to the index @i@ and the +-- current value of the array at index @i@, then writes the result into @i@ in +-- the array. +modifyArray :: (Monad m, MArray a e m, Ix i) => a i e -> i -> (i -> e -> e) -> m () +{-# INLINE modifyArray #-} +modifyArray arr i f = readArray arr i >>= writeArray arr i . (f i) + +-- | Same as @newArray@, but helping along the type checker. +newSTUArray :: (MArray (STUArray s) e (ST s), Ix i) + => (i, i) -> e -> ST s (STUArray s i e) +newSTUArray = newArray + +newSTArray :: (MArray (STArray s) e (ST s), Ix i) + => (i, i) -> e -> ST s (STArray s i e) +newSTArray = newArray + + +-- | Count the number of elements in the list that satisfy the predicate. +count :: (a -> Bool) -> [a] -> Int +count p = foldl' f 0 + where f x y | p y = x + 1 + | otherwise = x + +-- | /O(1)/ @argmin f x y@ is the argument whose image is least under @f@; if +-- the images are equal, returns the first. +argmin :: Ord b => (a -> b) -> a -> a -> a +argmin f x y = if f x <= f y then x else y + +-- | /O(length xs)/ @argminimum f xs@ returns the value in @xs@ whose image +-- is least under @f@; if @xs@ is empty, throws an error. +argminimum :: Ord b => (a -> b) -> [a] -> a +argminimum f = foldl1' (argmin f) + + +-- | Show the value with trace, then return it. Useful because you can wrap +-- it around any subexpression to print it when it is forced. +tracing :: (Show a) => a -> a +tracing x = trace (show x) x + +-- | Returns a predicate which holds exactly when both of the given predicates +-- hold. +(.&&.) :: (a -> Bool) -> (a -> Bool) -> (a -> Bool) +p .&&. q = \x -> p x && q x + + +-- | Generate a cut using the given UIP node. The cut generated contains +-- exactly the (transitively) implied nodes starting with (but not including) +-- the UIP on the conflict side, with the rest of the nodes on the reason +-- side. +uipCut :: (Graph gr) => + [Lit] -- ^ decision literals + -> FrozenLevelArray + -> gr a b -- ^ conflict graph + -> Graph.Node -- ^ unassigned, implied conflicting node + -> Graph.Node -- ^ a UIP in the conflict graph + -> Cut Set gr a b +uipCut dlits levelArr conflGraph conflNode uip = + Cut { reasonSide = Set.filter (\i -> levelArr!(V $ abs i) > 0) $ + allNodes Set.\\ impliedByUIP + , conflictSide = impliedByUIP + , cutUIP = uip + , cutGraph = conflGraph } + where + -- Transitively implied, and not including the UIP. + impliedByUIP = Set.insert extraNode $ + Set.fromList $ tail $ DFS.reachable uip conflGraph + -- The UIP may not imply the assigned conflict variable which needs to + -- be on the conflict side, unless it's a decision variable or the UIP + -- itself. + extraNode = if L (negate conflNode) `elem` dlits || negate conflNode == uip + then conflNode -- idempotent addition + else negate conflNode + allNodes = Set.fromList $ Graph.nodes conflGraph + + +-- | Generate a learned clause from a cut of the graph. Returns a pair of the +-- learned clause and the decision level to which to backtrack. +cutLearn :: (Graph gr, Foldable f) => IAssignment -> FrozenLevelArray + -> Cut f gr a b -> (Clause, Int) +cutLearn a levelArr cut = + ( clause + -- The new decision level is the max level of all variables in the + -- clause, excluding the uip (which is always at the current decision + -- level). + , maximum0 (map (levelArr!) . (`without` V (abs $ cutUIP cut)) . map var $ clause) ) + where + -- The clause is composed of the variables on the reason side which have + -- at least one successor on the conflict side. The value of the variable + -- is the negation of its value under the current assignment. + clause = + foldl' (\ls i -> + if any (`elem` conflictSide cut) (Graph.suc (cutGraph cut) i) + then L (negate $ a!(V $ abs i)):ls + else ls) + [] (reasonSide cut) + maximum0 [] = 0 -- maximum0 has 0 as its max for the empty list + maximum0 xs = maximum xs + + +-- | Creates the conflict graph, where each node is labeled by its literal and +-- level. +-- +-- Useful for getting pretty graphviz output of a conflict. +mkConflGraph :: DynGraph gr => + IAssignment + -> FrozenLevelArray + -> Map Var Clause + -> [Lit] -- ^ decision lits, in rev. chron. order + -> (Lit, Clause) -- ^ conflict info + -> gr CGNodeAnnot () +mkConflGraph mFr lev reasonMap _dlits (cLit, confl) = + Graph.mkGraph nodes' edges' + where + -- we pick out all the variables from the conflict graph, specially adding + -- both literals of the conflict variable, so that that variable has two + -- nodes in the graph. + nodes' = + ((0, CGNA (L 0) (-1)) :) $ -- lambda node + ((unLit cLit, CGNA cLit (-1)) :) $ + ((negate (unLit cLit), CGNA (negate cLit) (lev!(var cLit))) :) $ + -- annotate each node with its literal and level + map (\v -> (unVar v, CGNA (varToLit v) (lev!v))) $ + filter (\v -> v /= var cLit) $ + toList nodeSet' + + -- node set includes all variables reachable from conflict. This node set + -- construction needs a `seen' set because it might infinite loop + -- otherwise. + (nodeSet', edges') = + mkGr Set.empty (Set.empty, [ (unLit cLit, 0, ()) + , ((negate . unLit) cLit, 0, ()) ]) + [negate cLit, cLit] + varToLit v = (if v `isTrueUnder` mFr then id else negate) $ L (unVar v) + + -- seed with both conflicting literals + mkGr _ ne [] = ne + mkGr (seen :: Set Graph.Node) ne@(nodes, edges) (lit:lits) = + if haveSeen + then mkGr seen ne lits + else newNodes `seq` newEdges `seq` + mkGr seen' (newNodes, newEdges) (lits ++ pred) + where + haveSeen = seen `contains` litNode lit + newNodes = var lit `Set.insert` nodes + newEdges = [ ( litNode (negate x) -- unimplied lits from reasons are + -- complemented + , litNode lit, () ) + | x <- pred ] ++ edges + pred = filterReason $ + if lit == cLit then confl else + Map.findWithDefault [] (var lit) reasonMap `without` lit + filterReason = filter ( ((var lit /=) . var) .&&. + ((<= litLevel lit) . litLevel) ) + seen' = seen `with` litNode lit + litLevel l = if l == cLit then length _dlits else lev!(var l) + litNode l = -- lit to node + if var l == var cLit -- preserve sign of conflicting lit + then unLit l + else (abs . unLit) l + + diff --git a/src/Text/Tabular.hs b/src/Text/Tabular.hs new file mode 100644 --- /dev/null +++ b/src/Text/Tabular.hs @@ -0,0 +1,70 @@ +{- + This file is part of funsat. + + funsat is free software: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. + + Copyright 2008 Denis Bueno +-} + +{-| + +Tabular output. + +Converts 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( Table(..), mkTable, combine, unTable ) where + +import Data.List( intercalate ) + +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 + -- string representations of all the elements in the column + -- in which this cell occurs + , cellData :: !a } -- element printed in box of colWidth + +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 :: Table a -> [[a]] +unTable (Table rows) = [ map cellData r | (Row r) <- rows ] + +combine :: (Show a) => Table a -> Table a -> Table a +-- slow impl but works +combine t t' = mkTable (unTable t ++ unTable t') + +-- returns a list of the widths of each column +colWidths :: (Show a) => [[a]] -> [Int] +colWidths = map (maximum . map (length . show)) . zipn + +-- Pretty, columnar output. +instance (Show a) => Show (Table a) where + show (Table rows) = intercalate "\n" $ map showRow rows + where + showRow (Row cols) = intercalate " " $ colStrings + where + colStrings = [ padString (cellWidth c) (show d) + | c@(Cell {cellData=d}) <- cols ] + +padString :: Int -> String -> String +padString maxWidth str = str ++ replicate padLen ' ' + where padLen = maxWidth - length str + +zipn :: [[a]] -> [[a]] +zipn xss | any null xss = [] +zipn xss = map head xss : zipn (map tail xss) + + diff --git a/tests/Properties.hs b/tests/Properties.hs --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -4,94 +4,99 @@ {- 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 . + funsat is free software: it is released under the BSD3 open source license. + You can find details of this license in the file LICENSE at the root of the + source tree. Copyright 2008 Denis Bueno -} import Funsat.Solver hiding ((==>)) -import Control.Monad (replicateM) +import Control.Exception( assert ) +import Control.Monad import Data.Array.Unboxed import Data.BitSet (hash) -import Data.Bits +import Data.Bits hiding( xor ) import Data.Foldable hiding (sequence_) -import Data.List (nub, splitAt, unfoldr, delete, sort, sortBy) +import Data.List (nub, splitAt) import Data.Maybe -import Data.Ord( comparing ) +import Data.Set( Set ) import Debug.Trace -import Funsat.Solver( verify ) +import Funsat.Circuit hiding( Circuit(..) ) +import Funsat.Circuit( Circuit(input,true,false,ite,xor,onlyif) ) import Funsat.Types import Funsat.Utils import Language.CNF.Parse.ParseDIMACS( parseFile ) -import Prelude hiding ( or, and, all, any, elem, minimum, foldr, splitAt, concatMap - , sum, concat ) -import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace ) +import Prelude hiding ( or, and, all, any, elem, minimum, foldr, splitAt, concatMap, sum, concat ) +import Funsat.Resolution( ResolutionTrace(..) ) +import System.IO import System.Random import Test.QuickCheck hiding (defaultConfig) + import qualified Data.Foldable as Foldable import qualified Data.List as List import qualified Data.Set as Set +import qualified Data.Map as Map import qualified Funsat.Resolution as Resolution import qualified Language.CNF.Parse.ParseDIMACS as ParseCNF import qualified Test.QuickCheck as QC +import qualified Funsat.Circuit as C +import qualified Funsat.Circuit as Circuit main :: IO () main = do --- let s = solve1 prob1 --- case s of --- Unsat -> return () --- Sat m -> if not (verifyBool m prob1) --- then putStrLn (show (find (`isFalseUnder` m) prob1)) --- else return () - --setStdGen (mkStdGen 42) - check config prop_randAssign - check config prop_allIsTrueUnderA - check config prop_noneIsFalseUnderA - check config prop_noneIsUndefUnderA - check config prop_negIsFalseUnder - check config prop_negNotUndefUnder - check config prop_outsideUndefUnder - check config prop_clauseStatusUnderA - check config prop_negDefNotUndefUnder - check config prop_undefUnderImpliesNegUndef - check config prop_litHash - check config prop_varHash - check config prop_count + hPutStr stderr "prop_randAssign: " >> check config prop_randAssign + hPutStr stderr "prop_allIsTrueUnderA: " >> check config prop_allIsTrueUnderA + hPutStr stderr "prop_noneIsFalseUnderA: " >> check config prop_noneIsFalseUnderA + hPutStr stderr "prop_noneIsUndefUnderA: " >> check config prop_noneIsUndefUnderA + hPutStr stderr "prop_negIsFalseUnder: " >> check config prop_negIsFalseUnder + hPutStr stderr "prop_negNotUndefUnder: " >> check config prop_negNotUndefUnder + hPutStr stderr "prop_outsideUndefUnder: " >> check config prop_outsideUndefUnder + hPutStr stderr "prop_clauseStatusUnderA: " >> check config prop_clauseStatusUnderA + hPutStr stderr "prop_negDefNotUndefUnder: " >> check config prop_negDefNotUndefUnder + hPutStr stderr "prop_undefUnderImpliesNegUndef: " >> check config prop_undefUnderImpliesNegUndef + hPutStr stderr "prop_litHash: " >> check config prop_litHash + hPutStr stderr "prop_varHash: " >> check config prop_varHash + hPutStr stderr "prop_count: " >> check config prop_count + hPutStr stderr "prop_circuitToCnf: " >> check config prop_circuitToCnf + hPutStr stderr "prop_circuitSimplify: " >> check config prop_circuitSimplify - -- Add more tests above here. Setting the rng keeps the SAT instances - -- the same even if more tests are added above. Reproducible results - -- are important. + -- Add more tests above here. Setting the rng keeps the SAT instances the + -- same even if more tests are added above. I want this because if I make + -- a change that makes the solver dramatically faster or slower, I know + -- this wasn't due to the test distribution. + gen <- getStdGen setStdGen (mkStdGen 42) + hPutStr stderr "prop_solveCorrect: " check solveConfig prop_solveCorrect + setStdGen gen + hPutStr stderr "prop_solveCorrect (rand): " + check solveConfig prop_solveCorrect + gen <- getStdGen + setStdGen (mkStdGen 42) + hPutStr stderr "prop_resolutionChecker: " check resChkConfig prop_resolutionChecker + setStdGen gen + hPutStr stderr "prop_resolutionChecker (rand): " + check resChkConfig prop_resolutionChecker + + config = QC.defaultConfig { configMaxTest = 1000 } -- Special configuration for the "solve this random instance" tests. -solveConfig = QC.defaultConfig { configMaxTest = 2000 } +solveConfig = QC.defaultConfig { configMaxTest = 2000 } resChkConfig = QC.defaultConfig{ configMaxTest = 1200 } myConfigEvery testnum args = show testnum ++ ": " ++ show args ++ "\n\n" -- * Tests prop_solveCorrect (cnf :: CNF) = - label "prop_solveCorrect" $ trivial (numClauses cnf < 2 || numVars cnf < 2) $ classify (numClauses cnf > 15 || numVars cnf > 10) "c>15, v>10" $ classify (numClauses cnf > 30 || numVars cnf > 20) "c>30, v>20" $ @@ -107,39 +112,32 @@ Right _ -> True prop_resolutionChecker (cnf :: UnsatCNF) = - label "prop_resolutionChecker" $ case solve1 (unUnsatCNF cnf) of - (Sat _,_,_) -> label "SAT" True + (Sat _,_,_) -> label "SAT (unverified)" True (Unsat _,_,rt) -> label "UNSAT" $ - case Resolution.checkDepthFirst (fromJust rt) of - Left e -> False + case Resolution.genUnsatCore (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"$ allA (\i -> if i /= 0 then L i `isTrueUnder` m else True) m prop_noneIsFalseUnderA (m :: IAssignment) = - label "prop_noneIsFalseUnderA"$ not $ anyA (\i -> if i /= 0 then L i `isFalseUnder` m else False) m prop_noneIsUndefUnderA (m :: IAssignment) = - label "prop_noneIsUndefUnderA"$ not $ anyA (\i -> if i /= 0 then L i `isUndefUnder` m else False) m prop_negIsFalseUnder (m :: IAssignment) = - label "prop_negIsFalseUnder"$ allA (\l -> if l /= 0 then negate (L l) `isFalseUnder` m else True) m prop_negNotUndefUnder (m :: IAssignment) = - label "prop_negNotUndefUnder"$ allA (\l -> if l /= 0 then not (negate (L l) `isUndefUnder` m) else True) m prop_outsideUndefUnder (l :: Lit) (m :: IAssignment) = - label "prop_outsideUndefUnder"$ trivial ((unVar . var) l > rangeSize (bounds m)) $ inRange (bounds m) (var l) ==> trivial (m `contains` l || m `contains` negate l) $ @@ -147,20 +145,17 @@ l `isUndefUnder` m prop_negDefNotUndefUnder (l :: Lit) (m :: IAssignment) = - label "prop_negDefNotUndefUnder" $ inRange (bounds m) (var l) ==> m `contains` l || m `contains` (negate l) ==> l `isTrueUnder` m || negate l `isTrueUnder` m prop_undefUnderImpliesNegUndef (l :: Lit) (m :: IAssignment) = - label "prop_undefUnderImpliesNegUndef" $ inRange (bounds m) (var l) ==> trivial (m `contains` l) $ l `isUndefUnder` m ==> negate l `isUndefUnder` m prop_clauseStatusUnderA (c :: Clause) (m :: IAssignment) = - label "prop_clauseStatusUnderA" $ classify expectTrueTest "expectTrue"$ classify expectFalseTest "expectFalseTest"$ classify expectUndefTest "expectUndefTest"$ @@ -175,7 +170,6 @@ -- Verify assignments generated are sane, i.e. no assignment contains an -- element and its negation. prop_randAssign (a :: IAssignment) = - label "randAssign"$ not $ anyA (\l -> if l /= 0 then a `contains` (negate $ L l) else False) a -- unitPropFar should stop only if it can't propagate anymore. @@ -195,11 +189,9 @@ -- Make sure the bit set will work. prop_litHash (k :: Lit) (l :: Lit) = - label "prop_litHash" $ hash k == hash l <==> k == l prop_varHash (k :: Var) l = - label "prop_varHash" $ hash k == hash l <==> k == l @@ -207,49 +199,11 @@ infixl 3 <==> --- newtype WPTest s = WPTest (WatchedPair s) - --- instance Arbitrary (WPTest s) where --- arbitrary = sized sizedWPTest --- where sizedWPTest n = do --- [lit1, lit2] <- 2 `uniqElts` 1 --- clause :: Clause <- arbitrary --- return $ runST $ --- do r <- newSTRef (lit1, lit2) --- return (r, lit1 : lit2 : clause) - -newtype Nat = Nat { unNat :: Int } - deriving (Eq, Ord) -instance Show Nat where - show (Nat i) = "Nat " ++ show i -instance Num Nat where - (Nat x) + (Nat y) = Nat (x + y) - (Nat x) - (Nat y) | x >= y = Nat (x - y) - | x < y = error "Nat: subtraction out of range" - (Nat x) * (Nat y) = Nat (x * y) - abs = id - signum (Nat n) | n == 0 = 0 - | n > 0 = 1 - | n < 0 = error "Nat: signum of negative number" - fromInteger n | n >= 0 = Nat (fromInteger n) - | n < 0 = error "Negative natural literal found" - -instance Arbitrary Nat where - arbitrary = sized $ \n -> do i <- choose (0, n) - return (fromIntegral i) - - --- sanity checking for Arbitrary Nat instance. -prop_nat (xs :: [Nat]) = trivial (null xs) $ sum xs >= 0 -prop_nat1 (xs :: [Nat]) = trivial (null xs) $ unNat (sum xs) == sum (map unNat xs) - prop_count p xs = - label "prop_count" $ count p xs == length (filter p xs) where _types = xs :: [Int] prop_argmin f x y = - label "prop_argmin" $ f x /= f y ==> argmin f x y == m where m = if f x < f y then x else y @@ -258,7 +212,46 @@ show = const "" +-- ** Circuits and CNF conversion +-- If CNF generated from circuit satisfiable, check that circuit is by that +-- assignment. +prop_circuitToCnf :: Circuit.Tree Var -> Property +prop_circuitToCnf treeCircuit = + let pblm@(CircuitProblem{ problemCnf = cnf }) = + toCNF . runShared . castCircuit $ treeCircuit + (solution, _, _) = solve1 cnf + in case solution of + Sat{} -> let benv = projectCircuitSolution solution pblm + in label "Sat" + . trivial (Map.null benv) + $ runEval benv (castCircuit treeCircuit) + + Unsat{} -> label "Unsat (unverified)" True + +-- circuit and simplified version should evaluate the same +prop_circuitSimplify :: ArbBEnv -> Circuit.Tree Var -> Property +prop_circuitSimplify (ArbBEnv benv) c = + trivial (c == TTrue || c == TFalse) $ + assert (treeVars c `Set.isSubsetOf` Map.keysSet benv) $ + runEval benv (castCircuit c) + == runEval benv (castCircuit . simplifyTree $ c) + +{- +prop_circuitGraphIsTree :: C.Shared Var -> Property +prop_circuitGraphIsTree sh = c `equivalentTo` g + where + equivalentTo = undefined + g = castCircuit c :: Graph Var + c = C.runShared sh +-} + +treeVars :: (Ord v) => Circuit.Tree v -> Set v +treeVars = C.foldTree (flip Set.insert) Set.empty + + + + ------------------------------------------------------------------------------ -- * Helpers ------------------------------------------------------------------------------ @@ -344,12 +337,43 @@ instance Arbitrary CNF where arbitrary = sized (genRandom3SAT 3.0) +newtype ArbBEnv = ArbBEnv (BEnv Var) deriving (Show) +instance Arbitrary ArbBEnv where + coarbitrary = undefined + arbitrary = sized $ \n -> do + bools <- vector (n+1) :: Gen [Bool] + return . ArbBEnv $ Map.fromList (zip [V 1 .. V (n+1)] bools) + +instance Arbitrary (Tree Var) where + arbitrary = sized sizedCircuit + sizedLit n = do v <- choose (1, n) t <- oneof [return id, return negate] return $ L (t v) --- Generate a random 3SAT problem with the given ratio of clauses/variable. + +-- | Generator for a circuit containing at most `n' nodes, involving only the +-- literals 1 .. n. +sizedCircuit :: (Circuit c) => Int -> Gen (c Var) +sizedCircuit 0 = return . input . V $ 1 +sizedCircuit n = + oneof [ return true + , return false + , (return . input . V) n + , liftM2 C.and subcircuit2 subcircuit2 + , liftM2 C.or subcircuit2 subcircuit2 + , liftM C.not subcircuit1 + , liftM3 ite subcircuit3 subcircuit3 subcircuit3 + , liftM2 onlyif subcircuit2 subcircuit2 + , liftM2 C.iff subcircuit2 subcircuit2 + , liftM2 xor subcircuit2 subcircuit2 + ] + where subcircuit3 = sizedCircuit (n `div` 3) + subcircuit2 = sizedCircuit (n `div` 2) + subcircuit1 = sizedCircuit (n - 1) + +-- | Generate a random 3SAT problem with the given ratio of clauses/variable. -- -- Current research suggests: -- @@ -389,92 +413,10 @@ newtype UnsatCNF = UnsatCNF { unUnsatCNF :: CNF } deriving (Show) instance Arbitrary UnsatCNF where - arbitrary = do - f <- sized (genRandom3SAT 5.19) - return (UnsatCNF f) - + arbitrary = liftM UnsatCNF $ sized (genRandom3SAT 5.19) ------------------------------------------------------------------------------- --- ** Simplification ------------------------------------------------------------------------------- - -class WellFoundedSimplifier a where - -- | If the argument can be made simpler, a list of one-step simpler - -- objects. Only in cases where there are multiple "dimensions" to - -- simplify should the returned list have length more than 1. Otherwise - -- returns the empty list. - simplify :: a -> [a] - -instance WellFoundedSimplifier a => WellFoundedSimplifier [a] where - simplify [] = [] - simplify (x:xs) = case simplify x of - [] -> [xs] - x's-> map (:xs) x's - -instance WellFoundedSimplifier () where - simplify () = [] - -instance WellFoundedSimplifier Bool where - simplify True = [False] - simplify False = [] - -instance WellFoundedSimplifier Int where - simplify i | i == 0 = [] - | i > 0 = [i-1] - | i < 0 = [i+1] - --- Assign the highest variable and reduce the number of variables. -instance WellFoundedSimplifier CNF where - simplify f - | numVars f <= 1 = [] - | numVars f > 1 = [ f{ numVars = numVars f - 1 - , clauses = clauses' - , numClauses = Set.size clauses' } --- , f{ clauses = Set.deleteMax (clauses f) --- , numClauses = numClauses f - 1 } - ] - where - clauses' = foldl' assignVar Set.empty (clauses f) - pos = L (numVars f) - neg = negate pos - assignVar outClauses clause = - let clause' = neg `delete` clause - in if pos `elem` clause || null clause' then outClauses - else clause' `Set.insert` outClauses - - -simplifications :: WellFoundedSimplifier a => a -> [a] -simplifications a = concat $ unfoldr (\ xs -> let r = concatMap simplify xs - in if null r then Nothing - else Just (r, r)) - [a] - --- Returns smallest CNF simplification that also gives erroneous output. -minimalError :: CNF -> CNF -minimalError f = lastST f satAndWrong (simplifications f) - where satAndWrong f_inner = - trace (show (numVars f_inner) ++ "/" ++ show (numClauses f_inner)) $ - case solve1 f_inner of - (Unsat _,_,_) -> False - (Sat a,_,rt) -> not (verifyBool (Sat a) rt f_inner) - --- last (takeWhile p xs) in the common case. --- mnemonic: "last Such That" -lastST def _ [] = def -lastST def p (x:xs) = if p x then lastST x p xs else def - -prop_lastST (x :: Int) = - if not (null xs) && xa > 3 then - classify True "nontrivial" $ - last (takeWhile p xs) == lastST undefined p xs - else True `trivial` True - where p = (> xa `div` 2) - xs = simplifications xa - xa = abs x - - getCNF :: Int -> IO CNF getCNF maxVars = do g <- newStdGen return (generate (maxVars * 3) g arbitrary) @@ -492,15 +434,6 @@ CNF {numVars = v ,numClauses = c ,clauses = Set.fromList . map (map fromIntegral . elems) $ is} - - --- import qualified Data.ByteString.Char8 as B - --- hStrictGetContents :: Handle -> IO String --- hStrictGetContents h = do --- bs <- B.hGetContents h --- hClose h -- not sure if this is required; ByteString documentation isn't clear. --- return $ B.unpack bs -- lazy unpack into String verifyBool :: Solution -> Maybe ResolutionTrace -> CNF -> Bool diff --git a/todo.org b/todo.org deleted file mode 100644 --- a/todo.org +++ /dev/null @@ -1,248 +0,0 @@ -* Sat todo file - -* TODO Group paired result.x files into their own graphs. :GraphResult: -This would make GraphResult generate n graphs when n benchmark results are -available from both timestamps. This is just another dimension of generality -that isn't hard to support. - - -* TODO resTrace field of resolution trace in solver can go -Why do I even need the trace? I just need the original clause ids and the -source map, right? - -* DONE Export and document defaultConfig :release: - CLOSED: [2008-06-07 Sat 14:29] - -* DONE Release initial version to hackage - CLOSED: [2008-06-06 Fri 10:49] - -* DONE Derive resolution proof of UNSAT in order to aid debugging :feature: - CLOSED: [2008-06-07 Sat 20:32] -This feature essentially enables the following one, or vice versa. - -+Add Writer capability to the Funsat monad+ -Just put it in the state record. - -** DONE Write quickCheck tests for checker - CLOSED: [2008-07-07 Mon 20:05] -Use a generater that will always generate unsat problems, then check them, and -make sure unsat core is correct too. - -*** TODO [#A] Resolution.check has a bug. Find it. :bug:ARCHIVE: - -** DONE Add unique ids to clauses - CLOSED: [2008-06-07 Sat 20:32] - -** DONE [#A] Add unsatisfiable core extraction :feature: - CLOSED: [2008-06-07 Sat 14:23] - -Algorithm from DATE_2003: - -1. Each time learned clause generated, clause's ID is recorded, along with - each encountered "reason". - - So I should be able to simply assign IDs to each original clause and - learned clause. When I do the conflict analysis, each reason (by the - invariant) already has an ID. I record all of these and generate a new ID - for the learned clause. - -2. When unsat is determined, record reason for conflicting variable - assignment. That is, the clause that propagated the conflicting variable - assignment must have been false, so record its ID. [Is this true? Suppose - at decision level 0 bcp propagates -1 and 1 is assigned. It propagated -1 - because some clause was entirely false except it had -1. But 1 is - assigned. So, it must have been the clause was entirely false. Hence the - reason for the propagation of the last conflicting clause is the ID we - should record. QED.] - -3. Before returning Unsat from the solver, record all assigned variables - (which by construction are all at decision level 0) and their values, and - record the IDs of the "reason" for each variable. - -It should be sufficient to start with a linear trace of IDs along with the -final variable assignments (produced in step 3). In particular, we don't need -all the literals of each learned clause at recording time. - -** Correctness -@recursive_build@ reconstructs the clause corresponding to the input id. -First we build the final conflicting clause. This clause must be false under -the terminating assignment. Call this clause X. - -If the loop terminates and no errors, clearly we have a proper proof. - -If the loop never terminates, then X is never the empty clause. But if -resolve() finds a resolvent, cl is always "smaller". Since there are only -finitely many variables & reasons, we will get the empty clause or find an -error. - -*** In check_depth_first, can we resolve on any lit in clause & get a clause -that is false? - -Proof: -Assume SAT solver is correct. Let l be in the last clause. The antecedent -for l propagated -l (*), and therefore contains -l. Hence we can resolve and -still get a clause that is false. - -Suppose X is the antecedent clause for l in a clause Z. By induction -hypothesis, Z is false. Since X is the antecedent for l, X propagated -l (*). -... Hence, we can resolve on l preserving. - -If we cannot, SAT solver is incorrect. In particular, the assumptions marked -(*) are the ones guaranteed by the correct operation of the solver. - -*** In recursive_build - * recursive_build first bottoms out when it hits an original clause. - -**** Original clause -Suppose cl_id is an original clause. Then it is already built (i.e. should be -supplied to checker). - -If not, the clause we're constructing corresponds to a learned clause. -Construct clause CL of first source. (*) Then construct clause of second -source. Resolve them into X1. Resolve X1 with build clause of next source of -cl_id. Resolve into X2...Xn. Build and return Xn. - - [Both of these clauses are either reasons used or the conflicting clause - used when generating the learned clause. - - Suppose the conflict clause has only two sources. Obviously both must - mention the conflicting lit. Otherwise they would not be present.] - -*** Invariants -INVARIANT: every variable in the final assignment has an antecedent. This is -true if the SAT solver is correct. - -INVARIANT: every variable in an antecedent (reason) is assigned. Also true if -the SAT solver is true. - -INVARIANT: All reasons are non-empty. Duh, otherwise they could not have -propagated. - -Therefore, if any of these fails, there might be an error in the solver/trace -generation. So they should be reported as ResolutionErrors. - -* DONE Add -funbox-strict-fields to the ghc-options :bench: - CLOSED: [2008-06-06 Fri 13:49] -and see how it affects performance. - -Did this long ago. Minus the "see how it affects performance" part. - -* DONE [#A] Remove stupid command-line options :cleanup: - CLOSED: [2008-06-06 Fri 11:47] - -* TODO [#C] Initial state for dynamic variable ordering should be -based on the number of occurrences of literals in the clause database at the -beginning, or something. Some heuristic that puts important variables first -at the beginning, instead of starting out all at zero. - -* DONE [#A] Remove the monad stack from bcpLit - CLOSED: [2008-06-05 Thu 20:14] -There are three monads there! Can we just write a single monad data type on -top of ST that has errors and whatnot? - -Did this long ago. -** Result ... - -* TODO [#K] On some problems, select is a bottleneck, much :heuristics: -more than bcpLit. Even so, reverting to a static ordering gives worse -runtime. So ... if we had a faster way of selecting the min, it would be -nice. - -* TODO There is a bug in mkConflGraph :ARCHIVE: -mkConflGraph' is the old code that seemed to work, but it's much slower. - -* DONE Bug fixed - CLOSED: [2008-05-08 Thu 22:17] -** decision list wasn't reset on restarts -** propQ wasn't reset on restarts - -* TODO Problem simplification -** Whenever we restart, remove the negations of all unit facts from each clause. - -* DONE [#A] Debug clause learning - CLOSED: [2008-04-24 Thu 15:57] -Currently, bugs. - -** There is a confusion between reasons and actual assigned variables -When asking for the level of a variable in the current assignment, the -conflict variable should be treated specially -- it's at the current level. -Otherwise, you can just ask for the level of the variable. - -Say the conflicting literals is -20. Then 20 is in the current assignment --- -that's why -20 conflicts. Now, suppose you expand a literal `x' whose reason -contains -20 -- that is, since 20 is true, -20 was in a clause which became -unit, and propagated `x'. Asking for the level of -20 is wrong -- when asking -for the level of a *reason*, we always want the level of the corresponding -variable, so that we don't confuse it with the conflicting literal. - -* DONE VSIDS bumping should happen for each variable encountered - CLOSED: [2008-06-05 Thu 20:15] -while generating the learnt clause. - -* TODO [#K] Recursive learning/parallel stuff - -* DONE Learned clause deletion - CLOSED: [2008-04-03 Thu 12:18] - -* DONE Make "bad" bag use bitset - CLOSED: [2008-03-18 Tue 10:11] - -* 29 Feb 2008 16:43:29 -I had to re-install GHC 6.8.1 for a reason that is not important. I was going -to install 6.8.2, which I had to compile myself. While waiting for that, I -worked on DPLLSat with 6.8.1. My tests run in 5 seconds, without -optimisations! Last night I was waiting 10 minutes. And this is user time! -I have no idea why. I did change the unit propagation code today, but only -making it do more work! - -I'm going to install 6.8.2, and then put 6.8.1 somewhere else so I can switch -between them easily, somehow. Weird, weird. - -This could be explained by a different test distribution ... - -* DONE Make unit propagation propagate with learned clauses too. - CLOSED: [2008-03-18 Tue 10:11] - -* TODO [#K] Incorporate stupid frequency-based decision heuristic :ARCHIVE: - -* DONE Implement clause learning but only after - CLOSED: [2008-03-18 Tue 10:11] -watched literals, otherwise the number of times we have to walk the set of -clauses will really kill the runtime. - -* DONE Change watched literal imp so that we only propagate assignments - CLOSED: [2008-02-22 Fri 11:37] -that have actually been made since the last iteration; this saves time. - -So unitProp (maybe rename bcp?) should take a list of literals to propagate, -and compute until that list is emptied -- sounds like a worklist algorithm! - -* TODO Implement SAT-MICRO annotated clauses and literals :ARCHIVE: -instead of using the current dl (decision list). - -* TODO Probably don't need the cnf :ARCHIVE: -and wch fields of the state. Probably can get away with some watcher. - -* DONE [#A] Make watched literals work as follows: - CLOSED: [2008-02-22 Fri 11:38] --- watcherMap: Map Lit [((Lit, Lit), Clause)] - -** When l first added to assignment (either decision or propagation): -if -l is watched, then for each clause associated with -l, look at -l's paired -literal, q. If q is undefined under the assignment, then: - - -- If q is a unit literal of this clause, assign q. - - -- If q is *not* a unit literal of this clause, stop watching -l and -starting watching some other literal of the clause. (Choose next by removing -everything in the assignment from the clause, then picking a random element.) - -Write this in terms of a list of newly-assigned literals, so one can recurse -at the end. - - -* DONE [#A] Change assignment representation to O(1) - CLOSED: [2008-02-13 Wed 21:59] -** DONE Lits to Int - CLOSED: [2008-02-02 Sat 11:55] -