funsat 0.6.0 → 0.6.1
raw patch · 10 files changed
+765/−554 lines, 10 filesdep ~arraydep ~basedep ~containers
Dependency ranges changed: array, base, containers, fgl, mtl, pretty, random, time
Files
- Main.hs +136/−101
- funsat.cabal +41/−18
- src/Funsat/Circuit.hs +8/−2
- src/Funsat/Resolution.hs +1/−1
- src/Funsat/Solver.hs +85/−166
- src/Funsat/Types.hs +30/−35
- src/Funsat/Types/Internal.hs +95/−0
- src/Funsat/Utils.hs +8/−229
- src/Funsat/Utils/Internal.hs +332/−0
- tests/Properties.hs +29/−2
Main.hs view
@@ -14,146 +14,181 @@ import Control.Monad( when, forM_ ) import Data.Array.Unboxed( elems )-import Data.Foldable( fold, toList, elem )-import Data.List( intercalate )-import Data.Monoid-import Data.Set( Set )+import Data.List( intersperse )+import Data.Version( showVersion ) import Funsat.Solver ( solve , verify- , DPLLConfig(..) , defaultConfig , ShowWrapped(..) , statTable )-import Funsat.Types( CNF(..) )+import Funsat.Types( CNF(..), FunsatConfig(..), ConflictCut(..) )+import Paths_funsat( version ) import Prelude hiding ( elem ) import System.Console.GetOpt import System.Environment( getArgs ) import System.Exit( ExitCode(..), exitWith ) import Data.Time.Clock+ import qualified Data.Set as Set-import qualified Language.CNF.Parse.ParseDIMACS as ParseCNF+import qualified Language.CNF.Parse.ParseDIMACS as ParseDIMACS import qualified Text.Tabular as Tabular --#ifdef TESTING import qualified Properties-#endif -data Feature = WatchedLiterals- | ClauseLearning- | Restarts- | VSIDS- | ResolutionChecker- | UnsatCoreGeneration- deriving (Eq, Ord)-instance Show Feature where- show WatchedLiterals = "watched literals"- show ClauseLearning = "conflict clause learning"- show Restarts = "restarts"- show VSIDS = "dynamic variable ordering"- show ResolutionChecker = "resolution UNSAT checker"- show UnsatCoreGeneration = "UNSAT core generation"+options :: [OptDescr (Options -> Options)]+options =+ [ Option [] ["restart-at"]+ (ReqArg (\i o ->+ let c = optFunsatConfig o+ in o{ optFunsatConfig = c{configRestart = read i} }) "INT")+ (withDefault (configRestart . optFunsatConfig)+ "Restart after INT conflicts.") -allFeatures :: Set Feature-allFeatures = Set.fromList [WatchedLiterals, ClauseLearning, Restarts, VSIDS- ,ResolutionChecker, UnsatCoreGeneration]+ , Option [] ["restart-bump"]+ (ReqArg (\d o ->+ let c = optFunsatConfig o+ in o{ optFunsatConfig = c{configRestartBump = read d} }) "FLOAT")+ (withDefault (configRestartBump . optFunsatConfig)+ "Alter the number of conflicts required to restart by multiplying by FLOAT.") + , Option [] ["no-vsids"] (NoArg $ \o ->+ let c = optFunsatConfig o+ in o{ optFunsatConfig = c{configUseVSIDS = False} })+ "Use static variable ordering." -validOptions :: [OptDescr RunOptions]-validOptions =- [ Option [] ["no-vsids"] (NoArg $ disableF VSIDS)- "Use static variable ordering."- , Option [] ["no-restarts"] (NoArg $ disableF Restarts)- "Never restart."- , Option [] ["verify"] (NoArg RunTests)- "Run quickcheck properties and unit tests."- , Option [] ["print-features"] (NoArg (PrintFeatures Set.empty))- "Print the optimisations the SAT solver supports." ]+ , Option [] ["no-restarts"] (NoArg $ \o ->+ let c = optFunsatConfig o+ in o{ optFunsatConfig = c{configUseRestarts = False} })+ "Never restart." -disableF :: Feature -> RunOptions-disableF = Disable . Set.singleton+ , Option [] ["conflict-cut"]+ (ReqArg (\cut o ->+ let c = optFunsatConfig o+ in o{ optFunsatConfig = c{configCut = readCutOption cut} }) "1|d")+ "Which cut of the conflict graph to use for learning. 1=first UIP; d=decision lit" -data RunOptions = Disable (Set Feature) -- disable certain features- | RunTests -- run unit tests- | PrintFeatures (Set Feature) -- disable certain features--- Combines features, choosing only RunTests and PrintFeatures if present,--- otherwise combining sets of features to disable.-instance Monoid RunOptions where- mempty = Disable Set.empty- mappend (PrintFeatures f) (PrintFeatures f') = PrintFeatures (f `Set.union` f')- mappend (PrintFeatures f) (Disable f') = PrintFeatures (f `Set.union` f')- mappend o@(PrintFeatures _) _ = o- mappend o@RunTests _ = o- mappend (Disable s) (Disable s') = Disable (s `Set.union` s')- mappend (Disable _) o = o -- non-feature selection options override+ , Option [] ["verify"] (NoArg $ \o -> o{ optVerify = True })+ "Run quickcheck properties and unit tests." -parseOptions :: [String] -> IO (RunOptions, [FilePath])-parseOptions args = do- let (runoptionss, filepaths, errors) = getOpt RequireOrder validOptions args- when (not (null errors)) $ do { mapM_ putStr errors ;- putStrLn (usageInfo usageHeader validOptions) ;- exitWith (ExitFailure 1) }- return $ (fold runoptionss, filepaths)+ , Option [] ["profile"] (NoArg $ \o -> o{ optProfile = True })+ "Run solver. (assumes profiling build)" + , Option [] ["print-features"] (NoArg $ \o -> o{ optPrintFeatures = True })+ "Print the optimisations the SAT solver supports and exit."++ , Option [] ["version"] (NoArg $ \o -> o{ optVersion = True })+ "Print the version of funsat and exit."+ ]++data Options = Options+ { optVerify :: Bool+ , optProfile :: Bool+ , optPrintFeatures :: Bool+ , optFunsatConfig :: FunsatConfig+ , optVersion :: Bool }+ deriving (Show)+defaultOptions :: Options+defaultOptions = Options+ { optVerify = False+ , optProfile = False+ , optVersion = False+ , optPrintFeatures = False+ , optFunsatConfig = defaultConfig }++optUseVsids, optUseRestarts :: Options -> Bool+optUseVsids = configUseVSIDS . optFunsatConfig+optUseRestarts = configUseRestarts . optFunsatConfig++readCutOption ('1':_) = FirstUipCut+readCutOption ('d':_) = DecisionLitCut+readCutOption _ = error "error parsing cut option"++-- | Show default value of option at the end of the given string.+withDefault :: (Show v) => (Options -> v) -> String -> String+withDefault f s = s ++ " Default " ++ show (f defaultOptions) ++ "."++validateArgv :: [String] -> IO (Options, [FilePath])+validateArgv argv = do+ case getOpt Permute options argv of+ (o,n,[] ) -> return (foldl (flip ($)) defaultOptions o, n)+ (_,_,errs) -> ioError (userError (concat errs ++ usageInfo usageHeader options))++usageHeader :: String+usageHeader = "\nUsage: funsat [OPTION...] cnf-files..."+ main :: IO () main = do- (opts, files) <- getArgs >>= parseOptions- case opts of-#ifdef TESTING- RunTests -> Properties.main-#endif- PrintFeatures disabled ->- putStrLn $ intercalate ", " $ map show $- toList (allFeatures Set.\\ disabled)- Disable features -> do- putStr "Enabled features: "- putStrLn $ intercalate ", " $ map show $- toList (allFeatures Set.\\ features)- forM_ files $ parseAndSolve- where- parseAndSolve path = do- cnf <- parseCNF path- putStrLn $ show (numVars cnf) ++ " variables, "- ++ show (numClauses cnf) ++ " clauses"- Set.map seqList (clauses cnf)- `seq` putStrLn ("Solving " ++ path ++ "...")- startingTime <- getCurrentTime- let cfg =- (defaultConfig cnf)- { configUseVSIDS = not $ VSIDS `elem` features- , configUseRestarts = not $ Restarts `elem` features }- (solution, stats, rt) = solve cfg cnf- endingTime <- solution `seq` getCurrentTime- print solution- print $ statTable stats `Tabular.combine`- Tabular.mkTable- [[ WrapString "Real time "- , WrapString $ show (diffUTCTime endingTime startingTime)]]- putStr "Verifying solution..."- case verify solution rt cnf of- Just errorWitness ->- do putStrLn "\n--> VERIFICATION ERROR!"- print errorWitness- Nothing -> putStrLn "succeeded."+ (opts, files) <- getArgs >>= validateArgv+ when (optVerify opts) $ do+ Properties.main+ exitWith ExitSuccess + when (optProfile opts) $ do+ putStrLn "Solving ..."+ Properties.profile+ exitWith ExitSuccess -usageHeader = "Usage: funsat [options] <cnf-filename> ... <cnf-filename>"+ when (optVersion opts) $ do+ putStr "funsat "+ putStrLn (showVersion version)+ exitWith ExitSuccess + putStr "Feature config: "+ putStr . concat $ intersperse ", "+ [ if (optUseVsids opts) then "vsids" else "no vsids"+ , if (optUseRestarts opts) then "restarts" else "no restarts"+ , "unsat checking"+ ]+ putStr "\n"+ when (optPrintFeatures opts) $ exitWith ExitSuccess++ when (null files) $+ ioError (userError (usageInfo usageHeader options))++ forM_ files (parseAndSolve opts)+ where+ parseAndSolve opts path = do+ parseStart <- getCurrentTime+ cnf <- parseCNF path+ putStrLn $ show (numVars cnf) ++ " variables, "+ ++ show (numClauses cnf) ++ " clauses"+ Set.map seqList (clauses cnf)+ `seq` putStrLn ("Solving " ++ path ++ " ...")+ parseEnd <- getCurrentTime++ startingTime <- getCurrentTime+ let cfg = optFunsatConfig opts+ (solution, stats, rt) = solve cfg cnf+ endingTime <- solution `seq` getCurrentTime+ print solution+ print $ statTable stats `Tabular.combine`+ Tabular.mkTable+ [[ WrapString "Parsing time "+ , WrapString $ show (diffUTCTime parseEnd parseStart) ]+ ,[ WrapString "Real time "+ , WrapString $ show (diffUTCTime endingTime startingTime)]]+ putStr "Verifying solution..."+ case verify solution rt cnf of+ Just errorWitness ->+ do putStrLn "\n--> VERIFICATION ERROR!"+ print errorWitness+ Nothing -> putStrLn "succeeded."+ seqList l@[] = l seqList l@(x:xs) = x `seq` seqList xs `seq` l parseCNF :: FilePath -> IO CNF parseCNF path = do- result <- ParseCNF.parseFile path+ result <- ParseDIMACS.parseFile path case result of Left err -> error . show $ err Right c -> return . asCNF $ c -- | Convert parsed CNF to internal representation.-asCNF :: ParseCNF.CNF -> CNF-asCNF (ParseCNF.CNF v c is) =+asCNF :: ParseDIMACS.CNF -> CNF+asCNF (ParseDIMACS.CNF v c is) = CNF { numVars = v , numClauses = c , clauses = Set.fromList . map (map fromIntegral . elems) $ is }
funsat.cabal view
@@ -1,5 +1,5 @@ Name: funsat-Version: 0.6.0+Version: 0.6.1 Cabal-Version: >= 1.2 Description: @@ -30,10 +30,20 @@ Executable funsat Main-is: Main.hs Ghc-options: -funbox-strict-fields- -Wall -fwarn-tabs+ -Wall+ -fwarn-tabs -fno-warn-name-shadowing -fno-warn-orphans- Extensions: CPP, ScopedTypeVariables+ Extensions: CPP,+ BangPatterns,+ ScopedTypeVariables,+ TypeSynonymInstances,+ MultiParamTypeClasses,+ FunctionalDependencies,+ FlexibleInstances,+ FlexibleContexts++ CPP-options: -DTESTING Hs-source-dirs: . src tests Other-modules:@@ -43,45 +53,58 @@ Funsat.Resolution Funsat.Solver Funsat.Types+ Funsat.Types.Internal Funsat.Utils+ Funsat.Utils.Internal Text.Tabular Properties - Build-Depends: base,- random,- containers,- pretty,- mtl,- array,+ Build-Depends: base >= 3 && < 5,+ random < 2,+ containers >= 0.2 && < 0.3,+ pretty < 2,+ mtl >= 1 && < 2,+ array >= 0.2 && < 0.3, QuickCheck < 2, parse-dimacs >= 1.2 && < 2, bitset < 1, bimap >= 0.2 && < 0.3,- fgl,- time+ fgl >= 5 && <= 5.4.2.2,+ time < 1.2 Library+ Extensions: CPP,+ BangPatterns,+ ScopedTypeVariables,+ TypeSynonymInstances,+ MultiParamTypeClasses,+ FunctionalDependencies,+ FlexibleInstances,+ FlexibleContexts Exposed-modules: Control.Monad.MonadST Funsat.Circuit Funsat.Monad Funsat.Resolution Funsat.Solver Funsat.Types+ Funsat.Types.Internal Text.Tabular- Other-modules: Funsat.FastDom Funsat.Utils+ Funsat.Utils+ Funsat.Utils.Internal+ Other-modules: Funsat.FastDom Ghc-options: -funbox-strict-fields -Wall -fwarn-tabs -fno-warn-name-shadowing -fno-warn-orphans Extensions: CPP, ScopedTypeVariables Hs-source-dirs: src- Build-Depends: base,- containers,- pretty,- mtl,- array,+ Build-Depends: base >= 3 && < 5,+ containers >= 0.2 && < 0.3,+ pretty < 2,+ mtl >= 1 && < 2,+ array >= 0.2 && < 0.3, QuickCheck < 2, parse-dimacs >= 1.2 && < 2, bitset < 1, bimap >= 0.2 && < 0.3,- fgl+ fgl >= 5 && <= 5.4.2.2
src/Funsat/Circuit.hs view
@@ -5,6 +5,11 @@ -- class and various representations that admit efficient conversion to funsat -- CNF. --+-- The types in this class are more capable than simply being able to go from+-- (for example) an equality constraint to the CNF representation. In+-- particular, the `Shared' circuit type efficiently shares subterms,+-- potentially drastically reducing the memory require for the circuit.+-- -- The implementation for this module was adapted from -- <http://okmij.org/ftp/Haskell/DSLSharing.hs>. module Funsat.Circuit@@ -71,14 +76,15 @@ import Control.Monad.Reader-import Control.Monad.State.Lazy hiding ((>=>), forM_)+import Control.Monad.State.Strict 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 Funsat.Types( CNF(..), Lit(..), Var(..), var, lit, Solution(..), litSign )+import Funsat.Utils( litAssignment ) import Prelude hiding( not, and, or ) import qualified Data.Bimap as Bimap
src/Funsat/Resolution.hs view
@@ -43,7 +43,7 @@ import qualified Data.IntSet as IntSet import qualified Data.Map as Map import Funsat.Types-import Funsat.Utils( isSingle, getUnit, isFalseUnder )+import Funsat.Utils.Internal( isSingle, getUnit, isFalseUnder ) -- IDs = Ints
src/Funsat/Solver.hs view
@@ -1,28 +1,13 @@-{-# 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.+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 have taken pains 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@@ -31,6 +16,9 @@ Funsat will generate a minimal set of input clauses that are also unsatisfiable. +Another is the ability to compile high-level circuits into CNF. Seen the+"Funsat.Circuit" module.+ * 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.@@ -59,7 +47,7 @@ , verify , VerifyError(..) -- ** Configuration- , DPLLConfig(..)+ , FunsatConfig(..) , defaultConfig -- * Solver statistics , Stats(..)@@ -90,6 +78,7 @@ import Data.Array.ST import Data.Array.Unboxed import Data.Foldable hiding ( sequence_ )+import Data.Graph.Inductive.Tree import Data.Int( Int64 ) import Data.List( nub, tails, sortBy, sort ) import Data.Maybe@@ -99,8 +88,10 @@ -- import Debug.Trace (trace) import Funsat.Monad import Funsat.Utils+import Funsat.Utils.Internal import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace ) import Funsat.Types+import Funsat.Types.Internal import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) import Funsat.Resolution( ResolutionError(..) ) import Text.Printf( printf )@@ -118,7 +109,7 @@ -- 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 :: FunsatConfig -> 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.@@ -132,15 +123,15 @@ 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+ , propQ = Seq.empty, trail = [], level = undefined+ , stats = FunStats{numConfl = 0,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 :: MAssignment s -> FunMonad s (IAssignment, Bool) initialState m = do initialLevel <- liftST $ newSTUArray (V 1, V (numVars f)) noLevel modify $ \s -> s{ level = initialLevel }@@ -153,30 +144,30 @@ -- Watch each clause, making sure to bork if we find a contradiction. (`catchError`- (const $ liftST (unsafeFreezeAss m) >>= \a -> return (a,True))) $ do+ (const $ funFreeze 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)+ a <- funFreeze m return (a, False) -- | Solve with the default configuration `defaultConfig'. solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace)-solve1 f = solve (defaultConfig f) f+solve1 = solve defaultConfig -- | 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+-- conflict-based restarting (see `FunsatConfig').+stepToSolution :: MAssignment s -> FunMonad s Solution stepToSolution assignment = do step <- solveStep assignment useRestarts <- gets (configUseRestarts . dpllConfig) isTimeToRestart <- uncurry ((>=)) `liftM`- gets (numConfl &&& (configRestart . dpllConfig))+ gets ((numConfl . stats) &&& (configRestart . dpllConfig)) case step of Left m -> do when (useRestarts && isTimeToRestart) (do _stats <- extractStats@@ -187,20 +178,20 @@ Right s -> return s where resetState m = do- modify $ \s -> s{ numConfl = 0 }+ modify $ \s -> let st = stats s in s{ stats = st{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+ lvl <- gets level >>= funFreeze 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+ funFreeze m >>= simplifyDB -reportSolution :: Solution -> DPLLMonad s (Solution, Stats, Maybe ResolutionTrace)+reportSolution :: Solution -> FunMonad s (Solution, Stats, Maybe ResolutionTrace) reportSolution s = do stats <- extractStats case s of@@ -210,15 +201,6 @@ 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@@ -228,11 +210,12 @@ -- * 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 }+defaultConfig :: FunsatConfig+defaultConfig = Cfg { configRestart = 100 -- fromIntegral $ max (numVars f `div` 10) 100+ , configRestartBump = 1.5+ , configUseVSIDS = True+ , configUseRestarts = True+ , configCut = FirstUipCut } -- * Preprocessing @@ -247,7 +230,7 @@ -- `preprocessCNF'. -- -- Precondition: decision level 0.-simplifyDB :: IAssignment -> DPLLMonad s ()+simplifyDB :: IAssignment -> FunMonad 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.@@ -269,15 +252,15 @@ -- 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 :: MAssignment s -> FunMonad s (Either (MAssignment s) Solution) solveStep m = do- unsafeFreezeAss m >>= solveStepInvariants+ funFreeze m >>= solveStepInvariants conf <- gets dpllConfig let selector = if configUseVSIDS conf then select else selectStatic maybeConfl <- bcp m- mFr <- unsafeFreezeAss m+ mFr <- funFreeze m voArr <- gets (varOrderArr . varOrder)- voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze voArr)+ voFr <- FrozenVarOrder `liftM` funFreeze voArr s <- get stepForward $ -- Check if unsat.@@ -288,18 +271,18 @@ >< selector mFr voFr >=> decide m where -- Take the step chosen by the transition guards above.- stepForward Nothing = (Right . Sat) `liftM` unsafeFreezeAss m+ stepForward Nothing = (Right . Sat) `liftM` funFreeze m stepForward (Just step) = do r <- step case r of- Nothing -> (Right . Unsat) `liftM` liftST (unsafeFreezeAss m)+ Nothing -> (Right . Unsat) `liftM` funFreeze 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 :: Maybe (Lit, Clause, ClauseId) -> FunMonad s (Maybe a) postProcessUnsat maybeConfl = do traceClauseId $ (thd . fromJust) maybeConfl return Nothing@@ -308,7 +291,7 @@ -- | Check data structure invariants. Unless @-fno-ignore-asserts@ is passed, -- this should be optimised away to nothing.-solveStepInvariants :: IAssignment -> DPLLMonad s ()+solveStepInvariants :: IAssignment -> FunMonad s () {-# INLINE solveStepInvariants #-} solveStepInvariants _m = assert True $ do s <- get@@ -324,55 +307,6 @@ 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 @@ -385,7 +319,7 @@ -- watched literals. bcpLit :: MAssignment s -> Lit -- ^ Assigned literal which might propagate.- -> DPLLMonad s (Maybe (Lit, Clause, ClauseId))+ -> FunMonad s (Maybe (Lit, Clause, ClauseId)) bcpLit m l = do ws <- gets watches ; ls <- gets learnt clauses <- liftST $ readArray ws l@@ -410,7 +344,7 @@ {-# INLINE updateWatches #-} updateWatches _ [] = return () updateWatches alter (annCl@(watchRef, c, cid) : restClauses) = do- mFr <- unsafeFreezeAss m+ mFr :: IAssignment <- funFreeze 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.@@ -424,7 +358,7 @@ alter (annCl:) (negate l') Nothing -> do -- all other lits false, clause is unit- modify $ \s -> s{ numImpl = numImpl s + 1 }+ incNumImpl alter (annCl:) l isConsistent <- enqueue m (negate q) (Just (c, cid)) when (not isConsistent) $ do -- unit literal is conflicting@@ -434,7 +368,7 @@ -- | 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 :: MAssignment s -> FunMonad s (Maybe (Lit, Clause, ClauseId)) bcp m = do q <- gets propQ if Seq.null q then return Nothing@@ -462,13 +396,13 @@ -- | 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 :: MAssignment s -> Var -> FunMonad 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 }+ incNumDecisions+ modify $ \s -> s{ dl = ld:dl } enqueue m ld Nothing return $ Just m @@ -476,13 +410,13 @@ -- *** Backtracking --- | Non-chronological backtracking. The current returns the learned clause--- implied by the first unique implication point cut of the conflict graph.+-- | 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))+ -> FunMonad s (Maybe (MAssignment s)) backJump m c@(_, _conflict, _) = get >>= \(SC{dl=dl, reason=_reason}) -> do _theTrail <- gets trail -- trace ("********** conflict = " ++ show c) $ return ()@@ -490,57 +424,43 @@ -- 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+ incNumConfl ; incNumConflTotal+ levelArr <- do s <- get+ funFreeze (level s)+ (learntCl, learntClId, newLevel) <- analyse m 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+ mFr <- funFreeze 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+ mFr <- funFreeze m 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)+analyse :: MAssignment s -> FrozenLevelArray -> [Lit] -> (Lit, Clause, ClauseId)+ -> FunMonad 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 ()+analyse m levelArr dlits (cLit, cClause, cCid) = do+ conf <- gets dpllConfig+ mFr <- funFreeze m+ st <- get+ -- let conflGraph = mkConflGraph mFr levelArr (reason st) dlits (cLit, cClause)+ -- :: ConflictGraph Gr -- trace ("graphviz graph:\n" ++ graphviz' conflGraph) $ return () -- trace ("cut: " ++ show firstUIPCut) $ return () -- trace ("topSort: " ++ show topSortNodes) $ return ()@@ -548,15 +468,17 @@ -- 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 ()+ a <- case configCut conf of+ FirstUipCut -> firstUIPBFS m (numVars . cnf $ st) (reason st)+ DecisionLitCut -> error "decisionlitcut unimplemented"+ -- let lastDecision = fromMaybe $ find (\+-- trace ("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)+ -> FunMonad s (Clause, ClauseId, Int) firstUIPBFS m nVars reasonMap = do resolveSourcesR <- liftST $ newSTRef [] -- trace sources let addResolveSource clauseId =@@ -631,7 +553,7 @@ -- assignment, sets `noLevel', undoes reason. -- -- Does /not/ touch `dl'.-undoOne :: MAssignment s -> DPLLMonad s ()+undoOne :: MAssignment s -> FunMonad s () {-# INLINE undoOne #-} undoOne m = do trl <- gets trail@@ -646,7 +568,7 @@ , reason = Map.delete (var l) (reason s) } -- | Increase the recorded activity of given variable.-bump :: Var -> DPLLMonad s ()+bump :: Var -> FunMonad s () {-# INLINE bump #-} bump v = varOrderMod v (+ varInc) @@ -677,7 +599,7 @@ -- *** Clause compaction -- | Keep the smaller half of the learned clauses.-compactDB :: DPLLMonad s ()+compactDB :: FunMonad s () compactDB = do n <- numVars `liftM` gets cnf lArr <- gets learnt@@ -707,7 +629,7 @@ watchClause :: MAssignment s -> (Clause, ClauseId) -> Bool -- ^ Is this clause learned?- -> DPLLMonad s Bool+ -> FunMonad s Bool {-# INLINE watchClause #-} watchClause m (c, cid) isLearnt = do case c of@@ -744,11 +666,11 @@ -> Maybe (Clause, ClauseId) -- ^ The reason for enqueuing the literal. Including a -- non-@Nothing@ value here adjusts the `reason' map.- -> DPLLMonad s Bool+ -> FunMonad s Bool {-# INLINE enqueue #-} -- enqueue _m l _r | trace ("enqueue " ++ show l) $ False = undefined enqueue m l r = do- mFr <- unsafeFreezeAss m+ mFr <- funFreeze m case l `statusUnder` mFr of Right b -> return b -- conflict/already assigned Left () -> do@@ -763,7 +685,7 @@ return True -- | Pop the `propQ'. Error (crash) if it is empty.-dequeue :: DPLLMonad s Lit+dequeue :: FunMonad s Lit {-# INLINE dequeue #-} dequeue = do q <- gets propQ@@ -774,14 +696,14 @@ return top -- | Clear the `propQ'.-clearQueue :: DPLLMonad s ()+clearQueue :: FunMonad 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 :: Var -> (Double -> Double) -> FunMonad s () varOrderMod v f = do vo <- varOrderArr `liftM` gets varOrder vActivity <- liftST $ readArray vo v@@ -816,7 +738,7 @@ -- | Generate a new clause identifier (always unique).-nextTraceId :: DPLLMonad s Int+nextTraceId :: FunMonad s Int nextTraceId = do counter <- gets (resTraceIdCount . resolutionTrace) modifySlot resolutionTrace $ \s rt ->@@ -824,7 +746,7 @@ return $! counter -- | Add the given clause id to the trace.-traceClauseId :: ClauseId -> DPLLMonad s ()+traceClauseId :: ClauseId -> FunMonad s () traceClauseId cid = do modifySlot resolutionTrace $ \s rt -> s{resolutionTrace = rt{ resTrace = [cid] }}@@ -957,10 +879,10 @@ ++ " lits/clause)"]]) -extractStats :: DPLLMonad s Stats+extractStats :: FunMonad s Stats extractStats = do- s <- get- learntArr <- liftST $ unsafeFreezeWatchArray (learnt s)+ s <- gets stats+ learntArr <- get >>= funFreeze . learnt let learnts = (nub . Fl.concat) [ map (sort . (\(_,c,_) -> c)) (learntArr!i) | i <- (range . bounds) learntArr ] :: [Clause]@@ -975,11 +897,8 @@ , statsNumImpl = numImpl s } return stats -unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s])-unsafeFreezeWatchArray = freeze --constructResTrace :: Solution -> DPLLMonad s ResolutionTrace+constructResTrace :: Solution -> FunMonad s ResolutionTrace constructResTrace sol = do s <- get watchesIndices <- range `liftM` liftST (getBounds (watches s))
src/Funsat/Types.hs view
@@ -25,17 +25,15 @@ 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.Int( Int64 ) 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@@ -108,7 +106,7 @@ -- | 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)+data Solution = Sat !IAssignment | Unsat !IAssignment deriving (Eq) instance Show Solution where show (Sat a) = "satisfiable: " ++ showAssignment a@@ -193,37 +191,6 @@ -- | 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).@@ -242,6 +209,14 @@ -- assignment) and decision level. The only reason we make a new datatype for -- this is for its `Show' instance. data CGNodeAnnot = CGNA Lit Int++-- | Just a graph with special node annotations.+type ConflictGraph g = g CGNodeAnnot ()++-- | The lambda node is connected exactly to the two nodes causing the conflict.+cgLambda :: CGNodeAnnot+cgLambda = CGNA (L 0) (-1)+ instance Show CGNodeAnnot where show (CGNA (L 0) _) = "lambda" show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")"@@ -331,3 +306,23 @@ 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>"+++-- * Configuration++-- | A choice of conflict graph cut for learning clauses.+data ConflictCut = FirstUipCut+ | DecisionLitCut+ deriving (Show)++-- | Configuration parameters for the solver.+data FunsatConfig = 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+ , configCut :: !ConflictCut+ }+ deriving (Show)+
+ src/Funsat/Types/Internal.hs view
@@ -0,0 +1,95 @@+{-| Types used internally by funsat. -}+module Funsat.Types.Internal+ ( FunsatState(..)+ , FunMonad+ , FunStats(..)+ , incNumConfl+ , incNumConflTotal+ , incNumImpl+ , incNumDecisions+ , FunsatConfig(..) )+ 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.Monad.State( modify )+import Data.Int( Int64 )+import Data.Sequence( Seq )+-- import Debug.Trace (trace)+import Funsat.Monad+import Funsat.Types+import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum )+import qualified Data.Sequence as Seq++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 `Funsat.Solver.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.++ , varOrder :: VarOrder s++ , resolutionTrace :: PartialResolutionTrace++ , dpllConfig :: FunsatConfig++ , stats :: FunStats } deriving Show++data FunStats =+ FunStats+ { 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).+ } deriving (Eq, Ord, Show)++incNumConfl, incNumConflTotal, incNumImpl, incNumDecisions :: FunMonad s ()+incNumConfl = modify $ \s ->+ let st = stats s in s{ stats = st{numConfl = numConfl st + 1} }+incNumConflTotal = modify $ \s ->+ let st = stats s in s{ stats = st{numConflTotal = numConflTotal st + 1} }+incNumImpl = modify $ \s -> + let st = stats s in s{ stats = st{numImpl = numImpl st + 1} }+incNumDecisions = modify $ \s ->+ let st = stats s in s{ stats = st{numDecisions = numDecisions st + 1} }+++-- | 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 FunMonad s = SSTErrMonad (Lit, Clause, ClauseId) (FunsatState s) s+
src/Funsat/Utils.hs view
@@ -16,7 +16,7 @@ {-| -Generic utilities that happen to be used in the SAT solver.+Utilities. -} module Funsat.Utils where@@ -28,8 +28,7 @@ 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 Data.Set( Set ) import Debug.Trace( trace ) import Funsat.Types import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum )@@ -44,229 +43,9 @@ --- | `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--+-- | 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)
+ src/Funsat/Utils/Internal.hs view
@@ -0,0 +1,332 @@+{-# LANGUAGE MultiParamTypeClasses #-}++{-+ 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.Internal where++import Control.Monad.MonadST( MonadST, liftST )+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.Set( Set )+import Debug.Trace( trace )+import Funsat.Types+import Funsat.Types.Internal( FunMonad )+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+++class FunFreeze t e f | t -> f where+ funFreeze :: (MArray t e (ST s), Ix i, IArray f e) =>+ t i e -> FunMonad s (f i e)+ funThaw :: (MArray t e (ST s), Ix i, IArray f e) =>+ f i e -> FunMonad s (t i e)+instance FunFreeze (STUArray s) Int UArray where+ {-# INLINE funFreeze #-}+ funFreeze = liftST . unsafeFreeze+ {-# INLINE funThaw #-}+ funThaw = liftST . unsafeThaw++instance FunFreeze (STUArray s) Double UArray where+ {-# INLINE funFreeze #-}+ funFreeze = liftST . unsafeFreeze+ {-# INLINE funThaw #-}+ funThaw = liftST . unsafeThaw++instance FunFreeze (STArray s) [WatchedPair s] Array where+ {-# INLINE funFreeze #-}+ funFreeze = liftST . freeze+ {-# INLINE funThaw #-}+ funThaw = liftST . thaw++{-+-- | 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+++-- | `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. There is also a distinguished /lambda/ node, as used by Sabharwal+-- when he explains conflict graphs.+--+-- Useful for getting pretty graphviz output of a conflict.+mkConflGraph :: DynGraph g =>+ IAssignment+ -> FrozenLevelArray+ -> ReasonMap+ -> [Lit] -- ^ the trail (decision lits, in rev. chron. order)+ -> (Lit, Clause) -- ^ conflicting literal and reason clause+ -> ConflictGraph g+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, cgLambda) :) $+ ((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+ fst (Map.findWithDefault ([],undefined) (var lit) reasonMap)+ `without` lit+ filterReason = filter ( ((var lit /=) . var) .&&.+ ((<= litLevel lit) . litLevel) )+ seen' = seen `with` litNode lit+ litLevel l = if l == cLit then numDlits else lev!(var l)+ numDlits = length _dlits+ litNode l = -- lit to node+ if var l == var cLit -- preserve sign of conflicting lit+ then unLit l+ else (abs . unLit) l+++++-- | @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
tests/Properties.hs view
@@ -26,7 +26,7 @@ import Funsat.Circuit hiding( Circuit(..) ) import Funsat.Circuit( Circuit(input,true,false,ite,xor,onlyif) ) import Funsat.Types-import Funsat.Utils+import Funsat.Utils.Internal import Language.CNF.Parse.ParseDIMACS( parseFile ) import Prelude hiding ( or, and, all, any, elem, minimum, foldr, splitAt, concatMap, sum, concat ) import Funsat.Resolution( ResolutionTrace(..) )@@ -87,6 +87,33 @@ check resChkConfig prop_resolutionChecker +profile :: IO ()+profile = do+ -- hPutStr stderr "prop_circuitToCnf: " >> check config prop_circuitToCnf++ -- 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.@@ -101,7 +128,7 @@ classify (numClauses cnf > 15 || numVars cnf > 10) "c>15, v>10" $ classify (numClauses cnf > 30 || numVars cnf > 20) "c>30, v>20" $ classify (numVars cnf > 20) "c>30, v>30" $- case solve (defaultConfig cnf) cnf of+ case solve defaultConfig cnf of (Sat m,_,rt) -> label "SAT" $ verifyBool (Sat m) rt cnf (Unsat _,_,rt) -> label "UNSAT" $ case Resolution.checkDepthFirst (fromJust rt) of