funsat 0.5.2 → 0.6.0

raw patch · 24 files changed

+3232/−2948 lines, 24 filesdep +bimapdep ~QuickCheckdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: bimap

Dependency ranges changed: QuickCheck, base

API changes (from Hackage documentation)

Files

• CHANGES +4/−0
• Control/Monad/MonadST.hs +0/−51
• Funsat/FastDom.hs +0/−122
• Funsat/Monad.hs +0/−103
• Funsat/Resolution.hs +0/−274
• Funsat/Solver.hs +0/−1040
• Funsat/Types.hs +0/−317
• Funsat/Utils.hs +0/−281
• LICENSE +25/−160
• Main.hs +3/−12
• Text/Tabular.hs +0/−77
• bugs.org +0/−44
• funsat.cabal +30/−27
• src/Control/Monad/MonadST.hs +42/−0
• src/Funsat/Circuit.hs +814/−0
• src/Funsat/FastDom.hs +122/−0
• src/Funsat/Monad.hs +94/−0
• src/Funsat/Resolution.hs +284/−0
• src/Funsat/Solver.hs +1014/−0
• src/Funsat/Types.hs +333/−0
• src/Funsat/Utils.hs +272/−0
• src/Text/Tabular.hs +70/−0
• tests/Properties.hs +125/−192
• todo.org +0/−248

@@ -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.

@@ -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 <http://www.gnu.org/licenses/>.--    Copyright 2008 Denis Bueno--}----- | Idea from <http://haskell.org/pipermail/libraries/2003-September/001411.html>-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)-

@@ -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 <int-e@gmx.de>------ 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--}-

@@ -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 <http://www.gnu.org/licenses/>.--    Copyright 2008 Denis Bueno--}---{-|--The main SAT solver monad.  Embeds `ST'.  See type `SSTErrMonad', which stands-for ''State ST Error Monad''.---}-module Funsat.Monad-    ( liftST-    , runSSTErrMonad-    , evalSSTErrMonad-    , SSTErrMonad )-    where-import Control.Monad.Error-import Control.Monad.ST.Strict-import Control.Monad.State.Class-import Control.Monad.MonadST---instance MonadST s (SSTErrMonad e st s) where-    liftST = dpllST---- | Perform an @ST@ action in the DPLL monad.-dpllST :: ST s a -> SSTErrMonad e st s a-{-# INLINE dpllST #-}-dpllST st = SSTErrMonad (\k s -> st >>= \x -> k x s)---- | @runSSTErrMonad m s@ executes a `SSTErrMonad' action with initial state @s@--- until an error occurs or a result is returned.-runSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> (st -> ST s (Either e a, st))-runSSTErrMonad m = unSSTErrMonad m (\x s -> return (return x, s))--evalSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> st -> ST s (Either e a)-evalSSTErrMonad m s = do (result, _) <- runSSTErrMonad m s-                         return result---- | @SSTErrMonad e st s a@: the error type @e@, state type @st@, @ST@ thread--- @s@ and result type @a@.------ This is a monad embedding @ST@ and supporting error handling and state--- threading.  It uses CPS to avoid checking `Left' and `Right' for every--- `>>='; instead only checks on `catchError'. Idea adapted from--- <http://haskell.org/haskellwiki/Performance/Monads>.-newtype SSTErrMonad e st s a =-    SSTErrMonad { unSSTErrMonad :: forall r. (a -> (st -> ST s (Either e r, st)))-                                -> (st -> ST s (Either e r, st)) }--instance Monad (SSTErrMonad e st s) where-    return x = SSTErrMonad ($ x)-    (>>=)    = bindSSTErrMonad--bindSSTErrMonad :: SSTErrMonad e st s a -> (a -> SSTErrMonad e st s b)-                -> SSTErrMonad e st s b-{-# INLINE bindSSTErrMonad #-}-bindSSTErrMonad m f =-    {-# SCC "bindSSTErrMonad" #-}-    SSTErrMonad (\k -> unSSTErrMonad m (\a -> unSSTErrMonad (f a) k))--instance MonadState st (SSTErrMonad e st s) where-    get    = SSTErrMonad (\k s -> k s s)-    put s' = SSTErrMonad (\k _ -> k () s')--instance (Error e) => MonadError e (SSTErrMonad e st s) where-    throwError err =            -- throw away continuation-        SSTErrMonad (\_ s -> return (Left err, s))-    catchError action handler = {-# SCC "catchErrorSSTErrMonad" #-} SSTErrMonad-        (\k s -> do (x, s') <- runSSTErrMonad action s-                    case x of-                      Left error -> unSSTErrMonad (handler error) k s'-                      Right result -> k result s')--instance (Error e) => MonadPlus (SSTErrMonad e st s) where-    mzero     = SSTErrMonad (\_ s -> return (Left noMsg, s))-    mplus m n = SSTErrMonad (\k s ->-                                 do (r, s') <- runSSTErrMonad m s-                                    case r of-                                      Left _ -> unSSTErrMonad n k s'-                                      Right x -> k x s')

