diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -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] ... " + 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 } diff --git a/funsat.cabal b/funsat.cabal --- a/funsat.cabal +++ b/funsat.cabal @@ -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 diff --git a/src/Funsat/Circuit.hs b/src/Funsat/Circuit.hs --- a/src/Funsat/Circuit.hs +++ b/src/Funsat/Circuit.hs @@ -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 -- . 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 diff --git a/src/Funsat/Resolution.hs b/src/Funsat/Resolution.hs --- a/src/Funsat/Resolution.hs +++ b/src/Funsat/Resolution.hs @@ -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 diff --git a/src/Funsat/Solver.hs b/src/Funsat/Solver.hs --- a/src/Funsat/Solver.hs +++ b/src/Funsat/Solver.hs @@ -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)) diff --git a/src/Funsat/Types.hs b/src/Funsat/Types.hs --- a/src/Funsat/Types.hs +++ b/src/Funsat/Types.hs @@ -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 "" instance Show (STUArray s Var Double) where show = const "" instance Show (STArray s a b) where show = const "" + + +-- * 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) + diff --git a/src/Funsat/Types/Internal.hs b/src/Funsat/Types/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/Types/Internal.hs @@ -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 + diff --git a/src/Funsat/Utils.hs b/src/Funsat/Utils.hs --- a/src/Funsat/Utils.hs +++ b/src/Funsat/Utils.hs @@ -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) diff --git a/src/Funsat/Utils/Internal.hs b/src/Funsat/Utils/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Funsat/Utils/Internal.hs @@ -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 diff --git a/tests/Properties.hs b/tests/Properties.hs --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -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