@@ -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 <http://www.gnu.org/licenses/>.--    Copyright 2008 Denis Bueno--}---- | Generates and checks a resolution proof of UNSAT from a resolution trace--- of a SAT solver (Funsat in particular will generate this trace).  This is--- based on the implementation discussed in the paper ''Validating SAT Solvers--- Using an Independent Resolution-Based Checker: Practical Implementations--- and Other Applications'' by Lintao Zhang and Sharad Malik.------ As a side effect of this process an /unsatisfiable core/ is generated from--- the resolution trace, as discussed in the paper ''Extracting Small--- Unsatisfiable Cores from Unsatisfiable Boolean Formula'' by Zhang and--- Malik.-module Funsat.Resolution-    ( -- * Interface-      checkDepthFirst-     -- * Data Types-    , ResolutionTrace(..)-    , initResolutionTrace-    , ResolutionError(..)-    , UnsatisfiableCore )-        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)

@@ -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 <http://www.gnu.org/licenses/>.--    Copyright 2008 Denis Bueno--}---import Control.Arrow( (&&&) )-import Control.Exception( assert )-import Control.Monad.Error hiding ( (>=>), forM_, runErrorT )-import Control.Monad.MonadST( MonadST(..) )-import Control.Monad.ST.Strict-import Control.Monad.State.Lazy hiding ( (>=>), forM_ )-import Data.Array.ST-import Data.Array.Unboxed-import Data.Foldable hiding ( sequence_ )-import Data.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)

@@ -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 <http://www.gnu.org/licenses/>.--    Copyright 2008 Denis Bueno--}------ | Data types used when dealing with SAT problems in funsat.-module Funsat.Types where---import Control.Monad.MonadST( MonadST(..) )-import Control.Monad.ST.Strict-import Data.Array.ST-import Data.Array.Unboxed-import Data.BitSet ( BitSet )-import Data.Foldable hiding ( sequence_ )-import Data.Map ( Map )-import Data.Set ( Set )-import 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 "<STRef>"-instance Show (STUArray s Var Int) where show = const "<STUArray Var Int>"-instance Show (STUArray s Var Double) where show = const "<STUArray Var Double>"-instance Show (STArray s a b) where show = const "<STArray>"

@@ -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 <http://www.gnu.org/licenses/>.--    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--

@@ -1,165 +1,30 @@-		   GNU LESSER GENERAL PUBLIC LICENSE-                       Version 3, 29 June 2007-- Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>- 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.

@@ -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 <http://www.gnu.org/licenses/>.+    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 -}

@@ -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 <http://www.gnu.org/licenses/>.--    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)--                  

@@ -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:

@@ -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 <dbueno@gmail.com> 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

@@ -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 <http://haskell.org/pipermail/libraries/2003-September/001411.html>+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)+

@@ -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+-- <http://okmij.org/ftp/Haskell/DSLSharing.hs>.+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 <http://www.gnu.org/licenses/>.++    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++

@@ -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 <int-e@gmx.de>+--+-- 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+-}+

@@ -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+-- <http://haskell.org/haskellwiki/Performance/Monads>.+newtype SSTErrMonad e st s a =+    SSTErrMonad { unSSTErrMonad :: forall r. (a -> (st -> ST s (Either e r, st)))+                                -> (st -> ST s (Either e r, st)) }++instance Monad (SSTErrMonad e st s) where+    return x = SSTErrMonad ($ x)+    (>>=)    = bindSSTErrMonad++bindSSTErrMonad :: SSTErrMonad e st s a -> (a -> SSTErrMonad e st s b)+                -> SSTErrMonad e st s b+{-# INLINE bindSSTErrMonad #-}+bindSSTErrMonad m f =+    {-# SCC "bindSSTErrMonad" #-}+    SSTErrMonad (\k -> unSSTErrMonad m (\a -> unSSTErrMonad (f a) k))++instance MonadState st (SSTErrMonad e st s) where+    get    = SSTErrMonad (\k s -> k s s)+    put s' = SSTErrMonad (\k _ -> k () s')++instance (Error e) => MonadError e (SSTErrMonad e st s) where+    throwError err =            -- throw away continuation+        SSTErrMonad (\_ s -> return (Left err, s))+    catchError action handler = {-# SCC "catchErrorSSTErrMonad" #-} SSTErrMonad+        (\k s -> do (x, s') <- runSSTErrMonad action s+                    case x of+                      Left error -> unSSTErrMonad (handler error) k s'+                      Right result -> k result s')++instance (Error e) => MonadPlus (SSTErrMonad e st s) where+    mzero     = SSTErrMonad (\_ s -> return (Left noMsg, s))+    mplus m n = SSTErrMonad (\k s ->+                                 do (r, s') <- runSSTErrMonad m s+                                    case r of+                                      Left _ -> unSSTErrMonad n k s'+                                      Right x -> k x s')

@@ -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)

@@ -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)

@@ -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 "<STRef>"+instance Show (STUArray s Var Int) where show = const "<STUArray Var Int>"+instance Show (STUArray s Var Double) where show = const "<STUArray Var Double>"+instance Show (STArray s a b) where show = const "<STArray>"

@@ -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++

@@ -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)++                  

@@ -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 <http://www.gnu.org/licenses/>.+    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 "<fcn>"  +-- ** 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

@@ -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]-