diff --git a/SAT/Mios.hs b/SAT/Mios.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios.hs @@ -0,0 +1,297 @@ +-- | Minisat-based Implementation and Optimization Study on SAT solver +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Mios + ( + -- * Interface to the core of solver + versionId + , CNFDescription (..) + , module SAT.Mios.OptionParser + , runSolver + , solveSAT + , solveSATWithConfiguration + , solve + , getModel + -- * Assignment Validator + , validateAssignment + , validate + -- * For standalone programs + , executeSolverOn + , executeSolver + , executeValidatorOn + , executeValidator + -- * File IO + , dumpAssigmentAsCNF + ) + where + +import Control.Monad ((<=<), unless, void, when) +import Data.Char +import qualified Data.ByteString.Char8 as B +import Data.List +import Numeric (showFFloat) +import System.CPUTime +import System.Exit +import System.IO + +import SAT.Mios.Types +import SAT.Mios.Internal +import SAT.Mios.Solver +import SAT.Mios.Main +import SAT.Mios.OptionParser +import SAT.Mios.Validator + +reportElapsedTime :: Bool -> String -> Integer -> IO Integer +reportElapsedTime False _ _ = return 0 +reportElapsedTime _ _ 0 = getCPUTime +reportElapsedTime _ mes t = do + now <- getCPUTime + let toSecond = 1000000000000 :: Double + hPutStr stderr mes + hPutStrLn stderr $ showFFloat (Just 3) ((fromIntegral (now - t)) / toSecond) " sec" + return now + +-- | executes a solver on the given CNF file +-- This is the simplest entry to standalone programs; not for Haskell programs +executeSolverOn :: FilePath -> IO () +executeSolverOn path = executeSolver (miosDefaultOption { _targetFile = Just path }) + +-- | executes a solver on the given 'arg :: MiosConfiguration' +-- | This is another entry point for standalone programs. +executeSolver :: MiosProgramOption -> IO () +executeSolver opts@(_targetFile -> target@(Just cnfFile)) = do + t0 <- reportElapsedTime (_confTimeProbe opts) "" 0 + (desc, cls) <- parseHeader target <$> B.readFile cnfFile + when (_numberOfVariables desc == 0) $ error $ "couldn't load " ++ show cnfFile + s <- newSolver (toMiosConf opts) desc + parseClauses s desc cls + t1 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Parse: ") t0 + when (_confVerbose opts) $ do + nc <- nClauses s + hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (nVars s, _numberOfVariables desc) ++ " #c = " ++ show (nc, _numberOfClauses desc) + res <- simplifyDB s + -- when (_confVerbose opts) $ hPutStrLn stderr $ "`simplifyDB`: " ++ show res + result <- if res then solve s [] else return False + case result of + True | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "SATISFIABLE" + False | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "UNSATISFIABLE" + True -> print =<< getModel s + False -> do -- contradiction + -- FIXMEin future + when (_confVerbose opts) $ hPutStrLn stderr "UNSAT" + -- print =<< map lit2int <$> asList (conflict s) + putStrLn "[]" + case _outputFile opts of + Just fname -> dumpAssigmentAsCNF fname result =<< getModel s + Nothing -> return () + t2 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Solve: ") t1 + when (result && _confCheckAnswer opts) $ do + asg <- getModel s + s' <- newSolver (toMiosConf opts) desc + parseClauses s' desc cls + good <- validate s' asg + if _confVerbose opts + then hPutStrLn stderr $ if good then "A vaild answer" else "Internal error: mios returns a wrong answer" + else unless good $ hPutStrLn stderr "Internal error: mios returns a wrong answer" + void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Validate: ") t2 + void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0 + when (_confStatProbe opts) $ do + hPutStr stderr $ "## [" ++ showPath cnfFile ++ "] " + hPutStrLn stderr . intercalate ", " . map (\(k, v) -> show k ++ ": " ++ show v) =<< getStats s + +executeSolver _ = return () + +-- | new top-level interface that returns +-- +-- * conflicting literal set :: Left [Int] +-- * satisfiable assignment :: Right [Int] +-- +runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int]) +runSolver m d c = do + s <- newSolver m d + mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) c + noConf <- simplifyDB s + if noConf + then do + x <- solve s [] + if x + then Right <$> getModel s + else Left . map lit2int <$> asList (conflict s) + else return $ Left [] + + +-- | the easiest interface for Haskell programs +-- This returns the result @::[[Int]]@ for a given @(CNFDescription, [[Int]])@ +-- The first argument @target@ can be build by @Just target <- cnfFromFile targetfile@. +-- The second part of the first argument is a list of vector, which 0th element is the number of its real elements +solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int] +solveSAT = solveSATWithConfiguration defaultConfiguration + +-- | solves the problem (2rd arg) under the configuration (1st arg) +-- and returns an assignment as list of literals :: Int +solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int] +solveSATWithConfiguration conf desc cls = do + s <- newSolver conf desc + -- mapM_ (const (newVar s)) [0 .. _numberOfVariables desc - 1] + mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) cls + noConf <- simplifyDB s + if noConf + then do + result <- solve s [] + if result + then getModel s + else return [] + else return [] + +-- | validates a given assignment from STDIN for the CNF file (2nd arg) +-- this is the entry point for standalone programs +executeValidatorOn :: FilePath -> IO () +executeValidatorOn path = executeValidator (miosDefaultOption { _targetFile = Just path }) + +-- | validates a given assignment for the problem (2nd arg) +-- this is another entry point for standalone programs; see app/mios.hs +executeValidator :: MiosProgramOption -> IO () +executeValidator opts@(_targetFile -> target@(Just cnfFile)) = do + (desc, cls) <- parseHeader target <$> B.readFile cnfFile + when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ show cnfFile + s <- newSolver (toMiosConf opts) desc + parseClauses s desc cls + when (_confVerbose opts) $ + hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (_numberOfVariables desc) ++ " #c = " ++ show (_numberOfClauses desc) + when (_confVerbose opts) $ do + nc <- nClauses s + nl <- nLearnts s + hPutStrLn stderr $ "(nv, nc, nl) = " ++ show (nVars s, nc, nl) + asg <- read <$> getContents + unless (_confNoAnswer opts) $ print asg + result <- s `validate` (asg :: [Int]) + if result + then putStrLn ("It's a valid assignment for " ++ cnfFile ++ ".") >> exitSuccess + else putStrLn ("It's an invalid assignment for " ++ cnfFile ++ ".") >> exitFailure + +executeValidator _ = return () + +-- | returns True if a given assignment (2nd arg) satisfies the problem (1st arg) +-- if you want to check the @answer@ which a @slover@ returned, run @solver `validate` answer@, +-- where 'validate' @ :: Traversable t => Solver -> t Lit -> IO Bool@ +validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool +validateAssignment desc cls asg = do + s <- newSolver defaultConfiguration desc + mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) cls + s `validate` asg + +-- | dumps an assigment to file. +-- 2nd arg is +-- +-- * @True@ if the assigment is satisfiable assigment +-- +-- * @False@ if not +-- +-- >>> do y <- solve s ... ; dumpAssigmentAsCNF "result.cnf" y <$> model s +-- +dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO () +dumpAssigmentAsCNF fname False _ = do + withFile fname WriteMode $ \h -> do + hPutStrLn h "UNSAT" + +dumpAssigmentAsCNF fname True l = do + withFile fname WriteMode $ \h -> do + hPutStrLn h "SAT" + hPutStrLn h . unwords $ map show l + +-------------------------------------------------------------------------------- +-- DIMACS CNF Reader +-------------------------------------------------------------------------------- + +parseHeader :: Maybe FilePath -> B.ByteString -> (CNFDescription, B.ByteString) +parseHeader target bs = if B.head bs == 'p' then (parseP l, B.tail bs') else parseHeader target (B.tail bs') + where + (l, bs') = B.span ('\n' /=) bs + -- format: p cnf n m, length "p cnf" == 5 + parseP line = case B.readInt $ B.dropWhile (`elem` " \t") (B.drop 5 line) of + Just (x, second) -> case B.readInt (B.dropWhile (`elem` " \t") second) of + Just (y, _) -> CNFDescription x y target + _ -> CNFDescription 0 0 target + _ -> CNFDescription 0 0 target + +parseClauses :: Solver -> CNFDescription -> B.ByteString -> IO () +parseClauses s (CNFDescription nv nc _) bs = do + let maxLit = int2lit $ negate nv + buffer <- newVec $ maxLit + 1 + polvec <- newVecBool (maxLit + 1) False + let + loop :: Int -> B.ByteString -> IO () + loop ((< nc) -> False) _ = return () + loop i b = loop (i + 1) =<< readClause s buffer polvec b + loop 0 bs + -- static polarity + let + asg = assigns s + checkPolarity :: Int -> IO () + checkPolarity ((< nv) -> False) = return () + checkPolarity v = do + p <- getNthBool polvec $ var2lit v True + n <- getNthBool polvec $ var2lit v False + when (p == False || n == False) $ setNth asg v $ if p then lTrue else lFalse + checkPolarity $ v + 1 + checkPolarity 1 + +skipWhitespace :: B.ByteString -> B.ByteString +skipWhitespace s + | elem c " \t\n" = skipWhitespace $ B.tail s + | otherwise = s + where + c = B.head s + +-- | skip comment lines +-- __Pre-condition:__ we are on the benngining of a line +skipComments :: B.ByteString -> B.ByteString +skipComments s + | c == 'c' = skipComments . B.tail . B.dropWhile (/= '\n') $ s + | otherwise = s + where + c = B.head s + +parseInt :: B.ByteString -> (Int, B.ByteString) +parseInt st = do + let + zero = ord '0' + loop :: B.ByteString -> Int -> (Int, B.ByteString) + loop s val = case B.head s of + c | '0' <= c && c <= '9' -> loop (B.tail s) (val * 10 + ord c - zero) + _ -> (val, B.tail s) + case B.head st of + '-' -> let (k, x) = loop (B.tail st) 0 in (negate k, x) + '+' -> loop st (0 :: Int) + c | '0' <= c && c <= '9' -> loop st 0 + _ -> error "PARSE ERROR! Unexpected char" + +readClause :: Solver -> Vec -> VecBool -> B.ByteString -> IO B.ByteString +readClause s buffer pvec stream = do + let + loop :: Int -> B.ByteString -> IO B.ByteString + loop i b = do + let (k, b') = parseInt $ skipWhitespace b + if k == 0 + then do + -- putStrLn . ("clause: " ++) . show . map lit2int =<< asList stack + setNth buffer 0 $ i - 1 + addClause s buffer + return b' + else do + let l = int2lit k + setNth buffer i l + setNthBool pvec l True + loop (i + 1) b' + loop 1 . skipComments . skipWhitespace $ stream + + +showPath :: FilePath -> String +showPath str + | elem '/' str = take (len - length basename) (repeat ' ') ++ basename + | otherwise = take (len - length basename') (repeat ' ') ++ basename' + where + len = 50 + basename = reverse . takeWhile (/= '/') . reverse $ str + basename' = take len str diff --git a/SAT/Mios/Clause.hs b/SAT/Mios/Clause.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Clause.hs @@ -0,0 +1,144 @@ +{-# LANGUAGE + BangPatterns + , FlexibleInstances + , MagicHash + , MultiParamTypeClasses + , RecordWildCards + , ViewPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +-- | Clause, supporting pointer-based equality +module SAT.Mios.Clause + ( + Clause (..) +-- , isLit +-- , getLit + , shrinkClause + , newClauseFromVec + , sizeOfClause + -- * Vector of Clause + , ClauseVector + , newClauseVector + , getNthClause + , setNthClause + , swapClauses + ) + where + +import Control.Monad (forM_) +import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#) +import qualified Data.Vector as V +import qualified Data.Vector.Mutable as MV +import qualified Data.Vector.Unboxed.Mutable as UV +import Data.List (intercalate) +import SAT.Mios.Types + +-- | __Fig. 7.(p.11)__ +-- clause, null, binary clause. +-- This matches both of @Clause@ and @GClause@ in MiniSat +-- TODO: GADTs is better? +data Clause = Clause + { + learnt :: !Bool -- ^ whether this is a learnt clause +-- , rank :: !IntSingleton -- ^ goodness like LBD; computed in 'Ranking' + , activity :: !DoubleSingleton -- ^ activity of this clause + , protected :: !BoolSingleton -- ^ protected from reduce + , lits :: !Vec -- ^ which this clause consists of + } + | NullClause -- as null pointer +-- | BinaryClause Lit -- binary clause consists of only a propagating literal + +-- | The equality on 'Clause' is defined with 'reallyUnsafePtrEquality'. +instance Eq Clause where + {-# SPECIALIZE INLINE (==) :: Clause -> Clause -> Bool #-} + (==) x y = x `seq` y `seq` tagToEnum# (reallyUnsafePtrEquality# x y) + +instance Show Clause where + show NullClause = "NullClause" + show _ = "a clause" + +-- | supports a restricted set of 'VectorFamily' methods +instance VectorFamily Clause Lit where + dump mes NullClause = return $ mes ++ "Null" + dump mes Clause{..} = do + a <- show <$> getDouble activity + (len:ls) <- asList lits + return $ mes ++ "C" ++ show len ++ "{" ++ intercalate "," [show learnt, a, show . map lit2int . take len $ ls] ++ "}" + {-# SPECIALIZE INLINE asVec :: Clause -> Vec #-} + asVec Clause{..} = UV.unsafeTail lits + {-# SPECIALIZE INLINE asList :: Clause -> IO [Int] #-} + asList NullClause = return [] + asList Clause{..} = do + (n : ls) <- asList lits + return $ take n ls + +-- returns True if it is a 'BinaryClause' +-- FIXME: this might be discarded in minisat 2.2 +-- isLit :: Clause -> Bool +-- isLit (BinaryClause _) = True +-- isLit _ = False + +-- returns the literal in a BinaryClause +-- FIXME: this might be discarded in minisat 2.2 +-- getLit :: Clause -> Lit +-- getLit (BinaryClause x) = x + +-- coverts a binary clause to normal clause in order to reuse map-on-literals-in-a-clause codes +-- liftToClause :: Clause -> Clause +-- liftToClause (BinaryClause _) = error "So far I use generic function approach instead of lifting" + +-- | copies /vec/ and return a new 'Clause' +-- Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically. +{-# INLINE newClauseFromVec #-} +newClauseFromVec :: Bool -> Vec -> IO Clause +newClauseFromVec l vec = do + n <- getNth vec 0 + v <- newVec $ n + 1 + forM_ [0 .. n] $ \i -> setNth v i =<< getNth vec i + Clause l <$> {- newInt 0 <*> -} newDouble 0 <*> newBool False <*> return v + +-- | returns the number of literals in a clause, even if the given clause is a binary clause +{-# INLINE sizeOfClause #-} +sizeOfClause :: Clause -> IO Int +-- sizeOfClause (BinaryClause _) = return 1 +sizeOfClause !c = getNth (lits c) 0 + +-- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals +{-# INLINABLE shrinkClause #-} +shrinkClause :: Int -> Clause -> IO () +shrinkClause n !c = modifyNth (lits c) (subtract n) 0 + +-------------------------------------------------------------------------------- + +-- | Mutable 'Clause' Vector +type ClauseVector = MV.IOVector Clause + +instance VectorFamily ClauseVector Clause where + asList cv = V.toList <$> V.freeze cv + dump mes cv = do + l <- asList cv + sts <- mapM (dump ",") (l :: [Clause]) + return $ mes ++ tail (concat sts) + +-- | returns a new 'ClauseVector' +newClauseVector :: Int -> IO ClauseVector +newClauseVector n = do + v <- MV.new (max 4 n) + MV.set v NullClause + return v + +-- | returns the nth 'Clause' +{-# INLINE getNthClause #-} +getNthClause :: ClauseVector -> Int -> IO Clause +getNthClause = MV.unsafeRead + +-- | sets the nth 'Clause' +{-# INLINE setNthClause #-} +setNthClause :: ClauseVector -> Int -> Clause -> IO () +setNthClause = MV.unsafeWrite + +-- | swaps the two 'Clause's +{-# INLINE swapClauses #-} +swapClauses :: ClauseVector -> Int -> Int -> IO () +swapClauses = MV.unsafeSwap diff --git a/SAT/Mios/ClauseManager.hs b/SAT/Mios/ClauseManager.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/ClauseManager.hs @@ -0,0 +1,326 @@ +{-# LANGUAGE + BangPatterns + , DuplicateRecordFields + , FlexibleInstances + , MultiParamTypeClasses + , RecordWildCards + , ViewPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +-- | A shrinkable vector of 'C.Clause' +module SAT.Mios.ClauseManager + ( + -- * higher level interface for ClauseVector + ClauseManager (..) +-- -- * vector of clauses +-- , SimpleManager + -- * Manager with an extra Int (used as sort key or blocking literal) + , ClauseExtManager + , pushClauseWithKey + , getKeyVector + , markClause +-- , purifyManager + -- * WatcherList + , WatcherList + , newWatcherList + , getNthWatcher + , garbageCollect +-- , numberOfRegisteredClauses + ) + where + +import Control.Monad (forM, unless, when) +import qualified Data.IORef as IORef +import qualified Data.List as L +import qualified Data.Vector as V +import qualified Data.Vector.Mutable as MV +import SAT.Mios.Types +import qualified SAT.Mios.Clause as C + +-- | resizable clause vector +class ClauseManager a where + newManager :: Int -> IO a + numberOfClauses :: a -> IO Int + clearManager :: a -> IO () + shrinkManager :: a -> Int -> IO () + getClauseVector :: a -> IO C.ClauseVector + pushClause :: a -> C.Clause -> IO () +-- removeClause :: a -> C.Clause -> IO () +-- removeNthClause :: a -> Int -> IO () + +{- +-- | The Clause Container +data SimpleManager = SimpleManager + { + _nActives :: IntSingleton -- number of active clause + , _clauseVector :: IORef.IORef C.ClauseVector -- clause list + } + +instance ClauseManager SimpleManager where + {-# SPECIALIZE INLINE newManager :: Int -> IO SimpleManager #-} + newManager initialSize = do + i <- newInt 0 + v <- C.newClauseVector initialSize + SimpleManager i <$> IORef.newIORef v + {-# SPECIALIZE INLINE numberOfClauses :: SimpleManager -> IO Int #-} + numberOfClauses SimpleManager{..} = getInt _nActives + {-# SPECIALIZE INLINE clearManager :: SimpleManager -> IO () #-} + clearManager SimpleManager{..} = setInt _nActives 0 + {-# SPECIALIZE INLINE shrinkManager :: SimpleManager -> Int -> IO () #-} + shrinkManager SimpleManager{..} k = modifyInt _nActives (subtract k) + {-# SPECIALIZE INLINE getClauseVector :: SimpleManager -> IO C.ClauseVector #-} + getClauseVector SimpleManager{..} = IORef.readIORef _clauseVector + -- | O(1) inserter + {-# SPECIALIZE INLINE pushClause :: SimpleManager -> C.Clause -> IO () #-} + pushClause !SimpleManager{..} !c = do + !n <- getInt _nActives + !v <- IORef.readIORef _clauseVector + if MV.length v - 1 <= n + then do + v' <- MV.unsafeGrow v (max 8 (MV.length v)) + -- forM_ [n .. MV.length v' - 1] $ \i -> MV.unsafeWrite v' i C.NullClause + MV.unsafeWrite v' n c + IORef.writeIORef _clauseVector v' + else MV.unsafeWrite v n c + modifyInt _nActives (1 +) + -- | O(1) remove-and-compact function + {-# SPECIALIZE INLINE removeNthClause :: SimpleManager -> Int -> IO () #-} + removeNthClause SimpleManager{..} i = do + !n <- subtract 1 <$> getInt _nActives + !v <- IORef.readIORef _clauseVector + MV.unsafeWrite v i =<< MV.unsafeRead v n + setInt _nActives n + -- | O(n) but lightweight remove-and-compact function + -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it. + {-# SPECIALIZE INLINE removeClause :: SimpleManager -> C.Clause -> IO () #-} + removeClause SimpleManager{..} c = do + -- putStrLn =<< dump "@removeClause| remove " c + -- putStrLn =<< dump "@removeClause| from " m + !n <- subtract 1 <$> getInt _nActives + -- unless (0 <= n) $ error $ "removeClause catches " ++ show n + !v <- IORef.readIORef _clauseVector + let + seekIndex :: Int -> IO Int + seekIndex k = do + c' <- MV.unsafeRead v k + if c' == c then return k else seekIndex $ k + 1 + unless (n == -1) $ do + !i <- seekIndex 0 + MV.unsafeWrite v i =<< MV.unsafeRead v n + setInt _nActives n + +instance VectorFamily SimpleManager C.Clause where + dump mes SimpleManager{..} = do + n <- getInt _nActives + if n == 0 + then return $ mes ++ "empty clausemanager" + else do + l <- take n <$> (asList =<< IORef.readIORef _clauseVector) + sts <- mapM (dump ",") (l :: [C.Clause]) + return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts) +-} + +-------------------------------------------------------------------------------- + +-- | Clause + Blocking Literal +data ClauseExtManager = ClauseExtManager + { + _nActives :: !IntSingleton -- number of active clause + , _purged :: !BoolSingleton -- whether it needs gc + , _clauseVector :: IORef.IORef C.ClauseVector -- clause list + , _keyVector :: IORef.IORef Vec -- Int list + } + +instance ClauseManager ClauseExtManager where + {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-} + newManager initialSize = do + i <- newInt 0 + v <- C.newClauseVector initialSize + b <- newVec (MV.length v) + ClauseExtManager i <$> newBool False <*> IORef.newIORef v <*> IORef.newIORef b + {-# SPECIALIZE INLINE numberOfClauses :: ClauseExtManager -> IO Int #-} + numberOfClauses !m = getInt (_nActives m) + {-# SPECIALIZE INLINE clearManager :: ClauseExtManager -> IO () #-} + clearManager !m = setInt (_nActives m) 0 + {-# SPECIALIZE INLINE shrinkManager :: ClauseExtManager -> Int -> IO () #-} + shrinkManager !m k = modifyInt (_nActives m) (subtract k) + {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-} + getClauseVector !m = IORef.readIORef (_clauseVector m) + -- | O(1) insertion function + {-# SPECIALIZE INLINE pushClause :: ClauseExtManager -> C.Clause -> IO () #-} + pushClause !ClauseExtManager{..} !c = do + -- checkConsistency m c + !n <- getInt _nActives + !v <- IORef.readIORef _clauseVector + !b <- IORef.readIORef _keyVector + if MV.length v - 1 <= n + then do + let len = max 8 $ MV.length v + v' <- MV.unsafeGrow v len + b' <- vecGrow b len + MV.unsafeWrite v' n c + setNth b' n 0 + IORef.writeIORef _clauseVector v' + IORef.writeIORef _keyVector b' + else MV.unsafeWrite v n c >> setNth b n 0 + modifyInt _nActives (1 +) +{- + -- | O(n) but lightweight remove-and-compact function + -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it. + {-# SPECIALIZE INLINE removeClause :: ClauseExtManager -> C.Clause -> IO () #-} + removeClause ClauseExtManager{..} c = do + !n <- subtract 1 <$> getInt _nActives + !v <- IORef.readIORef _clauseVector + !b <- IORef.readIORef _keyVector + let + seekIndex :: Int -> IO Int + seekIndex k = do + c' <- MV.unsafeRead v k + if c' == c then return k else seekIndex $ k + 1 + unless (n == -1) $ do + !i <- seekIndex 0 + MV.unsafeWrite v i =<< MV.unsafeRead v n + setNth b i =<< getNth b n + setInt _nActives n + removeNthClause = error "removeNthClause is not implemented on ClauseExtManager" +-} + +-- | sets the expire flag to a clause +{-# INLINE markClause #-} +markClause :: ClauseExtManager -> C.Clause -> IO () +markClause ClauseExtManager{..} c = do + !n <- getInt _nActives + !v <- IORef.readIORef _clauseVector + let + seekIndex :: Int -> IO () + seekIndex k = do + c' <- MV.unsafeRead v k + if c' == c then MV.unsafeWrite v k C.NullClause else seekIndex $ k + 1 + unless (n == 0) $ do + seekIndex 0 + setBool _purged True + +{-# INLINE purifyManager #-} +purifyManager :: ClauseExtManager -> IO () +purifyManager ClauseExtManager{..} = do + diry <- getBool _purged + when diry $ do + n <- getInt _nActives + vec <- IORef.readIORef _clauseVector + keys <- IORef.readIORef _keyVector + let + loop :: Int -> Int -> IO Int + loop ((< n) -> False) n' = return n' + loop i j = do + c <- C.getNthClause vec i + if c /= C.NullClause + then do + unless (i == j) $ do + C.setNthClause vec j c + setNth keys j =<< getNth keys i + loop (i + 1) (j + 1) + else loop (i + 1) j + setInt _nActives =<< loop 0 0 + setBool _purged False + +-- | returns the associated Int vector +{-# INLINE getKeyVector #-} +getKeyVector :: ClauseExtManager -> IO Vec +getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector + +-- | O(1) inserter +{-# INLINE pushClauseWithKey #-} +pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO () +pushClauseWithKey !ClauseExtManager{..} !c k = do + -- checkConsistency m c + !n <- getInt _nActives + !v <- IORef.readIORef _clauseVector + !b <- IORef.readIORef _keyVector + if MV.length v - 1 <= n + then do + let len = max 8 $ MV.length v + v' <- MV.unsafeGrow v len + b' <- vecGrow b len + MV.unsafeWrite v' n c + setNth b' n k + IORef.writeIORef _clauseVector v' + IORef.writeIORef _keyVector b' + else MV.unsafeWrite v n c >> setNth b n k + modifyInt _nActives (1 +) + +instance VectorFamily ClauseExtManager C.Clause where + dump mes ClauseExtManager{..} = do + n <- getInt _nActives + if n == 0 + then return $ mes ++ "empty ClauseExtManager" + else do + l <- take n <$> (asList =<< IORef.readIORef _clauseVector) + sts <- mapM (dump ",") (l :: [C.Clause]) + return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts) + +-------------------------------------------------------------------------------- WatcherList + +-- | Vector of 'ClauseExtManager' +type WatcherList = V.Vector ClauseExtManager + +-- | /n/ is the number of 'Var', /m/ is default size of each watcher list +-- | For /n/ vars, we need [0 .. 2 + 2 * n - 1] slots, namely /2 * (n + 1)/-length vector +newWatcherList :: Int -> Int -> IO WatcherList +newWatcherList n m = V.fromList <$> forM [0 .. int2lit (negate n) + 1] (\_ -> newManager m) + +-- | returns the watcher List :: "ClauseManager" for "Literal" /l/ +{-# INLINE getNthWatcher #-} +getNthWatcher :: WatcherList -> Lit -> ClauseExtManager +getNthWatcher = V.unsafeIndex + +instance VectorFamily WatcherList C.Clause where + dump mes wl = (mes ++) . L.concat <$> forM [1 .. V.length wl - 1] (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i)) + +-- | purges all expirable clauses in 'WatcherList' +{-# INLINE garbageCollect #-} +garbageCollect :: WatcherList -> IO () +garbageCollect = V.mapM_ purifyManager + +{- +numberOfRegisteredClauses :: WatcherList -> IO Int +numberOfRegisteredClauses ws = sum <$> V.mapM numberOfClauses ws +-} + +{- +-------------------------------------------------------------------------------- debugging stuff + +checkConsistency :: ClauseManager a => a -> C.Clause -> IO () +checkConsistency manager c = do + nc <- numberOfClauses manager + vec <- getClauseVector manager + let + loop :: Int -> IO () + loop i = do + when (i < nc) $ do + c' <- MV.unsafeRead vec i + when (c' == c) $ error "insert a clause to a ClauseMananger twice" + loop $ i + 1 + loop 0 + +checkClauseOrder :: ClauseManager a => a -> IO () +checkClauseOrder manager = do + putStr "checking..." + nc <- numberOfClauses manager + vec <- getClauseVector manager + let + nthActivity :: Int -> IO Double + nthActivity i = getDouble . C.activity =<< MV.unsafeRead vec i + report :: Int -> Int -> IO () + report i j = (putStr . (++ ", ") . show =<< nthActivity i) >> when (i < j) (report (i + 1) j) + loop :: Int -> Double -> IO () + loop i v = do + when (i < nc) $ do + c <- MV.unsafeRead vec i + a <- getDouble (C.activity c) + when (c == C.NullClause) $ error "null is included" + when (v < a) $ report 0 i >> error ("unsorted clause vector: " ++ show (nc, i)) + loop (i + 1) a + loop 0 =<< nthActivity 0 + putStrLn "done" +-} diff --git a/SAT/Mios/Data/Singleton.hs b/SAT/Mios/Data/Singleton.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Data/Singleton.hs @@ -0,0 +1,105 @@ +{-# LANGUAGE + BangPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +-- | A fast(est) mutable data based on Data.Vector.Unboxed.Mutable + +module SAT.Mios.Data.Singleton + ( + -- * Bool + BoolSingleton + , newBool + , getBool + , setBool + , modifyBool + -- * Int + , IntSingleton + , newInt + , getInt + , setInt + , modifyInt + -- * Double + , DoubleSingleton + , newDouble + , getDouble + , setDouble + , modifyDouble + ) + where +import qualified Data.Vector.Unboxed.Mutable as UV + +-- | mutable Int +type IntSingleton = UV.IOVector Int + +-- | returns a new 'IntSingleton' +newInt :: Int -> IO IntSingleton +newInt k = do + s <- UV.new 1 + UV.unsafeWrite s 0 k + return s + +-- | returns the value +{-# INLINE getInt #-} +getInt :: IntSingleton -> IO Int +getInt val = UV.unsafeRead val 0 + +-- | sets the value +{-# INLINE setInt #-} +setInt :: IntSingleton -> Int -> IO () +setInt val !x = UV.unsafeWrite val 0 x + +-- | modifies the value +{-# INLINE modifyInt #-} +modifyInt :: IntSingleton -> (Int -> Int) -> IO () +modifyInt val f = UV.unsafeModify val f 0 + +-- | mutable Bool +type BoolSingleton = UV.IOVector Bool + +-- | returns a new 'BoolSingleton' +newBool :: Bool -> IO BoolSingleton +newBool b = do + s <- UV.new 1 + UV.unsafeWrite s 0 b + return s + +-- | returns the value +{-# INLINE getBool #-} +getBool :: BoolSingleton -> IO Bool +getBool val = UV.unsafeRead val 0 + +-- | sets the value +{-# INLINE setBool #-} +setBool :: BoolSingleton -> Bool -> IO () +setBool val !x = UV.unsafeWrite val 0 x + +-- | modifies the value +{-# INLINE modifyBool #-} +modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO () +modifyBool val f = UV.unsafeModify val f 0 + +-- | mutable Double +type DoubleSingleton = UV.IOVector Double + +-- | returns a new 'DoubleSingleton' +newDouble :: Double -> IO DoubleSingleton +newDouble d = do + s <- UV.new 1 + UV.unsafeWrite s 0 d + return s + +-- | returns the value +{-# INLINE getDouble #-} +getDouble :: DoubleSingleton -> IO Double +getDouble val = UV.unsafeRead val 0 + +-- | sets the value +{-# INLINE setDouble #-} +setDouble :: DoubleSingleton -> Double -> IO () +setDouble val !x = UV.unsafeWrite val 0 x + +-- | modifies the value +{-# INLINE modifyDouble #-} +modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO () +modifyDouble val f = UV.unsafeModify val f 0 diff --git a/SAT/Mios/Data/Stack.hs b/SAT/Mios/Data/Stack.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Data/Stack.hs @@ -0,0 +1,90 @@ +{-# LANGUAGE + MultiParamTypeClasses + #-} +{-# LANGUAGE Trustworthy #-} + +-- | stack of Int, by adding the length field as the zero-th element to a 'Vec' +module SAT.Mios.Data.Stack + ( + Stack + , newStack + , clearStack + , sizeOfStack + , pushToStack + , popFromStack + , lastOfStack + , shrinkStack + , asSizedVec +-- , isoVec + ) + where + +import qualified Data.Vector.Unboxed.Mutable as UV +import SAT.Mios.Types + +-- | Unboxed mutable stack for Int. +newtype Stack = Stack (UV.IOVector Int) + +instance VectorFamily Stack Int where + dump str v = (str ++) . show <$> asList v + {-# SPECIALIZE INLINE asVec :: Stack -> Vec #-} + asVec (Stack v) = UV.unsafeTail v + asList (Stack v) = do + (n : l) <- asList v + return $ take n l + +-- | returns the number of elements +{-# INLINE sizeOfStack #-} +sizeOfStack :: Stack -> IO Int +sizeOfStack (Stack v) = UV.unsafeRead v 0 + +-- | clear stack +{-# INLINE clearStack #-} +clearStack :: Stack -> IO () +clearStack (Stack v) = UV.unsafeWrite v 0 0 + +-- | returns a new stack which size is @size@ +{-# INLINABLE newStack #-} +newStack :: Int -> IO Stack +newStack n = do + v <- UV.new $ n + 1 + UV.set v 0 + return $ Stack v + +-- | pushs an int to 'Stack' +{-# INLINE pushToStack #-} +pushToStack :: Stack -> Int -> IO () +pushToStack (Stack v) x = do + i <- (+ 1) <$> UV.unsafeRead v 0 + UV.unsafeWrite v i x + UV.unsafeWrite v 0 i + +-- | drops the first element from 'Stack' +{-# INLINE popFromStack #-} +popFromStack :: Stack -> IO () +popFromStack (Stack v) = UV.unsafeModify v (subtract 1) 0 + +-- | peeks the last element in 'Stack' +{-# INLINE lastOfStack #-} +lastOfStack :: Stack -> IO Int +lastOfStack (Stack v) = UV.unsafeRead v =<< UV.unsafeRead v 0 + +-- | Shrink the stack. The given arg means the number of discards. +-- therefore, shrink s n == for [1 .. n] $ \_ -> pop s +{-# INLINE shrinkStack #-} +shrinkStack :: Stack -> Int -> IO () +shrinkStack (Stack v) k = UV.unsafeModify v (subtract k) 0 + +-- | converts Stack to sized Vec; this is the method to get the internal vector +{-# INLINE asSizedVec #-} +asSizedVec :: Stack -> Vec +asSizedVec (Stack v) = v + +{- +-- | isomorphic conversion to 'Vec' +-- +-- Note: 'asVec' drops the 1st element and no copy (unsafe operation); 'isoVec' really copies the real elements +{-# INLINE isoVec #-} +isoVec :: Stack -> IO Vec +isoVec (Stack v) = UV.clone . flip UV.take v . (1 +) =<< UV.unsafeRead v 0 +-} diff --git a/SAT/Mios/Data/Vec.hs b/SAT/Mios/Data/Vec.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Data/Vec.hs @@ -0,0 +1,86 @@ +-- | The fundamental data structure: Fixed Mutable Unboxed Int Vector +{-# LANGUAGE + BangPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Mios.Data.Vec + ( + Vec + , sizeOfVector + , getNth + , setNth + , swapBetween + , modifyNth + , setAll + , newVec + , newVecWith + , newSizedVecIntFromList + , newSizedVecIntFromUVector + , vecGrow + ) + where + +import qualified Data.Vector.Unboxed as U +import qualified Data.Vector.Unboxed.Mutable as UV + +-- | Costs of all operations are /O/(/1/) +type Vec = UV.IOVector Int + +-- | returns the size of 'Vec' +{-# INLINE sizeOfVector #-} +sizeOfVector :: Vec -> IO Int +sizeOfVector v = return $! UV.length v + +-- | returns a new 'Vec' +{-# INLINE newVec #-} +newVec :: Int -> IO Vec +newVec = UV.new + +-- | returns a new 'Vec' filled with an Int +{-# INLINE newVecWith #-} +newVecWith :: Int -> Int -> IO Vec +newVecWith n x = do + v <- UV.new n + UV.set v x + return v + +-- | gets the nth value +{-# INLINE getNth #-} +getNth :: Vec -> Int -> IO Int +getNth = UV.unsafeRead + +-- | sets the nth value +{-# INLINE setNth #-} +setNth :: Vec -> Int -> Int -> IO () +setNth = UV.unsafeWrite + +-- | modify the nth value +{-# INLINE modifyNth #-} +modifyNth :: Vec -> (Int -> Int) -> Int -> IO () +modifyNth = UV.unsafeModify + +-- | sets all elements +{-# INLINE setAll #-} +setAll :: Vec -> Int -> IO () +setAll = UV.set + +-- | swaps two elements +{-# INLINE swapBetween #-} +swapBetween:: Vec -> Int -> Int -> IO () +swapBetween = UV.unsafeSwap + +-- | returns a new 'Vec' from a @[Int]@ +{-# INLINE newSizedVecIntFromList #-} +newSizedVecIntFromList :: [Int] -> IO Vec +newSizedVecIntFromList !l = U.unsafeThaw $ U.fromList (length l : l) + +-- | returns a new 'Vec' from a Unboxed Int Vector +{-# INLINE newSizedVecIntFromUVector #-} +newSizedVecIntFromUVector :: U.Vector Int -> IO Vec +newSizedVecIntFromUVector = U.unsafeThaw + +-- | calls @unasfeGrow@ +{-# INLINE vecGrow #-} +vecGrow :: Vec -> Int -> IO Vec +vecGrow = UV.unsafeGrow diff --git a/SAT/Mios/Data/VecBool.hs b/SAT/Mios/Data/VecBool.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Data/VecBool.hs @@ -0,0 +1,55 @@ +-- | Mutable Unboxed Boolean Vector +-- +-- * __VecBool@::UV.IOVector Bool@ -- data type that contains a mutable list of elements +-- +{-# LANGUAGE + BangPatterns + , FlexibleInstances + , MultiParamTypeClasses + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Mios.Data.VecBool + ( + VecBool + , newVecBool + , getNthBool + , setNthBool + , modifyNthBool + ) + where + +import Control.Monad (forM) +import qualified Data.Vector.Unboxed.Mutable as UV +import SAT.Mios.Types (VectorFamily(..)) + +-- | Mutable unboxed Bool Vector +type VecBool = UV.IOVector Bool + +-- | provides 'clear' and 'size' +instance VectorFamily VecBool Bool where + clear _ = error "VecBool.clear" + asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v + dump str v = (str ++) . show <$> asList v + +-- | returns a new 'VecBool' +newVecBool :: Int -> Bool -> IO VecBool +newVecBool n x = do + v <- UV.new n + UV.set v x + return v + +-- | returns the nth value in 'VecBool' +{-# INLINE getNthBool #-} +getNthBool :: VecBool -> Int -> IO Bool +getNthBool = UV.unsafeRead + +-- | sets the nth value +{-# INLINE setNthBool #-} +setNthBool :: VecBool -> Int -> Bool -> IO () +setNthBool = UV.unsafeWrite + +-- | sets the nth value +{-# INLINE modifyNthBool #-} +modifyNthBool :: VecBool -> (Bool -> Bool) -> Int -> IO () +modifyNthBool = UV.unsafeModify diff --git a/SAT/Mios/Data/VecDouble.hs b/SAT/Mios/Data/VecDouble.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Data/VecDouble.hs @@ -0,0 +1,53 @@ +-- | Mutable Unboxed Double Vector +{-# LANGUAGE + BangPatterns + , FlexibleInstances + , MultiParamTypeClasses + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Mios.Data.VecDouble + ( + VecDouble + , newVecDouble + , getNthDouble + , setNthDouble + , modifyNthDouble + ) + where + +import Control.Monad (forM) +import Data.List () +import qualified Data.Vector.Unboxed.Mutable as UV +import SAT.Mios.Types (VectorFamily(..)) + +-- | Mutable unboxed Double Vector +type VecDouble = UV.IOVector Double + +instance VectorFamily VecDouble Double where + clear _ = error "VecDouble.clear" + asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v + dump str v = (str ++) . show <$> asList v + +-- | returns a new 'VecDouble' +newVecDouble :: Int -> Double -> IO VecDouble +newVecDouble n 0 = UV.new n +newVecDouble n x = do + v <- UV.new n + UV.set v x + return v + +-- | returns the nth value in 'VecDouble' +{-# INLINE getNthDouble #-} +getNthDouble :: Int -> VecDouble -> IO Double +getNthDouble !n v = UV.unsafeRead v n + +-- | sets the nth value +{-# INLINE setNthDouble #-} +setNthDouble :: Int -> VecDouble -> Double -> IO () +setNthDouble !n v !x = UV.unsafeWrite v n x + +-- | updates the nth value +{-# INLINE modifyNthDouble #-} +modifyNthDouble :: Int -> VecDouble -> (Double -> Double) -> IO () +modifyNthDouble !n v !f = UV.unsafeModify v f n diff --git a/SAT/Mios/Internal.hs b/SAT/Mios/Internal.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Internal.hs @@ -0,0 +1,33 @@ +-- | Mios Internal Settings +module SAT.Mios.Internal + ( + versionId + , MiosConfiguration (..) + , defaultConfiguration + , module Plumbing + ) + where +import SAT.Mios.Data.VecBool as Plumbing +import SAT.Mios.Data.VecDouble as Plumbing +import SAT.Mios.Data.Stack as Plumbing + +-- | version name +versionId :: String +versionId = "mios 1.3.0 -- https://github.com/shnarazk/mios" -- no more LBD + +-- | solver's parameters; random decision rate was dropped. +data MiosConfiguration = MiosConfiguration + { + variableDecayRate :: !Double -- ^ decay rate for variable activity +-- , clauseDecayRate :: !Double -- ^ decay rate for clause activity + } + +-- | dafault configuration +-- +-- * Minisat-1.14 uses @(0.95, 0.999, 0.2 = 20 / 1000)@. +-- * Minisat-2.20 uses @(0.95, 0.999, 0)@. +-- * Gulcose-4.0 uses @(0.8 , 0.999, 0)@. +-- * Mios-1.2 uses @(0.95, 0.999, 0)@. +-- +defaultConfiguration :: MiosConfiguration +defaultConfiguration = MiosConfiguration 0.95 {- 0.999 -} {- 0 -} diff --git a/SAT/Mios/Main.hs b/SAT/Mios/Main.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Main.hs @@ -0,0 +1,810 @@ +{-# LANGUAGE + BangPatterns + , RecordWildCards + , ScopedTypeVariables + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +-- | This is a part of MIOS; main heuristics +module SAT.Mios.Main + ( + simplifyDB + , solve + ) + where + +import Control.Monad (forM_, unless, void, when) +import Data.Bits +import Data.Foldable (foldrM) +import SAT.Mios.Types +import SAT.Mios.Internal +import SAT.Mios.Clause +import SAT.Mios.ClauseManager +import SAT.Mios.Solver +-- import SAT.Mios.Ranking + +-------------------------------------------------------------------------------- Ranking +-- | a special version of ranking +{-# INLINE ranking' #-} +ranking' :: Clause -> IO Int +ranking' = sizeOfClause + +-- | #114: __RemoveWatch__ +{-# INLINABLE removeWatch #-} +removeWatch :: Solver -> Clause -> IO () +removeWatch (watches -> w) c = do + let lvec = asVec c + l1 <- negateLit <$> getNth lvec 0 + markClause (getNthWatcher w l1) c + l2 <- negateLit <$> getNth lvec 1 + markClause (getNthWatcher w l2) c + +-------------------------------------------------------------------------------- +-- Operations on 'Clause' +-------------------------------------------------------------------------------- + +-- | __Fig. 8. (p.12)__ create a new LEARNT clause and adds it to watcher lists +-- This is a strippped-down version of 'newClause' in Solver +{-# INLINABLE newLearntClause #-} +newLearntClause :: Solver -> Vec -> IO () +newLearntClause s@Solver{..} ps = do + good <- getBool ok + when good $ do + -- ps is a 'SizedVectorInt'; ps[0] is the number of active literals + -- Since this solver must generate only healthy learnt clauses, we need not to run misc check in 'newClause' + k <- getNth ps 0 + case k of + 1 -> do + l <- getNth ps 1 + unsafeEnqueue s l NullClause + _ -> do + -- allocate clause: + c <- newClauseFromVec True ps + let vec = asVec c + -- Pick a second literal to watch: + let + findMax :: Int -> Int -> Int -> IO Int + findMax ((< k) -> False) j _ = return j + findMax i j val = do + v' <- lit2var <$> getNth vec i + a <- getNth assigns v' + b <- getNth level v' + if (a /= lBottom) && (val < b) + then findMax (i + 1) i b + else findMax (i + 1) j val + swapBetween vec 1 =<< findMax 0 0 0 -- Let @max_i@ be the index of the literal with highest decision level + -- Bump, enqueue, store clause: + setDouble (activity c) . fromIntegral =<< decisionLevel s -- newly learnt clauses should be considered active + -- Add clause to all managers + pushClause learnts c + l <- getNth vec 0 + pushClauseWithKey (getNthWatcher watches (negateLit l)) c 0 + l1 <- negateLit <$> getNth vec 1 + pushClauseWithKey (getNthWatcher watches l1) c 0 + -- update the solver state by @l@ + unsafeEnqueue s l c + -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue + -- setRank s c + setBool (protected c) True + +-- | __Simplify.__ At the top-level, a constraint may be given the opportunity to +-- simplify its representation (returns @False@) or state that the constraint is +-- satisfied under the current assignment and can be removed (returns @True@). +-- A constraint must /not/ be simplifiable to produce unit information or to be +-- conflicting; in that case the propagation has not been correctly defined. +-- +-- MIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy. +{-# INLINABLE simplify #-} +simplify :: Solver -> Clause -> IO Bool +simplify s c = do + n <- sizeOfClause c + let + lvec = asVec c + loop ::Int -> IO Bool + loop ((< n) -> False) = return False + loop i = do + v <- valueLit s =<< getNth lvec i + if v == 1 then return True else loop (i + 1) + loop 0 + +-------------------------------------------------------------------------------- +-- MIOS NOTE on Minor methods: +-- +-- * no (meaningful) 'newVar' in mios +-- * 'assume' is defined in 'Solver' +-- * `cancelUntil` is defined in 'Solver' + +-------------------------------------------------------------------------------- +-- Major methods + +-- | M114: __Fig. 10. (p.15)__ +-- +-- analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel :: int&) -> [void] +-- +-- __Description:_- +-- Analzye confilct and produce a reason clause. +-- +-- __Pre-conditions:__ +-- * 'out_learnt' is assumed to be cleared. +-- * Corrent decision level must be greater than root level. +-- +-- __Post-conditions:__ +-- * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. +-- * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the +-- rest of literals. There may be others from the same level though. +-- +-- @analyze@ is invoked from @search@ +-- {-# INLINEABLE analyze #-} +analyze :: Solver -> Clause -> IO Int +analyze s@Solver{..} confl = do + -- litvec + clearStack litsLearnt + pushToStack litsLearnt 0 -- reserve the first place for the unassigned literal + dl <- decisionLevel s + let + litsVec = asVec litsLearnt + trailVec = asVec trail + loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int + loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level + when (learnt c) $ do + claBumpActivity s c +{- + -- update LBD like #Glucose4.0 + d <- getInt (lbd c) + when (2 < d) $ do + nblevels <- lbdOf s c + when (nblevels + 1 < d) $ do -- improve the LBD + when (d <= 30) $ setBool (protected c) True -- 30 is `lbLBDFrozenClause` + -- seems to be interesting: keep it fro the next round + setInt (lbd c) nblevels -- Update it +-} + sc <- sizeOfClause c + let + lvec = asVec c + loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int) + loopOnLiterals ((< sc) -> False) b pc = return (b, pc) -- b = btLevel, pc = pathC + loopOnLiterals j b pc = do + (q :: Lit) <- getNth lvec j + let v = lit2var q + sn <- getNth an'seen v + l <- getNth level v + if sn == 0 && 0 < l + then do + varBumpActivity s v + setNth an'seen v 1 + if dl <= l -- cancelUntil doesn't clear level of cancelled literals + then do + -- glucose heuristics + r <- getNthClause reason v + when (r /= NullClause && learnt r) $ pushToStack lastDL q + -- end of glucose heuristics + loopOnLiterals (j + 1) b (pc + 1) + else pushToStack litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc + else loopOnLiterals (j + 1) b pc + (b', pathC') <- loopOnLiterals (if p == bottomLit then 0 else 1) bl pathC + let + -- select next clause to look at + nextPickedUpLit :: Int -> IO Int + nextPickedUpLit i = do + x <- getNth an'seen . lit2var =<< getNth trailVec i + if x == 0 then nextPickedUpLit $ i - 1 else return i + ti' <- nextPickedUpLit ti + nextP <- getNth trailVec ti' + let nextV = lit2var nextP + confl' <- getNthClause reason nextV + setNth an'seen nextV 0 + if 1 < pathC' + then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1) + else setNth litsVec 0 (negateLit nextP) >> return b' + ti <- subtract 1 <$> sizeOfStack trail + levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0 + -- Simplify phase (implemented only @expensive_ccmin@ path) + n <- sizeOfStack litsLearnt + clearStack an'stack -- analyze_stack.clear(); + clearStack an'toClear -- out_learnt.copyTo(analyze_toclear); + pushToStack an'toClear =<< getNth litsVec 0 + let + merger :: Int -> Int -> IO Int + merger ((< n) -> False) b = return b + merger i b = do + l <- getNth litsVec i + pushToStack an'toClear l + -- restrict the search depth (range) to 32 + merger (i + 1) . setBit b . (31 .&.) =<< getNth level (lit2var l) + levels <- merger 1 0 + let + loopOnLits :: Int -> Int -> IO () + loopOnLits ((< n) -> False) n' = shrinkStack litsLearnt $ n - n' + loopOnLits i j = do + l <- getNth litsVec i + c1 <- (NullClause ==) <$> getNthClause reason (lit2var l) + if c1 + then setNth litsVec j l >> loopOnLits (i + 1) (j + 1) + else do + c2 <- not <$> analyzeRemovable s l levels + if c2 + then setNth litsVec j l >> loopOnLits (i + 1) (j + 1) + else loopOnLits (i + 1) j + loopOnLits 1 1 -- the first literal is specail + -- glucose heuristics + nld <- sizeOfStack lastDL + r <- sizeOfStack litsLearnt -- this is not the right value + let + vec = asVec lastDL + loopOnLastDL :: Int -> IO () + loopOnLastDL ((< nld) -> False) = return () + loopOnLastDL i = do + v <- lit2var <$> getNth vec i + r' <- ranking' =<< getNthClause reason v + when (r < r') $ varBumpActivity s v + loopOnLastDL $ i + 1 + loopOnLastDL 0 + clearStack lastDL + -- Clear seen + k <- sizeOfStack an'toClear + let + vec' = asVec an'toClear + cleaner :: Int -> IO () + cleaner ((< k) -> False) = return () + cleaner i = do + v <- lit2var <$> getNth vec' i + setNth an'seen v 0 + cleaner $ i + 1 + cleaner 0 + return levelToReturn + +-- | #M114 +-- Check if 'p' can be removed, 'abstract_levels' is used to abort early if the algorithm is +-- visiting literals at levels that cannot be removed later. +-- +-- Implementation memo: +-- +-- * @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt'). +-- This is used only in this function and @analyze@. +-- +{-# INLINEABLE analyzeRemovable #-} +analyzeRemovable :: Solver -> Lit -> Int -> IO Bool +analyzeRemovable Solver{..} p minLevel = do + -- assert (reason[var(p)]!= NullCaulse); + clearStack an'stack -- analyze_stack.clear() + pushToStack an'stack p -- analyze_stack.push(p); + top <- sizeOfStack an'toClear + let + loopOnStack :: IO Bool + loopOnStack = do + k <- sizeOfStack an'stack -- int top = analyze_toclear.size(); + if 0 == k + then return True + else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL); + sl <- lastOfStack an'stack + popFromStack an'stack -- analyze_stack.pop(); + c <- getNthClause reason (lit2var sl) -- getRoot sl + nl <- sizeOfClause c + let + cvec = asVec c + loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){ + loopOnLit ((< nl) -> False) = loopOnStack + loopOnLit i = do + p' <- getNth cvec i -- valid range is [0 .. nl - 1] + let v' = lit2var p' + l' <- getNth level v' + c1 <- (1 /=) <$> getNth an'seen v' + if c1 && (0 /= l') -- if (!analyze_seen[var(p)] && level[var(p)] != 0){ + then do + c3 <- (NullClause /=) <$> getNthClause reason v' + if c3 && testBit minLevel (l' .&. 31) -- if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){ + then do + setNth an'seen v' 1 -- analyze_seen[var(p)] = 1; + pushToStack an'stack p' -- analyze_stack.push(p); + pushToStack an'toClear p' -- analyze_toclear.push(p); + loopOnLit $ i + 1 + else do + -- loopOnLit (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0; + top' <- sizeOfStack an'toClear + let vec = asVec an'toClear + forM_ [top .. top' - 1] $ \j -> do x <- getNth vec j; setNth an'seen (lit2var x) 0 + -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop + shrinkStack an'toClear $ top' - top + return False + else loopOnLit $ i + 1 + loopOnLit 1 + loopOnStack + +-- | #114 +-- analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void] +-- +-- __Description:__ +-- Specialized analysis proceduce to express the final conflict in terms of assumptions. +-- 'root_level' is allowed to point beyond end of trace (useful if called after conflict while +-- making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed +-- if conflict arose before search even started). +-- +analyzeFinal :: Solver -> Clause -> Bool -> IO () +analyzeFinal Solver{..} confl skipFirst = do + clearStack conflict + rl <- getInt rootLevel + unless (rl == 0) $ do + n <- sizeOfClause confl + let + lvec = asVec confl + loopOnConfl :: Int -> IO () + loopOnConfl ((< n) -> False) = return () + loopOnConfl i = do + (x :: Var) <- lit2var <$> getNth lvec i + lvl <- getNth level x + when (0 < lvl) $ setNth an'seen x 1 + loopOnConfl $ i + 1 + loopOnConfl $ if skipFirst then 1 else 0 + tls <- sizeOfStack trailLim + trs <- sizeOfStack trail + tlz <- getNth (asVec trailLim) 0 + let + trailVec = asVec trail + loopOnTrail :: Int -> IO () + loopOnTrail ((tlz <=) -> False) = return () + loopOnTrail i = do + (l :: Lit) <- getNth trailVec i + let (x :: Var) = lit2var l + saw <- getNth an'seen x + when (saw == 1) $ do + (r :: Clause) <- getNthClause reason x + if r == NullClause + then pushToStack conflict (negateLit l) + else do + k <- sizeOfClause r + let + cvec = asVec r + loopOnLits :: Int -> IO () + loopOnLits ((< k) -> False) = return () + loopOnLits j = do + (v :: Var) <- lit2var <$> getNth cvec j + lv <- getNth level v + when (0 < lv) $ setNth an'seen v 1 + loopOnLits $ i + 1 + loopOnLits 1 + setNth an'seen x 0 + loopOnTrail $ i - 1 + loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth (asVec trailLim) rl + +-- | M114: +-- propagate : [void] -> [Clause+] +-- +-- __Description:__ +-- Porpagates all enqueued facts. If a conflict arises, the conflicting clause is returned. +-- otherwise CRef_undef. +-- +-- __Post-conditions:__ +-- * the propagation queue is empty, even if there was a conflict. +-- +-- memo: @propagate@ is invoked by @search@,`simpleDB` and `solve` +{-# INLINABLE propagate #-} +propagate :: Solver -> IO Clause +propagate s@Solver{..} = do + -- myVal <- getNth stats (fromEnum NumOfBackjump) + let +{- + myVal = 0 + bumpAllVar :: IO () -- not in use + bumpAllVar = do + let + loop :: Int -> IO () + loop ((<= nVars) -> False) = return () + loop i = do + c <- getNth pr'seen i + when (c == myVal) $ varBumpActivity s i + loop $ i + 1 + loop 1 +-} + trailVec = asVec trail + while :: Clause -> Bool -> IO Clause + while confl False = {- bumpAllVar >> -} return confl + while confl True = do + (p :: Lit) <- getNth trailVec =<< getInt qHead + modifyInt qHead (+ 1) + let (ws :: ClauseExtManager) = getNthWatcher watches p + end <- numberOfClauses ws + cvec <- getClauseVector ws + bvec <- getKeyVector ws +-- rc <- getNthClause reason $ lit2var p +-- byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> getInt (lbd rc) else return False + let +{- + checkAllLiteralsIn :: Clause -> IO () -- not in use + checkAllLiteralsIn c = do + nc <- sizeOfClause c + let + vec = asVec c + loop :: Int -> IO () + loop((< nc) -> False) = return () + loop i = do + (v :: Var) <- lit2var <$> getNth vec i + setNth pr'seen v myVal + loop $ i + 1 + loop 0 +-} + forClause :: Clause -> Int -> Int -> IO Clause + forClause confl i@((< end) -> False) j = do + shrinkManager ws (i - j) + while confl =<< ((<) <$> getInt qHead <*> sizeOfStack trail) + forClause confl i j = do + (l :: Lit) <- getNth bvec i + bv <- if l == 0 then return lFalse else valueLit s l + if bv == lTrue + then do + unless (i == j) $ do -- NOTE: if i == j, the path doesn't require accesses to cvec! + (c :: Clause) <- getNthClause cvec i + setNthClause cvec j c + setNth bvec j l + forClause confl (i + 1) (j + 1) + else do + -- checkAllLiteralsIn c + (c :: Clause) <- getNthClause cvec i + let + lits = asVec c + falseLit = negateLit p + -- Make sure the false literal is data[1] + ((falseLit ==) <$> getNth lits 0) >>= (`when` swapBetween lits 0 1) + -- if 0th watch is true, then clause is already satisfied. + (first :: Lit) <- getNth lits 0 + val <- valueLit s first + if val == lTrue + then setNthClause cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1) + else do + -- Look for new watch + cs <- sizeOfClause c + let + forLit :: Int -> IO Clause + forLit ((< cs) -> False) = do + -- Did not find watch; clause is unit under assignment: + setNthClause cvec j c + setNth bvec j 0 + result <- enqueue s first c + if not result + then do + ((== 0) <$> decisionLevel s) >>= (`when` setBool ok False) + -- #BBCP + setInt qHead =<< sizeOfStack trail + -- Copy the remaining watches: + let + copy i'@((< end) -> False) j' = forClause c i' j' + copy i' j' = do + setNthClause cvec j' =<< getNthClause cvec i' + setNth bvec j' =<< getNth bvec i' + copy (i' + 1) (j' + 1) + copy (i + 1) (j + 1) + else forClause confl (i + 1) (j + 1) + forLit k = do + (l :: Lit) <- getNth lits k + lv <- valueLit s l + if lv /= lFalse + then do + swapBetween lits 1 k + pushClauseWithKey (getNthWatcher watches (negateLit l)) c l + forClause confl (i + 1) j + else forLit $ k + 1 + forLit 2 + forClause confl 0 0 + while NullClause =<< ((<) <$> getInt qHead <*> sizeOfStack trail) + +-- | #M22 +-- reduceDB: () -> [void] +-- +-- __Description:__ +-- Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked +-- clauses are clauses that are reason to some assignment. Binary clauses are never removed. +{-# INLINABLE reduceDB #-} +reduceDB :: Solver -> IO () +reduceDB s@Solver{..} = do + n <- nLearnts s + vec <- getClauseVector learnts + let + loop :: Int -> IO () + loop ((< n) -> False) = return () + loop i = (removeWatch s =<< getNthClause vec i) >> loop (i + 1) + k <- sortClauses s learnts (div n 2) -- k is the number of clauses not to be purged + loop k -- CAVEAT: `vec` is a zero-based vector + garbageCollect watches + shrinkManager learnts (n - k) + +-- | (Good to Bad) Quick sort the key vector based on their activities and returns number of privileged clauses. +-- this function uses the same metrix as reduceDB_lt in glucose 4.0: +-- 1. binary clause +-- 2. smaller rank +-- 3. larger activity defined in MiniSat +-- , where smaller value is better. +-- +-- they are coded into an Int as the following layout: +-- +-- * 14 bit: LBD or 0 for preserved clauses +-- * 19 bit: converted activity +-- * remain: clauseVector index +-- +(rankWidth :: Int, activityWidth :: Int, indexWidth :: Int) = (l, a, w - (l + a + 1)) + where + w = finiteBitSize (0:: Int) + (l, a) = case () of + _ | 64 <= w -> (8, 25) -- 30 bit => 1G clauses + _ | 60 <= w -> (8, 24) -- 26 bit => 64M clauses + _ | 32 <= w -> (6, 7) -- 18 bit => 256K clauses + _ | 29 <= w -> (6, 5) -- 17 bit => 128K clauses +-- _ -> error "Int on your CPU doesn't have sufficient bit width." + +{-# INLINABLE sortClauses #-} +sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int +sortClauses s cm nneeds = do + -- constants + let + rankMax :: Int + rankMax = 2 ^ rankWidth - 1 + activityMax :: Int + activityMax = 2 ^ activityWidth - 1 + activityScale :: Double + activityScale = fromIntegral activityMax + indexMax :: Int + indexMax = (2 ^ indexWidth - 1) -- 67,108,863 for 26 + n <- numberOfClauses cm + -- when (indexMax < n) $ error $ "## The number of learnt clauses " ++ show n ++ " exceeds mios's " ++ show indexWidth ++" bit manage capacity" + vec <- getClauseVector cm + keys <- getKeyVector cm + -- 1: assign keys + let + assignKey :: Int -> Int -> IO Int + assignKey ((< n) -> False) m = return m + assignKey i m = do + c <- getNthClause vec i + k <- (\k -> if k == 2 then return k else fromEnum <$> getBool (protected c)) =<< sizeOfClause c + case k of + 1 -> setBool (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1) + 2 -> setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1) + _ -> do + l <- locked s c -- this is expensive + if l + then setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1) + else do + d <- ranking' c + b <- floor . (activityScale *) . (1 -) . logBase claActivityThreshold . max 1 <$> getDouble (activity c) + setNth keys i $ shiftL (min rankMax d) (activityWidth + indexWidth) + shiftL b indexWidth + i + assignKey (i + 1) m + limit <- min n . (+ nneeds) <$> assignKey 0 0 + -- 2: sort keyVector + let + sortOnRange :: Int -> Int -> IO () + sortOnRange left right + | limit < left = return () + | left >= right = return () + | left + 1 == right = do + a <- getNth keys left + b <- getNth keys right + unless (a < b) $ swapBetween keys left right + | otherwise = do + let p = div (left + right) 2 + pivot <- getNth keys p + swapBetween keys p left -- set a sentinel for r' + let + nextL :: Int -> IO Int + nextL i@((<= right) -> False) = return i + nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 1) else return i + nextR :: Int -> IO Int + nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 1) else return i + divide :: Int -> Int -> IO Int + divide l r = do + l' <- nextL l + r' <- nextR r + if l' < r' then swapBetween keys l' r' >> divide (l' + 1) (r' - 1) else return r' + m <- divide (left + 1) right + swapBetween keys left m + sortOnRange left (m - 1) + sortOnRange (m + 1) right + sortOnRange 0 (n - 1) + -- 3: place clauses + let + seek :: Int -> IO () + seek ((< limit) -> False) = return () + seek i = do + bits <- getNth keys i + when (indexMax < bits) $ do + c <- getNthClause vec i + let + sweep k = do + k' <- (indexMax .&.) <$> getNth keys k + setNth keys k k + if k' == i + then setNthClause vec k c + else getNthClause vec k' >>= setNthClause vec k >> sweep k' + sweep i + seek $ i + 1 + seek 0 + return limit + +-- | #M22 +-- +-- simplify : [void] -> [bool] +-- +-- __Description:__ +-- Simplify the clause database according to the current top-level assigment. Currently, the only +-- thing done here is the removal of satisfied clauses, but more things can be put here. +-- +{-# INLINABLE simplifyDB #-} +simplifyDB :: Solver -> IO Bool +simplifyDB s@Solver{..} = do + good <- getBool ok + if good + then do + p <- propagate s + if p /= NullClause + then setBool ok False >> return False + else do + -- Clear watcher lists: + n <- sizeOfStack trail + let + vec = asVec trail + loopOnLit ((< n) -> False) = return () + loopOnLit i = do + l <- getNth vec i + clearManager . getNthWatcher watches $ l + clearManager . getNthWatcher watches $ negateLit l + loopOnLit $ i + 1 + loopOnLit 0 + -- Remove satisfied clauses: + let + for :: Int -> IO Bool + for ((< 2) -> False) = return True + for t = do + let ptr = if t == 0 then learnts else clauses + vec' <- getClauseVector ptr + n' <- numberOfClauses ptr + let + loopOnVector :: Int -> Int -> IO Bool + loopOnVector ((< n') -> False) j = shrinkManager ptr (n' - j) >> return True + loopOnVector i j = do + c <- getNthClause vec' i + l <- locked s c + r <- simplify s c + if not l && r + then removeWatch s c >> loopOnVector (i + 1) j + else setNthClause vec' j c >> loopOnVector (i + 1) (j + 1) + loopOnVector 0 0 + ret <- for 0 + garbageCollect watches + return ret + else return False + +-- | #M22 +-- +-- search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] +-- +-- __Description:__ +-- Search for a model the specified number of conflicts. +-- NOTE: Use negative value for 'nof_conflicts' indicate infinity. +-- +-- __Output:__ +-- 'l_True' if a partial assigment that is consistent with respect to the clause set is found. If +-- all variables are decision variables, that means that the clause set is satisfiable. 'l_False' +-- if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. +{-# INLINABLE search #-} +search :: Solver -> Int -> Int -> IO LiftedBool +search s@Solver{..} nOfConflicts nOfLearnts = do + -- clear model + let + loop :: Int -> IO LiftedBool + loop conflictC = do + !confl <- propagate s + d <- decisionLevel s + if confl /= NullClause + then do + -- CONFLICT + incrementStat s NumOfBackjump 1 + r <- getInt rootLevel + if d == r + then do + -- Contradiction found: + analyzeFinal s confl False + return LFalse + else do +-- u <- (== 0) . (flip mod 5000) <$> getNth stats (fromEnum NumOfBackjump) +-- when u $ do +-- d <- getDouble varDecay +-- when (d < 0.95) $ modifyDouble varDecay (+ 0.01) + backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself + (s `cancelUntil`) . max backtrackLevel =<< getInt rootLevel + newLearntClause s $ asSizedVec litsLearnt + k <- sizeOfStack litsLearnt + when (k == 1) $ do + (v :: Var) <- lit2var <$> getNth (asVec litsLearnt) 0 + setNth level v 0 + varDecayActivity s + -- claDecayActivity s + loop $ conflictC + 1 + else do -- NO CONFLICT + -- Simplify the set of problem clauses: + when (d == 0) . void $ simplifyDB s -- our simplifier cannot return @False@ here + k1 <- numberOfClauses learnts + k2 <- nAssigns s + when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses + case () of + _ | k2 == nVars -> do + -- Model found: + forM_ [0 .. nVars - 1] $ \i -> setNthBool model i . (lTrue ==) =<< getNth assigns (i + 1) + return LTrue + _ | conflictC >= nOfConflicts -> do + -- Reached bound on number of conflicts + (s `cancelUntil`) =<< getInt rootLevel -- force a restart + claRescaleActivityAfterRestart s + incrementStat s NumOfRestart 1 + return Bottom + _ -> do + -- New variable decision: + v <- select s -- many have heuristic for polarity here + -- << #phasesaving + oldVal <- getNth phases v + unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@ + -- >> #phasesaving + loop conflictC + good <- getBool ok + if good then loop 0 else return LFalse + +-- | __Fig. 16. (p.20)__ +-- Main solve method. +-- +-- __Pre-condition:__ If assumptions are used, 'simplifyDB' must be +-- called right before using this method. If not, a top-level conflict (resulting in a +-- non-usable internal state) cannot be distinguished from a conflict under assumptions. +solve :: (Foldable t) => Solver -> t Lit -> IO Bool +solve s@Solver{..} assumps = do + -- PUSH INCREMENTAL ASSUMPTIONS: + let + injector :: Lit -> Bool -> IO Bool + injector _ False = return False + injector a True = do + b <- assume s a + if not b + then do -- conflict analyze + (confl :: Clause) <- getNthClause reason (lit2var a) + analyzeFinal s confl True + pushToStack conflict (negateLit a) + cancelUntil s 0 + return False + else do + confl <- propagate s + if confl /= NullClause + then do + analyzeFinal s confl True + cancelUntil s 0 + return False + else return True + good <- simplifyDB s + x <- if good then foldrM injector True assumps else return False + if not x + then return False + else do + setInt rootLevel =<< decisionLevel s + -- SOLVE: + nc <- fromIntegral <$> nClauses s + let + while :: Double -> Double -> IO Bool + while nOfConflicts nOfLearnts = do + status <- search s (floor nOfConflicts) (floor nOfLearnts) + if status == Bottom + then while (1.5 * nOfConflicts) (1.1 * nOfLearnts) + else cancelUntil s 0 >> return (status == LTrue) + while 100 (nc / 3.0) + +-- +-- 'enqueue' is defined in 'Solver'; most functions in M114 use 'unsafeEnqueue' +-- +{-# INLINABLE unsafeEnqueue #-} +unsafeEnqueue :: Solver -> Lit -> Clause -> IO () +unsafeEnqueue s@Solver{..} p from = do + let v = lit2var p + setNth assigns v $! if positiveLit p then lTrue else lFalse + setNth level v =<< decisionLevel s + setNthClause reason v from -- NOTE: @from@ might be NULL! + pushToStack trail p + +-- __Pre-condition:__ propagation queue is empty +{-# INLINE unsafeAssume #-} +unsafeAssume :: Solver -> Lit -> IO () +unsafeAssume s@Solver{..} p = do + pushToStack trailLim =<< sizeOfStack trail + unsafeEnqueue s p NullClause diff --git a/SAT/Mios/OptionParser.hs b/SAT/Mios/OptionParser.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/OptionParser.hs @@ -0,0 +1,133 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE Safe #-} + +-- | command line option parser for mios +module SAT.Mios.OptionParser + ( + MiosConfiguration (..) + , defaultConfiguration + , MiosProgramOption (..) + , miosDefaultOption + , miosOptions + , miosUsage + , miosParseOptions + , miosParseOptionsFromArgs + , toMiosConf + ) + where + +import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo) +import System.Environment (getArgs) +import SAT.Mios.Internal (MiosConfiguration (..), defaultConfiguration) + +-- | configuration swithces +data MiosProgramOption = MiosProgramOption + { + _targetFile :: Maybe String + , _outputFile :: Maybe String + , _confVariableDecayRate :: !Double +-- , _confClauseDecayRate :: Double +-- , _confRandomDecisionRate :: Int + , _confCheckAnswer :: !Bool + , _confVerbose :: !Bool + , _confTimeProbe :: !Bool + , _confStatProbe :: !Bool + , _confNoAnswer :: !Bool + , _validateAssignment :: !Bool + , _displayHelp :: !Bool + , _displayVersion :: !Bool + } + +-- | default option settings +miosDefaultOption :: MiosProgramOption +miosDefaultOption = MiosProgramOption + { + _targetFile = Just "" + , _outputFile = Nothing + , _confVariableDecayRate = variableDecayRate defaultConfiguration +-- , _confClauseDecayRate = clauseDecayRate defaultConfiguration +-- , _confRandomDecisionRate = randomDecisionRate defaultConfiguration + , _confCheckAnswer = False + , _confVerbose = False + , _confTimeProbe = False + , _confStatProbe = False + , _confNoAnswer = False + , _validateAssignment = False + , _displayHelp = False + , _displayVersion = False + } + +-- | definition of mios option +miosOptions :: [OptDescr (MiosProgramOption -> MiosProgramOption)] +miosOptions = + [ + Option ['d'] ["variable-decay-rate"] + (ReqArg (\v c -> c { _confVariableDecayRate = read v }) (show (_confVariableDecayRate miosDefaultOption))) + "[solver] variable activity decay rate (0.0 - 1.0)" +-- , Option ['c'] ["clause-decay-rate"] +-- (ReqArg (\v c -> c { _confClauseDecayRate = read v }) (show (_confClauseDecayRate miosDefaultOption))) +-- "[solver] clause activity decay rate (0.0 - 1.0)" +-- , Option ['r'] ["random-decision-rate"] +-- (ReqArg (\v c -> c { _confRandomDecisionRate = read v }) (show (_confRandomDecisionRate miosDefaultOption))) +-- "[solver] random selection rate (0 - 1000)" + , Option [':'] ["validate-assignment"] + (NoArg (\c -> c { _validateAssignment = True })) + "[solver] read an assignment from STDIN and validate it" + , Option [] ["validate"] + (NoArg (\c -> c { _confCheckAnswer = True })) + "[solver] self-check the (satisfied) answer" + , Option ['o'] ["output"] + (ReqArg (\v c -> c { _outputFile = Just v })"file") + "[option] filename to store the result" +{- + , Option [] ["stdin"] + (NoArg (\c -> c { _targetFile = Nothing })) + "[option] read a CNF from STDIN instead of a file" +-} + , Option ['v'] ["verbose"] + (NoArg (\c -> c { _confVerbose = True })) + "[option] display misc information" + , Option ['X'] ["hide-solution"] + (NoArg (\c -> c { _confNoAnswer = True })) + "[option] hide the solution" + , Option [] ["time"] + (NoArg (\c -> c { _confTimeProbe = True })) + "[option] display execution time" + , Option [] ["stat"] + (NoArg (\c -> c { _confStatProbe = True })) + "[option] display statistics information" + , Option ['h'] ["help"] + (NoArg (\c -> c { _displayHelp = True })) + "[misc] display this help message" + , Option [] ["version"] + (NoArg (\c -> c { _displayVersion = True })) + "[misc] display program ID" + ] + +-- | generates help message +miosUsage :: String -> String +miosUsage mes = usageInfo mes miosOptions + +-- | builds "MiosProgramOption" from string given as command option +miosParseOptions :: String -> [String] -> IO MiosProgramOption +miosParseOptions mes argv = + case getOpt Permute miosOptions argv of + (o, [], []) -> do + return $ foldl (flip id) miosDefaultOption o + (o, (n:_), []) -> do + let conf = foldl (flip id) miosDefaultOption o + return $ conf { _targetFile = Just n } + (_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes)) + +-- | builds "MiosProgramOption" from a String +miosParseOptionsFromArgs :: String -> IO MiosProgramOption +miosParseOptionsFromArgs mes = miosParseOptions mes =<< getArgs + +-- | converts "MiosProgramOption" into "SIHConfiguration" +toMiosConf :: MiosProgramOption -> MiosConfiguration +toMiosConf opts = MiosConfiguration + { + variableDecayRate = _confVariableDecayRate opts +-- , clauseDecayRate = _confClauseDecayRate opts +-- , randomDecisionRate = _confRandomDecisionRate opts + } diff --git a/SAT/Mios/Solver.hs b/SAT/Mios/Solver.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Solver.hs @@ -0,0 +1,611 @@ +{-# LANGUAGE + BangPatterns + , RecordWildCards + , ScopedTypeVariables + , TupleSections + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +-- | This is a part of MIOS; main data +module SAT.Mios.Solver + ( + -- * Solver + Solver (..) + , newSolver + -- * Misc Accessors + , nAssigns + , nClauses + , nLearnts + , decisionLevel + , valueVar + , valueLit + , locked + -- * State Modifiers + , addClause + , enqueue + , assume + , cancelUntil + , getModel + -- * Activities + , claBumpActivity +-- , claDecayActivity + , claRescaleActivityAfterRestart + , varBumpActivity + , varDecayActivity + , claActivityThreshold + -- * Stats + , StatIndex (..) + , getStat + , setStat + , incrementStat + , getStats + ) + where + +import Control.Monad ((<=<), forM_, unless, when) +import SAT.Mios.Types +import SAT.Mios.Internal +import SAT.Mios.Clause +import SAT.Mios.ClauseManager + +-- | __Fig. 2.(p.9)__ Internal State of the solver +data Solver = Solver + { + -- Public Interface + model :: !VecBool -- ^ If found, this vector has the model + , conflict :: !Stack -- ^ set of literals in the case of conflicts + -- Clause Database + , clauses :: !ClauseExtManager -- ^ List of problem constraints. + , learnts :: !ClauseExtManager -- ^ List of learnt clauses. + , watches :: !WatcherList -- ^ a list of constraint wathing 'p', literal-indexed + -- Assignment Management + , assigns :: !Vec -- ^ The current assignments indexed on variables; var-indexed + , phases :: !Vec -- ^ The last assignments indexed on variables; var-indexed + , trail :: !Stack -- ^ List of assignments in chronological order; var-indexed + , trailLim :: !Stack -- ^ Separator indices for different decision levels in 'trail'. + , qHead :: !IntSingleton -- ^ 'trail' is divided at qHead; assignments and queue + , reason :: !ClauseVector -- ^ For each variable, the constraint that implied its value; var-indexed + , level :: !Vec -- ^ For each variable, the decision level it was assigned; var-indexed + -- Variable Order + , activities :: !VecDouble -- ^ Heuristic measurement of the activity of a variable; var-indexed + , order :: !VarHeap -- ^ Keeps track of the dynamic variable order. + -- Configuration + , config :: !MiosConfiguration -- ^ search paramerters + , nVars :: !Int -- ^ number of variables +-- , claInc :: !DoubleSingleton -- ^ Clause activity increment amount to bump with. +-- , varDecay :: !DoubleSingleton -- ^ used to set 'varInc' + , varInc :: !DoubleSingleton -- ^ Variable activity increment amount to bump with. + , rootLevel :: !IntSingleton -- ^ Separates incremental and search assumptions. + -- Working Memory + , ok :: !BoolSingleton -- ^ return value holder + , an'seen :: !Vec -- ^ scratch var for 'analyze'; var-indexed + , an'toClear :: !Stack -- ^ ditto + , an'stack :: !Stack -- ^ ditto + , pr'seen :: !Vec -- ^ used in propagate + , litsLearnt :: !Stack -- ^ used to create a learnt clause + , lastDL :: !Stack -- ^ last decision level used in analyze + , stats :: !Vec -- ^ statistics information holder +{- + , lbd'seen :: !Vec -- ^ used in lbd computation + , lbd'key :: !IntSingleton -- ^ used in lbd computation +-} + } + +-- | returns an everything-is-initialized solver from the arguments +newSolver :: MiosConfiguration -> CNFDescription -> IO Solver +newSolver conf (CNFDescription nv nc _) = do + Solver + -- Public Interface + <$> newVecBool nv False -- model + <*> newStack nv -- coflict + -- Clause Database + <*> newManager nc -- clauses + <*> newManager nc -- learnts + <*> newWatcherList nv 2 -- watches + -- Assignment Management + <*> newVecWith (nv + 1) lBottom -- assigns + <*> newVecWith (nv + 1) lBottom -- phases + <*> newStack nv -- trail + <*> newStack nv -- trailLim + <*> newInt 0 -- qHead + <*> newClauseVector (nv + 1) -- reason + <*> newVecWith (nv + 1) (-1) -- level + -- Variable Order + <*> newVecDouble (nv + 1) 0 -- activities + <*> newVarHeap nv -- order + -- Configuration + <*> return conf -- config + <*> return nv -- nVars +-- <*> newDouble 1.0 -- claInc +-- <*> newDouble (variableDecayRate conf) -- varDecay + <*> newDouble 1.0 -- varInc + <*> newInt 0 -- rootLevel + -- Working Memory + <*> newBool True -- ok + <*> newVec (nv + 1) -- an'seen + <*> newStack nv -- an'toClear + <*> newStack nv -- an'stack + <*> newVecWith (nv + 1) (-1) -- pr'seen + <*> newStack nv -- litsLearnt + <*> newStack nv -- lastDL + <*> newVec (1 + fromEnum (maxBound :: StatIndex)) -- stats +{- +-- <*> newVec nv -- lbd'seen +-- <*> newInt 0 -- lbd'key +-} + +-------------------------------------------------------------------------------- +-- Accessors + +-- | returns the number of current assigments +{-# INLINE nAssigns #-} +nAssigns :: Solver -> IO Int +nAssigns = sizeOfStack . trail + +-- | returns the number of constraints (clauses) +{-# INLINE nClauses #-} +nClauses :: Solver -> IO Int +nClauses = numberOfClauses . clauses + +-- | returns the number of learnt clauses +{-# INLINE nLearnts #-} +nLearnts :: Solver -> IO Int +nLearnts = numberOfClauses . learnts + +-- | return the model as a list of literal +getModel :: Solver -> IO [Int] +getModel s = zipWith (\n b -> if b then n else negate n) [1 .. ] <$> asList (model s) + +-- | returns the current decision level +{-# INLINE decisionLevel #-} +decisionLevel :: Solver -> IO Int +decisionLevel = sizeOfStack . trailLim + +-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Var' +{-# INLINE valueVar #-} +valueVar :: Solver -> Var -> IO Int +valueVar = getNth . assigns + +-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit' +{-# INLINE valueLit #-} +valueLit :: Solver -> Lit -> IO Int -- FIXME: LiftedBool +valueLit (assigns -> a) !p = (\x -> if positiveLit p then x else negate x) <$> getNth a (lit2var p) + +-- | __Fig. 7. (p.11)__ +-- returns @True@ if the clause is locked (used as a reason). __Learnt clauses only__ +{-# INLINE locked #-} +locked :: Solver -> Clause -> IO Bool +locked s c = (c ==) <$> (getNthClause (reason s) . lit2var =<< getNth (lits c) 1) + +-------------------------------------------------------------------------------- Statistics + +-- | stat index +data StatIndex = + NumOfBackjump + | NumOfRestart + deriving (Bounded, Enum, Eq, Ord, Read, Show) + +-- | returns the value of 'StatIndex' +{-# INLINE getStat #-} +getStat :: Solver -> StatIndex -> IO Int +getStat (stats -> v) (fromEnum -> i) = getNth v i + +-- | sets to 'StatIndex' +{-# INLINE setStat #-} +setStat :: Solver -> StatIndex -> Int -> IO () +setStat (stats -> v) (fromEnum -> i) x = setNth v i x + +-- | increments a stat data corresponding to 'StatIndex' +{-# INLINE incrementStat #-} +incrementStat :: Solver -> StatIndex -> Int -> IO () +incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i + +-- | returns the statistics as list +{-# INLINABLE getStats #-} +getStats :: Solver -> IO [(StatIndex, Int)] +getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex] + +-------------------------------------------------------------------------------- State Modifiers + +-- | returns @False@ if a conflict has occured. +-- This function is called only before the solving phase to register the given clauses. +{-# INLINABLE addClause #-} +addClause :: Solver -> Vec -> IO Bool +addClause s@Solver{..} vecLits = do + result <- clauseNew s vecLits False + case result of + (False, _) -> return False -- Conflict occured + (True, c) -> do + unless (c == NullClause) $ pushClause clauses c + return True -- No conflict + +-- | __Fig. 8. (p.12)__ create a new clause and adds it to watcher lists +-- Constructor function for clauses. Returns @False@ if top-level conflict is determined. +-- @outClause@ may be set to Null if the new clause is already satisfied under the current +-- top-level assignment. +-- +-- __Post-condition:__ @ps@ is cleared. For learnt clauses, all +-- literals will be false except @lits[0]@ (this by design of the 'analyze' method). +-- For the propagation to work, the second watch must be put on the literal which will +-- first be unbound by backtracking. (Note that none of the learnt-clause specific things +-- needs to done for a user defined contraint type.) +{-# INLINABLE clauseNew #-} +clauseNew :: Solver -> Vec -> Bool -> IO (Bool, Clause) +clauseNew s@Solver{..} ps isLearnt = do + -- now ps[0] is the number of living literals + exit <- do + let + handle :: Int -> Int -> Int -> IO Bool + handle j l n -- removes duplicates, but returns @True@ if this clause is satisfied + | j > n = return False + | otherwise = do + y <- getNth ps j + case () of + _ | y == l -> do -- finds a duplicate + swapBetween ps j n + modifyNth ps (subtract 1) 0 + handle j l (n - 1) + _ | - y == l -> setNth ps 0 0 >> return True -- p and negateLit p occurs in ps + _ -> handle (j + 1) l n + loopForLearnt :: Int -> IO Bool + loopForLearnt i = do + n <- getNth ps 0 + if n < i + then return False + else do + l <- getNth ps i + sat <- handle (i + 1) l n + if sat + then return True + else loopForLearnt $ i + 1 + loop :: Int -> IO Bool + loop i = do + n <- getNth ps 0 + if n < i + then return False + else do + l <- getNth ps i -- check the i-th literal's satisfiability + sat <- valueLit s l -- any literal in ps is true + case sat of + 1 -> setNth ps 0 0 >> return True + -1 -> do + swapBetween ps i n + modifyNth ps (subtract 1) 0 + loop i + _ -> do + sat' <- handle (i + 1) l n + if sat' + then return True + else loop $ i + 1 + if isLearnt then loopForLearnt 1 else loop 1 + k <- getNth ps 0 + case k of + 0 -> return (exit, NullClause) + 1 -> do + l <- getNth ps 1 + (, NullClause) <$> enqueue s l NullClause + _ -> do + -- allocate clause: + c <- newClauseFromVec isLearnt ps + let vec = asVec c + when isLearnt $ do + -- Pick a second literal to watch: + let + findMax :: Int -> Int -> Int -> IO Int + findMax ((< k) -> False) j _ = return j + findMax i j val = do + v' <- lit2var <$> getNth vec i + a <- getNth assigns v' + b <- getNth level v' + if (a /= lBottom) && (val < b) + then findMax (i + 1) i b + else findMax (i + 1) j val + -- Let @max_i@ be the index of the literal with highest decision level + max_i <- findMax 0 0 0 + swapBetween vec 1 max_i + -- check literals occurences + -- x <- asList c + -- unless (length x == length (nub x)) $ error "new clause contains a element doubly" + -- Bumping: + claBumpActivity s c -- newly learnt clauses should be considered active + forM_ [0 .. k -1] $ varBumpActivity s . lit2var <=< getNth vec -- variables in conflict clauses are bumped + -- Add clause to watcher lists: + l0 <- negateLit <$> getNth vec 0 + pushClauseWithKey (getNthWatcher watches l0) c 0 + l1 <- negateLit <$> getNth vec 1 + pushClauseWithKey (getNthWatcher watches l1) c 0 + return (True, c) + +-- | __Fig. 9 (p.14)__ +-- Puts a new fact on the propagation queue, as well as immediately updating the variable's value +-- in the assignment vector. If a conflict arises, @False@ is returned and the propagation queue is +-- cleared. The parameter 'from' contains a reference to the constraint from which 'p' was +-- propagated (defaults to @Nothing@ if omitted). +{-# INLINABLE enqueue #-} +enqueue :: Solver -> Lit -> Clause -> IO Bool +enqueue s@Solver{..} p from = do +{- + -- bump psedue lbd of @from@ + when (from /= NullClause && learnt from) $ do + l <- getInt (lbd from) + k <- (12 +) <$> decisionLevel s + when (k < l) $ setInt (lbd from) k +-} + let signumP = if positiveLit p then lTrue else lFalse + let v = lit2var p + val <- valueVar s v + if val /= lBottom + then do -- Existing consistent assignment -- don't enqueue + return $ val == signumP + else do + -- New fact, store it + setNth assigns v signumP + setNth level v =<< decisionLevel s + setNthClause reason v from -- NOTE: @from@ might be NULL! + pushToStack trail p + return True + +-- | __Fig. 12 (p.17)__ +-- returns @False@ if immediate conflict. +-- +-- __Pre-condition:__ propagation queue is empty +{-# INLINE assume #-} +assume :: Solver -> Lit -> IO Bool +assume s p = do + pushToStack (trailLim s) =<< sizeOfStack (trail s) + enqueue s p NullClause + +-- | #M22: Revert to the states at given level (keeping all assignment at 'level' but not beyond). +{-# INLINABLE cancelUntil #-} +cancelUntil :: Solver -> Int -> IO () +cancelUntil s@Solver{..} lvl = do + dl <- decisionLevel s + when (lvl < dl) $ do + let tr = asVec trail + let tl = asVec trailLim + lim <- getNth tl lvl + ts <- sizeOfStack trail + ls <- sizeOfStack trailLim + let + loopOnTrail :: Int -> IO () + loopOnTrail ((lim <=) -> False) = return () + loopOnTrail c = do + x <- lit2var <$> getNth tr c + setNth phases x =<< getNth assigns x + setNth assigns x lBottom + -- #reason to set reason Null + -- if we don't clear @reason[x] :: Clause@ here, @reason[x]@ remains as locked. + -- This means we can't reduce it from clause DB and affects the performance. + setNthClause reason x NullClause -- 'analyze` uses reason without checking assigns + -- FIXME: #polarity https://github.com/shnarazk/minisat/blosb/master/core/Solver.cc#L212 + undo s x + -- insertHeap s x -- insertVerOrder + loopOnTrail $ c - 1 + loopOnTrail $ ts - 1 + shrinkStack trail (ts - lim) + shrinkStack trailLim (ls - lvl) + setInt qHead =<< sizeOfStack trail + +-------------------------------------------------------------------------------- VarOrder + +-- | Interfate to select a decision var based on variable activity. +instance VarOrder Solver where + -- | __Fig. 6. (p.10)__ + -- Creates a new SAT variable in the solver. + newVar _ = return 0 + -- i <- nVars s + -- Version 0.4:: push watches =<< newVec -- push' + -- Version 0.4:: push watches =<< newVec -- push' + -- push undos =<< newVec -- push' + -- push reason NullClause -- push' + -- push assigns lBottom + -- push level (-1) + -- push activities (0.0 :: Double) + -- newVar order + -- growQueueSized (i + 1) propQ + -- return i + {-# SPECIALIZE INLINE update :: Solver -> Var -> IO () #-} + update = increaseHeap + {-# SPECIALIZE INLINE undo :: Solver -> Var -> IO () #-} + undo s v = inHeap s v >>= (`unless` insertHeap s v) + {-# SPECIALIZE INLINE select :: Solver -> IO Var #-} + select s = do + let + asg = assigns s + -- | returns the most active var (heap-based implementation) + loop :: IO Var + loop = do + n <- numElementsInHeap s + if n == 0 + then return 0 + else do + v <- getHeapRoot s + x <- getNth asg v + if x == lBottom then return v else loop + loop + +-------------------------------------------------------------------------------- Activities + +varActivityThreshold :: Double +varActivityThreshold = 1e100 + +claActivityThreshold :: Double +claActivityThreshold = 1e20 + +-- | __Fig. 14 (p.19)__ Bumping of clause activity +{-# INLINE varBumpActivity #-} +varBumpActivity :: Solver -> Var -> IO () +varBumpActivity s@Solver{..} x = do + !a <- (+) <$> getNthDouble x activities <*> getDouble varInc + setNthDouble x activities a + when (varActivityThreshold < a) $ varRescaleActivity s + update s x -- update the position in heap + +-- | __Fig. 14 (p.19)__ +{-# INLINE varDecayActivity #-} +varDecayActivity :: Solver -> IO () +varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config) +-- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay + +-- | __Fig. 14 (p.19)__ +{-# INLINE varRescaleActivity #-} +varRescaleActivity :: Solver -> IO () +varRescaleActivity Solver{..} = do + forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (/ varActivityThreshold) + modifyDouble varInc (/ varActivityThreshold) + +-- | __Fig. 14 (p.19)__ +{-# INLINE claBumpActivity #-} +claBumpActivity :: Solver -> Clause -> IO () +claBumpActivity s Clause{..} = do + dl <- decisionLevel s + a <- (fromIntegral dl +) <$> getDouble activity + setDouble activity a + -- setBool protected True + when (claActivityThreshold <= a) $ claRescaleActivity s + +{- +-- | __Fig. 14 (p.19)__ +{-# INLINE claDecayActivity #-} +claDecayActivity :: Solver -> IO () +claDecayActivity Solver{..} = modifyDouble claInc (/ clauseDecayRate config) +-} + +-- | __Fig. 14 (p.19)__ +{-# INLINE claRescaleActivity #-} +claRescaleActivity :: Solver -> IO () +claRescaleActivity Solver{..} = do + vec <- getClauseVector learnts + n <- numberOfClauses learnts + let + loopOnVector :: Int -> IO () + loopOnVector ((< n) -> False) = return () + loopOnVector i = do + c <- getNthClause vec i + modifyDouble (activity c) (/ claActivityThreshold) + loopOnVector $ i + 1 + loopOnVector 0 + -- modifyDouble claInc (/ claActivityThreshold) + +-- | __Fig. 14 (p.19)__ +{-# INLINE claRescaleActivityAfterRestart #-} +claRescaleActivityAfterRestart :: Solver -> IO () +claRescaleActivityAfterRestart Solver{..} = do + vec <- getClauseVector learnts + n <- numberOfClauses learnts + let + loopOnVector :: Int -> IO () + loopOnVector ((< n) -> False) = return () + loopOnVector i = do + c <- getNthClause vec i + d <- sizeOfClause c + if d < 9 + then modifyDouble (activity c) sqrt + else setDouble (activity c) 0 + setBool (protected c) False + loopOnVector $ i + 1 + loopOnVector 0 + +-------------------------------------------------------------------------------- VarHeap + +-- | 'VarHeap' is a heap tree built from two 'Vec' +-- This implementation is identical wtih that in Minisat-1.14 +-- Note: the zero-th element of @heap@ is used for holding the number of elements +-- Note: VarHeap itself is not a @VarOrder@, because it requires a pointer to solver +data VarHeap = VarHeap + { + heap :: Vec -- order to var + , idxs :: Vec -- var to order (index) + } + +newVarHeap :: Int -> IO VarHeap +newVarHeap n = do + v1 <- newVec (n + 1) + v2 <- newVec (n + 1) + let + loop :: Int -> IO () + loop ((<= n) -> False) = setNth v1 0 n >> setNth v2 0 n + loop i = setNth v1 i i >> setNth v2 i i >> loop (i + 1) + loop 1 + return $ VarHeap v1 v2 + +{-# INLINE numElementsInHeap #-} +numElementsInHeap :: Solver -> IO Int +numElementsInHeap (order -> heap -> h) = getNth h 0 + +{-# INLINE inHeap #-} +inHeap :: Solver -> Var -> IO Bool +inHeap (order -> idxs -> at) n = (/= 0) <$> getNth at n + +{-# INLINE increaseHeap #-} +increaseHeap :: Solver -> Int -> IO () +increaseHeap s@(order -> idxs -> at) n = inHeap s n >>= (`when` (percolateUp s =<< getNth at n)) + +{-# INLINABLE percolateUp #-} +percolateUp :: Solver -> Int -> IO () +percolateUp Solver{..} start = do + let VarHeap to at = order + v <- getNth to start + ac <- getNthDouble v activities + let + loop :: Int -> IO () + loop i = do + let iP = div i 2 -- parent + if iP == 0 + then setNth to i v >> setNth at v i -- end + else do + v' <- getNth to iP + acP <- getNthDouble v' activities + if ac > acP + then setNth to i v' >> setNth at v' i >> loop iP -- loop + else setNth to i v >> setNth at v i -- end + loop start + +{-# INLINABLE percolateDown #-} +percolateDown :: Solver -> Int -> IO () +percolateDown Solver{..} start = do + let (VarHeap to at) = order + n <- getNth to 0 + v <- getNth to start + ac <- getNthDouble v activities + let + loop :: Int -> IO () + loop i = do + let iL = 2 * i -- left + if iL <= n + then do + let iR = iL + 1 -- right + l <- getNth to iL + r <- getNth to iR + acL <- getNthDouble l activities + acR <- getNthDouble r activities + let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL) + if ac' > ac + then setNth to i child >> setNth at child i >> loop ci + else setNth to i v >> setNth at v i -- end + else setNth to i v >> setNth at v i -- end + loop start + +{-# INLINE insertHeap #-} +insertHeap :: Solver -> Var -> IO () +insertHeap s@(order -> VarHeap to at) v = do + n <- (1 +) <$> getNth to 0 + setNth at v n + setNth to n v + setNth to 0 n + percolateUp s n + +-- | renamed from 'getmin' +{-# INLINE getHeapRoot #-} +getHeapRoot :: Solver -> IO Int +getHeapRoot s@(order -> VarHeap to at) = do + r <- getNth to 1 + l <- getNth to =<< getNth to 0 -- the last element's value + setNth to 1 l + setNth at l 1 + setNth at r 0 + modifyNth to (subtract 1) 0 -- pop + n <- getNth to 0 + when (1 < n) $ percolateDown s 1 + return r diff --git a/SAT/Mios/Types.hs b/SAT/Mios/Types.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Types.hs @@ -0,0 +1,269 @@ +{-# LANGUAGE + BangPatterns + , FlexibleContexts + , FlexibleInstances + , FunctionalDependencies + , MultiParamTypeClasses + #-} +{-# LANGUAGE Trustworthy #-} + +-- | Basic data types used throughout mios. +module SAT.Mios.Types + ( + -- Singleton + module SAT.Mios.Data.Singleton + -- Fixed Unboxed Mutable Int Vector + , module SAT.Mios.Data.Vec + -- Abstract interfaces + , VectorFamily (..) + -- * Variable + , Var + , bottomVar + , int2var + -- * Internal encoded Literal + , Lit + , lit2int + , int2lit + , bottomLit + , newLit + , positiveLit + , lit2var + , var2lit + , negateLit + -- * Assignment + , LiftedBool (..) + , lbool + , lFalse + , lTrue + , lBottom + , VarOrder (..) + -- * CNF + , CNFDescription (..) + ) + where + +import Control.Monad (forM) +import Data.Bits +import qualified Data.Vector.Unboxed.Mutable as UV +import SAT.Mios.Data.Singleton +import SAT.Mios.Data.Vec + +-- | Public interface as /Container/ +class VectorFamily s t | s -> t where + -- * Size operations + -- | erases all elements in it + clear :: s -> IO () + clear = error "no default method for clear" + -- * Debug + -- | dump the contents + dump :: Show t => String -> s -> IO String + dump msg _ = error $ msg ++ ": no defalut method for dump" + -- | get a raw data + asVec :: s -> UV.IOVector Int + asVec = error "asVector undefined" + -- | converts into a list + asList :: s -> IO [t] + asList = error "asList undefined" + {-# MINIMAL dump #-} + +-- | provides 'clear' and 'size' +instance VectorFamily Vec Int where + clear = error "Vec.clear" + {-# SPECIALIZE INLINE asList :: Vec -> IO [Int] #-} + asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v + dump str v = (str ++) . show <$> asList v + {-# SPECIALIZE INLINE asVec :: Vec -> Vec #-} + asVec = id + +-- | represents "Var" +type Var = Int + +-- | Special constant in 'Var' (p.7) +bottomVar :: Var +bottomVar = 0 + +-- | converts a usual Int as literal to an internal 'Var' presentation +-- +-- >>> int2var 1 +-- 1 -- the first literal is the first variable +-- >>> int2var 2 +-- 2 -- literal @2@ is variable 2 +-- >>> int2var (-2) +-- 2 -- literal @-2@ is corresponding to variable 2 +-- +{-# INLINE int2var #-} +int2var = abs + +-- | The literal data has an 'index' method which converts the literal to +-- a "small" integer suitable for array indexing. The 'var' method returns +-- the underlying variable of the literal, and the 'sign' method if the literal +-- is signed (False for /x/ and True for /-x/). +type Lit = Int + +-- | Special constant in 'Lit' (p.7) +bottomLit :: Lit +bottomLit = 0 + +-- | converts "Var" into 'Lit' +newLit :: Var -> Lit +newLit = error "newLit undefined" + +-- | returns @True@ if the literal is positive +{-# INLINE positiveLit #-} +positiveLit :: Lit -> Bool +positiveLit = even + +-- | negates literal +-- +-- >>> negateLit 2 +-- 3 +-- >>> negateLit 3 +-- 2 +-- >>> negateLit 4 +-- 5 +-- >>> negateLit 5 +-- 4 +{-# INLINE negateLit #-} +negateLit :: Lit -> Lit +negateLit !l = complementBit l 0 -- if even l then l + 1 else l - 1 + +---------------------------------------- +----------------- Var +---------------------------------------- + +-- | converts 'Lit' into 'Var' +-- +-- >>> lit2var 2 +-- 1 +-- >>> lit2var 3 +-- 1 +-- >>> lit2var 4 +-- 2 +-- >>> lit2var 5 +-- 2 +{-# INLINE lit2var #-} +lit2var :: Lit -> Var +lit2var !n = shiftR n 1 + +-- | converts a 'Var' to the corresponing literal +-- +-- >>> var2lit 1 True +-- 2 +-- >>> var2lit 1 False +-- 3 +-- >>> var2lit 2 True +-- 4 +-- >>> var2lit 2 False +-- 5 +{-# INLINE var2lit #-} +var2lit :: Var -> Bool -> Lit +var2lit !v True = shiftL v 1 +var2lit !v _ = shiftL v 1 + 1 + +---------------------------------------- +----------------- Int +---------------------------------------- + +-- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@ +-- +-- >>> int2lit 1 +-- 2 +-- >>> int2lit (-1) +-- 3 +-- >>> int2lit 2 +-- 4 +-- >>> int2lit (-2) +-- 5 +-- +{-# INLINE int2lit #-} +int2lit :: Int -> Lit +int2lit n + | 0 < n = 2 * n + | otherwise = -2 * n + 1 + +-- | converts `Lit' into 'Int' as @int2lit . lit2int == id@ +-- +-- >>> lit2int 2 +-- 1 +-- >>> lit2int 3 +-- -1 +-- >>> lit2int 4 +-- 2 +-- >>> lit2int 5 +-- -2 +{-# INLINE lit2int #-} +lit2int :: Lit -> Int +lit2int l = case divMod l 2 of + (i, 0) -> i + (i, _) -> - i + +-- | Lifted Boolean domain (p.7) that extends 'Bool' with "⊥" means /undefined/ +-- design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2. +data LiftedBool = Bottom | LFalse | LTrue + deriving (Bounded, Eq, Ord, Read, Show) + +instance Enum LiftedBool where + {-# SPECIALIZE INLINE toEnum :: Int -> LiftedBool #-} + toEnum 1 = LTrue + toEnum (-1) = LFalse + toEnum _ = Bottom + {-# SPECIALIZE INLINE fromEnum :: LiftedBool -> Int #-} + fromEnum Bottom = 0 + fromEnum LFalse = 1 + fromEnum LTrue = 2 + +-- | converts 'Bool' into 'LBool' +{-# INLINE lbool #-} +lbool :: Bool -> LiftedBool +lbool True = LTrue +lbool False = LFalse + +-- | A contant representing False +lFalse:: Int +lFalse = -1 + +-- | A constant representing True +lTrue :: Int +lTrue = 1 + +-- | A constant for "undefined" +lBottom :: Int +lBottom = 0 + +-- | Assisting ADT for the dynamic variable ordering of the solver. +-- The constructor takes references to the assignment vector and the activity +-- vector of the solver. The method 'select' will return the unassigned variable +-- with the highest activity. +class VarOrder o where + -- | constructor + newVarOrder :: (VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO o + newVarOrder _ _ = error "newVarOrder undefined" + + -- | Called when a new variable is created. + newVar :: o -> IO Var + newVar = error "newVar undefined" + + -- | Called when variable has increased in activity. + update :: o -> Var -> IO () + update _ = error "update undefined" + + -- | Called when all variables have been assigned new activities. + updateAll :: o -> IO () + updateAll = error "updateAll undefined" + + -- | Called when variable is unbound (may be selected again). + undo :: o -> Var -> IO () + undo _ _ = error "undo undefined" + + -- | Called to select a new, unassigned variable. + select :: o -> IO Var + select = error "select undefined" + +-- | misc information on CNF +data CNFDescription = CNFDescription + { + _numberOfVariables :: !Int -- ^ number of variables + , _numberOfClauses :: !Int -- ^ number of clauses + , _pathname :: Maybe FilePath -- ^ given filename + } + deriving (Eq, Ord, Show) diff --git a/SAT/Mios/Util/BoolExp.hs b/SAT/Mios/Util/BoolExp.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/BoolExp.hs @@ -0,0 +1,244 @@ +{-# LANGUAGE BangPatterns, FlexibleInstances, ViewPatterns, UndecidableInstances #-} +{-# LANGUAGE Safe #-} + +-- | Boolean Expression module to build CNF from arbitrary expressions +-- Tseitin translation: http://en.wikipedia.org/wiki/Tseitin_transformation +module SAT.Mios.Util.BoolExp + ( + -- * Class & Type + BoolComponent (..) + , BoolForm (..) + -- * Expression contructors + , (-|-) + , (-&-) + , (-=-) + , (-!-) + , (->-) + , neg + -- * List Operation + , disjunctionOf + , (-|||-) + , conjunctionOf + , (-&&&-) + -- * Convert function + , asList + , asList_ + , asLatex + , asLatex_ + , numberOfVariables + , numberOfClauses + , tseitinBase + ) + where + +import Data.List (foldl', intercalate) + +-- | the start index for the generated variables by Tseitin encoding +tseitinBase :: Int +tseitinBase = 1600000 + +data L = L Int + +-- | class of objects that can be interpeted as a bool expression +class BoolComponent a where + toBF :: a -> BoolForm -- lift to BoolForm + +-- | CNF expression +data BoolForm = Cnf (Int, Int) [[Int]] + deriving (Eq, Show) + +instance BoolComponent Int where + toBF a = Cnf (abs a, max tseitinBase (abs a)) [[a]] + +instance BoolComponent L where + toBF (L a) = Cnf (abs a, max tseitinBase (abs a)) [[a]] + +instance BoolComponent [Char] where + toBF (read -> a) = Cnf (abs a, max tseitinBase (abs a)) [[a]] + +instance BoolComponent BoolForm where + toBF = id + +-- | returns the number of variables in the 'BoolForm' +numberOfVariables :: BoolForm -> Int +numberOfVariables (Cnf (a, b) _) = a + b - tseitinBase + +-- | returns the number of clauses in the 'BoolForm' +numberOfClauses :: BoolForm -> Int +numberOfClauses (Cnf _ l) = length l + +boolFormTrue = Cnf (-1, 1) [] +boolFormFalse = Cnf (-1, -1) [] + +instance BoolComponent Bool where + toBF True = boolFormTrue + toBF False = boolFormFalse + +isTrue :: BoolForm -> Bool +isTrue = (== boolFormTrue) + +isFalse :: BoolForm -> Bool +isFalse = (== boolFormFalse) + +-- | return a 'clause' list only if it contains some real clause (not a literal) +clausesOf :: BoolForm -> [[Int]] +clausesOf cnf@(Cnf _ [[]]) = [] +clausesOf cnf@(Cnf _ [[x]]) = [] +clausesOf cnf@(Cnf _ l) = l + +maxRank :: BoolForm -> Int +maxRank (Cnf (n, _) _) = n + +-- | returns the number of valiable used as the output of this expression. +-- and returns itself it the expression is a literal. +-- Otherwise the number is a integer larger than 'tseitinBase'. +-- Therefore @1 + max tseitinBase the-returned-value@ is the next literal variable for future. +tseitinNumber :: BoolForm -> Int +tseitinNumber (Cnf (m, n) [[x]]) = x +tseitinNumber (Cnf (_, n) _) = n + +renumber :: Int -> BoolForm -> (BoolForm, Int) +renumber base (Cnf (m, n) l) + | l == [] = (Cnf (m, n) l, 0) + | tseitinBase < base = (Cnf (m, n') l', n') + | otherwise = (Cnf (n', tseitinBase) l', n') + where + l' = map (map f) l + n' = maximum $ map maximum l' + offset = base - tseitinBase - 1 + f x = if abs x < tseitinBase then x else signum x * (abs x + offset) + +instance Ord BoolForm where + compare (Cnf _ a) (Cnf _ b) = compare a b + +-- | disjunction constructor +-- +-- >>> asList $ "3" -|- "4" +-- [[3,4,-5],[-3,5],[-4,5]] +-- +-- >>> asList (("3" -|- "4") -|- "-1") +-- [[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]] +-- +(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> e1) -|- (toBF -> e2') + | isTrue e1 || isTrue e2' = boolFormTrue + | isFalse e1 && isFalse e2' = boolFormFalse + | isFalse e1 = e2' + | isFalse e2' = e1 + | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[a, b, - c], [- a, c], [- b, c]] + where + a = tseitinNumber e1 + (e2, b) = renumber (1 + max tseitinBase a) e2' + m = max (maxRank e1) (maxRank e2) + c = 1 + max tseitinBase (max a b) + +-- | conjunction constructor +-- +-- >>> asList $ "3" -&- "-2" +-- [[-3,2,4],[3,-4],[-2,-4]] +-- +-- >>> asList $ "3" -|- ("1" -&- "2") +-- [[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]] +-- +(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> e1) -&- (toBF -> e2') + | isTrue e1 && isTrue e2' = boolFormTrue + | isFalse e1 || isFalse e2' = boolFormFalse + | isTrue e1 = e2' + | isTrue e2' = e1 + | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[- a, - b, c], [a, - c], [b, - c]] + where + a = tseitinNumber e1 + (e2, b) = renumber (1 + max tseitinBase a) e2' + m = max (maxRank e1) (maxRank e2) + c = 1 + max tseitinBase (max a b) + +-- | negate a form +-- +-- >>> asList $ neg ("1" -|- "2") +-- [[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]] +neg :: (BoolComponent a) => a -> BoolForm +neg (toBF -> e) = + Cnf (m, c) $ clausesOf e ++ [[- a, - c], [a, c]] + where + a = tseitinNumber e + m = maxRank e + c = 1 + max tseitinBase a + +-- | equal on BoolForm +(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> e1) -=- (toBF -> e2) = (e1 -&- e2) -|- (neg e1 -&- neg e2) + +-- | negation on BoolForm +(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> e1) -!- (toBF -> e2) = (neg e1 -&- e2) -|- (e1 -&- neg e2) + +-- | implication as a short cut +-- +-- >>> asList ("1" ->- "2") +-- [[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]] +(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm +(toBF -> a) ->- (toBF -> b) = (neg a) -|- b + +-- | merge [BoolForm] by '(-|-)' +disjunctionOf :: [BoolForm] -> BoolForm +disjunctionOf [] = boolFormFalse +disjunctionOf (x:l) = foldl' (-|-) x l + +-- | an alias of 'disjunctionOf' +(-|||-) = disjunctionOf + +-- | merge [BoolForm] by '(-&-)' +conjunctionOf :: [BoolForm] -> BoolForm +conjunctionOf [] = boolFormTrue +conjunctionOf (x:l) = foldl' (-&-) x l + +-- | an alias of 'conjunctionOf' +(-&&&-) = conjunctionOf + +-- | converts a BoolForm to "[[Int]]" +asList_ :: BoolForm -> [[Int]] +asList_ cnf@(Cnf (m,_) _) + | isTrue cnf = [] + | isFalse cnf = [[]] + | otherwise = l' + where + (Cnf _ l', _) = renumber (m + 1) cnf + +-- | converts a *satisfied* BoolForm to "[[Int]]" +asList :: BoolForm -> [[Int]] +asList cnf@(Cnf (m,n) l) + | isTrue cnf = [] + | isFalse cnf = [[]] + | n <= tseitinBase = l + | otherwise = [m'] : l' + where + (Cnf (m', _) l', _) = renumber (m + 1) cnf + +-- | make latex string from CNF, using 'asList_' +-- +-- >>> asLatex $ "3" -|- "4" +-- "\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n" +-- +asLatex_ :: BoolForm -> String +asLatex_ b = beg ++ s ++ end + where + beg = "\\begin{displaymath}\n" + end = "\n\\end{displaymath}\n" + s = intercalate " \\wedge " [ makeClause c | c <- asList_ b] + makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")" + makeLiteral l + | 0 < l = " x_{" ++ show l ++ "} " + | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} " + +-- | make latex string from CNF, using 'asList' +asLatex :: BoolForm -> String +asLatex b = beg ++ s ++ end + where + beg = "\\begin{displaymath}\n" + end = "\n\\end{displaymath}\n" + s = intercalate " \\wedge " [ makeClause c | c <- asList b] + makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")" + makeLiteral l + | 0 < l = " x_{" ++ show l ++ "} " + | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} " diff --git a/SAT/Mios/Util/CNFIO.hs b/SAT/Mios/Util/CNFIO.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/CNFIO.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE Safe #-} + +-- | Read/Write a CNF file only with ghc standard libraries +module SAT.Mios.Util.CNFIO + ( + -- * Input + fromFile + , clauseListFromFile + , fromMinisatOutput + , clauseListFromMinisatOutput + -- * Output + , toFile + , toCNFString + , asCNFString + , asCNFString_ + -- * Bool Operation + , module SAT.Mios.Util.BoolExp + ) + where +import SAT.Mios.Util.CNFIO.Reader +import SAT.Mios.Util.CNFIO.Writer +import SAT.Mios.Util.CNFIO.MinisatReader +import SAT.Mios.Util.BoolExp + +-- | String from BoolFrom +asCNFString :: BoolForm -> String +asCNFString = toCNFString . asList + +-- | String from BoolFrom +asCNFString_ :: BoolForm -> String +asCNFString_ = toCNFString . asList_ diff --git a/SAT/Mios/Util/CNFIO/MinisatReader.hs b/SAT/Mios/Util/CNFIO/MinisatReader.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/CNFIO/MinisatReader.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE Safe #-} + +-- | Read an output file of minisat +module SAT.Mios.Util.CNFIO.MinisatReader + ( + -- * Interface + fromMinisatOutput + , clauseListFromMinisatOutput + ) + where +-- import Control.Applicative ((<$>), (<*>), (<*), (*>)) +import Data.Char +import Text.ParserCombinators.ReadP + +-- parser +-- |parse a non-signed integer +{-# INLINE pint #-} +pint = do + n <- munch isDigit + return (read n :: Int) + +{-# INLINE mint #-} +mint = do + char '-' + n <- munch isDigit + return (- (read n::Int)) + +-- |parse a (signed) integer +{-# INLINE int #-} +int = mint <++ pint + +-- |return integer list that terminates at zero +{-# INLINE seqNums #-} +seqNums = do + skipSpaces + x <- int + skipSpaces + if (x == 0) then return [] else (x :) <$> seqNums + +-- |top level interface for parsing CNF +{-# INLINE parseMinisatOutput #-} +parseMinisatOutput :: ReadP ((Int, Int), [Int]) +parseMinisatOutput = do + string "SAT" + skipSpaces + l <- seqNums + return ((length l,0), l) + +-- |read a minisat output: +-- ((numbefOfVariables, 0), [Literal]) +-- +-- >>> fromFile "result" +-- ((3, 0), [1, -2, 3]) +-- +{-# INLINE fromMinisatOutput #-} +fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int])) +fromMinisatOutput f = do + c <- readFile f + case readP_to_S parseMinisatOutput c of + [(a, _)] -> return $ Just a + _ -> return Nothing + +-- | return clauses as [[Int]] from 'file' +-- +-- >>> clauseListFromMinisatOutput "result" +-- [1,-2,3] +-- +clauseListFromMinisatOutput :: FilePath -> IO [Int] +clauseListFromMinisatOutput l = do + res <- fromMinisatOutput l + case res of + Just p -> return (snd p) + _ -> return [] diff --git a/SAT/Mios/Util/CNFIO/Reader.hs b/SAT/Mios/Util/CNFIO/Reader.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/CNFIO/Reader.hs @@ -0,0 +1,130 @@ +{-# LANGUAGE Safe #-} + +-- | Read a CNF file without haskell-platform +module SAT.Mios.Util.CNFIO.Reader + ( + -- * Interface + fromFile + , clauseListFromFile + ) + where +import Control.Applicative ((<$>), (<*>), (<*), (*>)) +import Data.Char +import Text.ParserCombinators.ReadP + +-- parser +{-# INLINE newline #-} +newline = char '\n' + +{-# INLINE digit #-} +digit = satisfy isDigit + +{-# INLINE spaces #-} +spaces = munch (`elem` " \t") + +{-# INLINE noneOf #-} +noneOf s = satisfy (`notElem` s) + +-- |parse a non-signed integer +{-# INLINE pint #-} +pint = do + n <- munch isDigit + return (read n :: Int) + +{-# INLINE mint #-} +mint = do + char '-' + n <- munch isDigit + return (- (read n::Int)) + +-- |parse a (signed) integer +{-# INLINE int #-} +int = mint <++ pint + +-- |Parse something like: p FORMAT VARIABLES CLAUSES +{-# INLINE problemLine #-} +problemLine = do + char 'p' + skipSpaces + (string "cnf" <++ string "CNF") + skipSpaces + vars <- pint + skipSpaces + clas <- pint + spaces + newline + return (vars, clas) + +-- |Parse something like: c This in an example of a comment line. +{-# INLINE commentLines #-} +commentLines = do + l <- look + if (head l) == 'c' + then do + munch ('\n' /=) + newline + commentLines + else return () + +_commentLines = do + char 'c' + munch ('\n' /=) + newline + l <- look + if (head l) == 'c' then commentLines else return () + +-- |Parse the preamble part +{-# INLINE preambleCNF #-} +preambleCNF = do + commentLines + problemLine + +-- |return integer list that terminates at zero +{-# INLINE seqNums #-} +seqNums = do + skipSpaces + x <- int + skipSpaces + if (x == 0) then return [] else (x :) <$> seqNums + +-- |Parse something like: 1 -2 0 4 0 -3 0 +{-# INLINE parseClauses #-} +parseClauses :: Int -> ReadP [[Int]] +parseClauses n = count n seqNums + +-- |top level interface for parsing CNF +{-# INLINE parseCNF #-} +parseCNF :: ReadP ((Int, Int), [[Int]]) +parseCNF = do + a <- preambleCNF + b <- parseClauses (snd a) + return (a, b) + +-- |driver:: String -> Either ParseError Int +driver input = readP_to_S (parseClauses 1) input + +-- |read a CNF file and return: +-- ((numbefOfVariables, numberOfClauses), [Literal]) +-- +-- >>> fromFile "acnf" +-- ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]] +-- +{-# INLINE fromFile #-} +fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]])) +fromFile f = do + c <- readFile f + case readP_to_S parseCNF c of + [(a, _)] -> return $ Just a + _ -> return Nothing + +-- | return clauses as [[Int]] from 'file' +-- +-- >>> clauseListFromFile "a.cnf" +-- [[1, 2], [-2, 3], [-1, 2, -3], [3]] +-- +clauseListFromFile :: FilePath -> IO [[Int]] +clauseListFromFile l = do + res <- fromFile l + case res of + Just (_, l) -> return l + _ -> return [] diff --git a/SAT/Mios/Util/CNFIO/Writer.hs b/SAT/Mios/Util/CNFIO/Writer.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/CNFIO/Writer.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE Safe #-} + +-- | Write SAT data to CNF file +module SAT.Mios.Util.CNFIO.Writer + ( + -- * Interface + toFile + , toCNFString + , toString + , toLatexString + ) + where +import Data.List (intercalate, nub, sort) +import System.IO + +-- | Write the CNF to file 'f', using 'toCNFString' +toFile :: FilePath -> [[Int]] -> IO () +toFile f l = writeFile f $ toCNFString l + +-- | Convert [Clause] to String, where Clause is [Int] +-- +-- >>> toCNFString [] +-- "p cnf 0 0\n" +-- +-- >>> toCNFString [[-1, 2], [-3, -4]] +-- "p cnf 4 2\n-1 2 0\n-3 -4 0\n" +-- +-- >>> toCNFString [[1], [-2], [-3, -4], [1,2,3,4]] +-- "p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n" +-- +toCNFString :: [[Int]] -> String +toCNFString l = hdr ++ str + where + hdr = "p cnf " ++ show numV ++ " " ++ show numC ++ "\n" + numC = length l + numV = last $ nub $ sort $ map abs $ concat l + str = concat [intercalate " " (map show c) ++ " 0\n" | c <- l] + +-- | converts @[[Int]]@ to a String +toString :: [[Int]] -> String -> String -> String +toString l and' or' = intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] + where + lit x + | 0 <= x = "X" ++ show x + | otherwise = "-X" ++ show (abs x) + a = pad and' + o = pad or' + pad s = " " ++ s ++ " " + +-- | converts @[[Int]]@ to a LaTeX expression +toLatexString :: [[Int]] -> String +toLatexString l = "\\begin{eqnarray*}\n" ++ intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] ++ "\n\\end{eqnarray*}" + where + lit x + | 0 <= x = "X_{" ++ show x ++ "}" + | otherwise = "\\overline{X_{" ++ show (abs x) ++ "}}" + a = " \n\\wedge " + o = " \\vee " diff --git a/SAT/Mios/Validator.hs b/SAT/Mios/Validator.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Validator.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE + ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +-- | validate an assignment +module SAT.Mios.Validator + ( + validate + ) + where + +import Data.Foldable (toList) +import SAT.Mios.Types +import SAT.Mios.Clause +import SAT.Mios.ClauseManager +import SAT.Mios.Solver + +-- | validates the assignment even if the implementation of 'Solver' is wrong; we re-implement some functions here. +validate :: Traversable t => Solver -> t Int -> IO Bool +validate s (toList -> map int2lit -> lst) = do + assignment <- newVec $ 1 + nVars s + vec <- getClauseVector (clauses s) + nc <- numberOfClauses (clauses s) + let + inject :: Lit -> IO () + inject l = setNth assignment (lit2var l) $ if positiveLit l then lTrue else lFalse + -- returns True if the literal is satisfied under the assignment + satisfied :: Lit -> IO Bool + satisfied l + | positiveLit l = (lTrue ==) <$> getNth assignment (lit2var l) + | otherwise = (lFalse ==) <$> getNth assignment (lit2var l) + -- returns True is any literal in the given list + satAny :: [Lit] -> IO Bool + satAny [] = return False + satAny (l:ls) = do + sat' <- satisfied l + if sat' then return True else satAny ls + -- traverses all clauses in 'clauses' + loopOnVector :: Int -> IO Bool + loopOnVector ((< nc) -> False) = return True + loopOnVector i = do + c <- getNthClause vec i + sat' <- satAny =<< asList c + if sat' then loopOnVector (i + 1) else return False + if null lst + then error "validator got an empty assignment." + else mapM_ inject lst >> loopOnVector 0 diff --git a/SAT/Solver/Mios.hs b/SAT/Solver/Mios.hs deleted file mode 100644 --- a/SAT/Solver/Mios.hs +++ /dev/null @@ -1,298 +0,0 @@ --- | Minisat-based Implementation and Optimization Study on SAT solver -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios - ( - -- * Interface to the core of solver - versionId - , CNFDescription (..) - , module SAT.Solver.Mios.OptionParser - , runSolver - , solveSAT - , solveSATWithConfiguration - , solve - , getModel - -- * Assignment Validator - , validateAssignment - , validate - -- * For standalone programs - , executeSolverOn - , executeSolver - , executeValidatorOn - , executeValidator - -- * File IO - , dumpAssigmentAsCNF - ) - where - -import Control.Monad ((<=<), unless, void, when) -import Data.Char -import qualified Data.ByteString.Char8 as B -import Data.List -import qualified Data.Vector.Unboxed as U -import Numeric (showFFloat) -import System.CPUTime -import System.Exit -import System.IO - -import SAT.Solver.Mios.Types -import SAT.Solver.Mios.Internal -import SAT.Solver.Mios.Solver -import SAT.Solver.Mios.M114 -import SAT.Solver.Mios.OptionParser -import SAT.Solver.Mios.Validator - -reportElapsedTime :: Bool -> String -> Integer -> IO Integer -reportElapsedTime False _ _ = return 0 -reportElapsedTime _ _ 0 = getCPUTime -reportElapsedTime _ mes t = do - now <- getCPUTime - let toSecond = 1000000000000 :: Double - hPutStr stderr mes - hPutStrLn stderr $ showFFloat (Just 3) ((fromIntegral (now - t)) / toSecond) " sec" - return now - --- | executes a solver on the given CNF file --- This is the simplest entry to standalone programs; not for Haskell programs -executeSolverOn :: FilePath -> IO () -executeSolverOn path = executeSolver (miosDefaultOption { _targetFile = Just path }) - --- | executes a solver on the given 'arg :: MiosConfiguration' --- | This is another entry point for standalone programs. -executeSolver :: MiosProgramOption -> IO () -executeSolver opts@(_targetFile -> target@(Just cnfFile)) = do - t0 <- reportElapsedTime (_confTimeProbe opts) "" 0 - (desc, cls) <- parseHeader target <$> B.readFile cnfFile - when (_numberOfVariables desc == 0) $ error $ "couldn't load " ++ show cnfFile - s <- newSolver (toMiosConf opts) desc - parseClauses s desc cls - t1 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Parse: ") t0 - when (_confVerbose opts) $ do - nc <- nClauses s - hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (nVars s, _numberOfVariables desc) ++ " #c = " ++ show (nc, _numberOfClauses desc) - res <- simplifyDB s - -- when (_confVerbose opts) $ hPutStrLn stderr $ "`simplifyDB`: " ++ show res - result <- solve s [] - case result of - True | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "SATISFIABLE" - False | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "UNSATISFIABLE" - True -> print =<< getModel s - False -> do -- contradiction - -- FIXMEin future - when (_confVerbose opts) $ hPutStrLn stderr "UNSAT" - -- print =<< map lit2int <$> asList (conflict s) - putStrLn "[]" - case _outputFile opts of - Just fname -> dumpAssigmentAsCNF fname result =<< getModel s - Nothing -> return () - t2 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Solve: ") t1 - when (result && _confCheckAnswer opts) $ do - asg <- getModel s - s' <- newSolver (toMiosConf opts) desc - parseClauses s' desc cls - good <- validate s' asg - if _confVerbose opts - then hPutStrLn stderr $ if good then "A vaild answer" else "Internal error: mios returns a wrong answer" - else unless good $ hPutStrLn stderr "Internal error: mios returns a wrong answer" - void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Validate: ") t2 - void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0 - when (_confStatProbe opts) $ do - hPutStr stderr $ "## [" ++ showPath cnfFile ++ "] " - hPutStrLn stderr . intercalate ", " . map (\(k, v) -> show k ++ ": " ++ show v) =<< getStats s - -executeSolver _ = return () - --- | new top-level interface that returns --- --- * conflicting literal set :: Left [Int] --- * satisfiable assignment :: Right [Int] --- -runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int]) -runSolver m d c = do - s <- newSolver m d - mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) c - noConf <- simplifyDB s - if noConf - then do - x <- solve s [] - if x - then Right <$> getModel s - else Left . map lit2int <$> asList (conflict s) - else return $ Left [] - - --- | the easiest interface for Haskell programs --- This returns the result @::[[Int]]@ for a given @(CNFDescription, [[Int]])@ --- The first argument @target@ can be build by @Just target <- cnfFromFile targetfile@. --- The second part of the first argument is a list of vector, which 0th element is the number of its real elements -solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int] -solveSAT = solveSATWithConfiguration defaultConfiguration - --- | solves the problem (2rd arg) under the configuration (1st arg) --- and returns an assignment as list of literals :: Int -solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int] -solveSATWithConfiguration conf desc cls = do - s <- newSolver conf desc - -- mapM_ (const (newVar s)) [0 .. _numberOfVariables desc - 1] - mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) cls - noConf <- simplifyDB s - if noConf - then do - result <- solve s [] - if result - then getModel s - else return [] - else return [] - --- | validates a given assignment from STDIN for the CNF file (2nd arg) --- this is the entry point for standalone programs -executeValidatorOn :: FilePath -> IO () -executeValidatorOn path = executeValidator (miosDefaultOption { _targetFile = Just path }) - --- | validates a given assignment for the problem (2nd arg) --- this is another entry point for standalone programs; see app/mios.hs -executeValidator :: MiosProgramOption -> IO () -executeValidator opts@(_targetFile -> target@(Just cnfFile)) = do - (desc, cls) <- parseHeader target <$> B.readFile cnfFile - when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ show cnfFile - s <- newSolver (toMiosConf opts) desc - parseClauses s desc cls - when (_confVerbose opts) $ - hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (_numberOfVariables desc) ++ " #c = " ++ show (_numberOfClauses desc) - when (_confVerbose opts) $ do - nc <- nClauses s - nl <- nLearnts s - hPutStrLn stderr $ "(nv, nc, nl) = " ++ show (nVars s, nc, nl) - asg <- read <$> getContents - unless (_confNoAnswer opts) $ print asg - result <- s `validate` (asg :: [Int]) - if result - then putStrLn ("It's a valid assignment for " ++ cnfFile ++ ".") >> exitSuccess - else putStrLn ("It's an invalid assignment for " ++ cnfFile ++ ".") >> exitFailure - -executeValidator _ = return () - --- | returns True if a given assignment (2nd arg) satisfies the problem (1st arg) --- if you want to check the @answer@ which a @slover@ returned, run @solver `validate` answer@, --- where 'validate' @ :: Traversable t => Solver -> t Lit -> IO Bool@ -validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool -validateAssignment desc cls asg = do - s <- newSolver defaultConfiguration desc - mapM_ ((s `addClause`) <=< (newSizedVecIntFromList . map int2lit)) cls - s `validate` asg - --- | dumps an assigment to file. --- 2nd arg is --- --- * @True@ if the assigment is satisfiable assigment --- --- * @False@ if not --- --- >>> do y <- solve s ... ; dumpAssigmentAsCNF "result.cnf" y <$> model s --- -dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO () -dumpAssigmentAsCNF fname False _ = do - withFile fname WriteMode $ \h -> do - hPutStrLn h "UNSAT" - -dumpAssigmentAsCNF fname True l = do - withFile fname WriteMode $ \h -> do - hPutStrLn h "SAT" - hPutStrLn h . unwords $ map show l - --------------------------------------------------------------------------------- --- DIMACS CNF Reader --------------------------------------------------------------------------------- - -parseHeader :: Maybe FilePath -> B.ByteString -> (CNFDescription, B.ByteString) -parseHeader target bs = if B.head bs == 'p' then (parseP l, B.tail bs') else parseHeader target (B.tail bs') - where - (l, bs') = B.span ('\n' /=) bs - -- format: p cnf n m, length "p cnf" == 5 - parseP line = case B.readInt $ B.dropWhile (`elem` " \t") (B.drop 5 line) of - Just (x, second) -> case B.readInt (B.dropWhile (`elem` " \t") second) of - Just (y, _) -> CNFDescription x y target - _ -> CNFDescription 0 0 target - _ -> CNFDescription 0 0 target - -parseClauses :: Solver -> CNFDescription -> B.ByteString -> IO () -parseClauses s (CNFDescription nv nc _) bs = do - let maxLit = int2lit $ negate nv - buffer <- newVec $ maxLit + 1 - polvec <- newVecBool (maxLit + 1) False - let - loop :: Int -> B.ByteString -> IO () - loop ((< nc) -> False) _ = return () - loop i b = loop (i + 1) =<< readClause s buffer polvec b - loop 0 bs - -- static polarity - let - asg = assigns s - checkPolarity :: Int -> IO () - checkPolarity ((< nv) -> False) = return () - checkPolarity v = do - p <- getNthBool polvec $ var2lit v True - n <- getNthBool polvec $ var2lit v False - when (p == False || n == False) $ setNth asg v $ if p then lTrue else lFalse - checkPolarity $ v + 1 - checkPolarity 1 - -skipWhitespace :: B.ByteString -> B.ByteString -skipWhitespace s - | elem c " \t\n" = skipWhitespace $ B.tail s - | otherwise = s - where - c = B.head s - --- | skip comment lines --- __Pre-condition:__ we are on the benngining of a line -skipComments :: B.ByteString -> B.ByteString -skipComments s - | c == 'c' = skipComments . B.tail . B.dropWhile (/= '\n') $ s - | otherwise = s - where - c = B.head s - -parseInt :: B.ByteString -> (Int, B.ByteString) -parseInt st = do - let - zero = ord '0' - loop :: B.ByteString -> Int -> (Int, B.ByteString) - loop s val = case B.head s of - c | '0' <= c && c <= '9' -> loop (B.tail s) (val * 10 + ord c - zero) - _ -> (val, B.tail s) - case B.head st of - '-' -> let (k, x) = loop (B.tail st) 0 in (negate k, x) - '+' -> loop st (0 :: Int) - c | '0' <= c && c <= '9' -> loop st 0 - _ -> error "PARSE ERROR! Unexpected char" - -readClause :: Solver -> Vec -> VecBool -> B.ByteString -> IO B.ByteString -readClause s buffer pvec stream = do - let - loop :: Int -> B.ByteString -> IO B.ByteString - loop i b = do - let (k, b') = parseInt $ skipWhitespace b - if k == 0 - then do - -- putStrLn . ("clause: " ++) . show . map lit2int =<< asList stack - setNth buffer 0 $ i - 1 - addClause s buffer - return b' - else do - let l = int2lit k - setNth buffer i l - setNthBool pvec l True - loop (i + 1) b' - loop 1 . skipComments . skipWhitespace $ stream - - -showPath :: FilePath -> String -showPath str - | elem '/' str = take (len - length basename) (repeat ' ') ++ basename - | otherwise = take (len - length basename') (repeat ' ') ++ basename' - where - len = 50 - basename = reverse . takeWhile (/= '/') . reverse $ str - basename' = take len str diff --git a/SAT/Solver/Mios/Clause.hs b/SAT/Solver/Mios/Clause.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Clause.hs +++ /dev/null @@ -1,144 +0,0 @@ --- | Clause, a data supporting pointer-based equality -{-# LANGUAGE - BangPatterns - , FlexibleInstances - , MagicHash - , MultiParamTypeClasses - , RecordWildCards - , ViewPatterns - #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios.Clause - ( - Clause (..) --- , isLit --- , getLit - , shrinkClause - , newClauseFromVec - , sizeOfClause - -- * Vector of Clause - , ClauseVector - , newClauseVector - , getNthClause - , setNthClause - , swapClauses - ) - where - -import Control.Monad (forM_) -import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#) -import qualified Data.Vector as V -import qualified Data.Vector.Mutable as MV -import qualified Data.Vector.Unboxed.Mutable as UV -import Data.List (intercalate) -import SAT.Solver.Mios.Types - --- | __Fig. 7.(p.11)__ --- clause, null, binary clause. --- This matches both of @Clause@ and @GClause@ in MiniSat --- TODO: GADTs is better? -data Clause = Clause - { - learnt :: !Bool -- ^ whether this is a learnt clause - , activity :: !DoubleSingleton -- ^ activity of this clause - , protected :: !BoolSingleton -- ^ protected from reduce - , lbd :: !IntSingleton -- ^ storing the LBD; values are computed in Solver - , lits :: !Vec -- ^ which this clause consists of - } --- | BinaryClause Lit -- binary clause consists of only a propagating literal - | NullClause -- as null pointer - --- | The equality on 'Clause' is defined with 'reallyUnsafePtrEquality'. -instance Eq Clause where - {-# SPECIALIZE INLINE (==) :: Clause -> Clause -> Bool #-} - (==) x y = x `seq` y `seq` tagToEnum# (reallyUnsafePtrEquality# x y) - -instance Show Clause where - show NullClause = "NullClause" - show _ = "a clause" - --- | supports a restricted set of 'VectorFamily' methods -instance VectorFamily Clause Lit where - dump mes NullClause = return $ mes ++ "Null" - dump mes Clause{..} = do - a <- show <$> getDouble activity - (len:ls) <- asList lits - return $ mes ++ "C" ++ show len ++ "{" ++ intercalate "," [show learnt, a, show . map lit2int . take len $ ls] ++ "}" - {-# SPECIALIZE INLINE asVec :: Clause -> Vec #-} - asVec Clause{..} = UV.unsafeTail lits - {-# SPECIALIZE INLINE asList :: Clause -> IO [Int] #-} - asList NullClause = return [] - asList Clause{..} = do - (n : ls) <- asList lits - return $ take n ls - --- returns True if it is a 'BinaryClause' --- FIXME: this might be discarded in minisat 2.2 --- isLit :: Clause -> Bool --- isLit (BinaryClause _) = True --- isLit _ = False - --- returns the literal in a BinaryClause --- FIXME: this might be discarded in minisat 2.2 --- getLit :: Clause -> Lit --- getLit (BinaryClause x) = x - --- coverts a binary clause to normal clause in order to reuse map-on-literals-in-a-clause codes --- liftToClause :: Clause -> Clause --- liftToClause (BinaryClause _) = error "So far I use generic function approach instead of lifting" - --- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals -{-# INLINABLE shrinkClause #-} -shrinkClause :: Int -> Clause -> IO () -shrinkClause !n Clause{..} = setNth lits 0 . subtract n =<< getNth lits 0 - --- | copies /vec/ and return a new 'Clause' --- Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically. -{-# INLINE newClauseFromVec #-} -newClauseFromVec :: Bool -> Vec -> IO Clause -newClauseFromVec l vec = do - n <- getNth vec 0 - v <- newVec $ n + 1 - forM_ [0 .. n] $ \i -> setNth v i =<< getNth vec i - Clause l <$> newDouble 0 <*> newBool False <*> newInt n <*> return v - --- | returns the number of literals in a clause, even if the given clause is a binary clause -{-# INLINE sizeOfClause #-} -sizeOfClause :: Clause -> IO Int --- sizeOfClause (BinaryClause _) = return 1 -sizeOfClause !c = getNth (lits c) 0 - --------------------------------------------------------------------------------- - --- | Mutable 'Clause' Vector -type ClauseVector = MV.IOVector Clause - -instance VectorFamily ClauseVector Clause where - asList cv = V.toList <$> V.freeze cv - dump mes cv = do - l <- asList cv - sts <- mapM (dump ",") (l :: [Clause]) - return $ mes ++ tail (concat sts) - --- | returns a new 'ClauseVector' -newClauseVector :: Int -> IO ClauseVector -newClauseVector n = do - v <- MV.new (max 4 n) - MV.set v NullClause - return v - --- | returns the nth 'Clause' -{-# INLINE getNthClause #-} -getNthClause :: ClauseVector -> Int -> IO Clause -getNthClause = MV.unsafeRead - --- | sets the nth 'Clause' -{-# INLINE setNthClause #-} -setNthClause :: ClauseVector -> Int -> Clause -> IO () -setNthClause = MV.unsafeWrite - --- | swaps the two 'Clause's -{-# INLINE swapClauses #-} -swapClauses :: ClauseVector -> Int -> Int -> IO () -swapClauses = MV.unsafeSwap diff --git a/SAT/Solver/Mios/ClauseManager.hs b/SAT/Solver/Mios/ClauseManager.hs deleted file mode 100644 --- a/SAT/Solver/Mios/ClauseManager.hs +++ /dev/null @@ -1,324 +0,0 @@ --- | A shrinkable 'VectorFamily' of 'C.Clause' -{-# LANGUAGE - BangPatterns - , DuplicateRecordFields - , FlexibleInstances - , MultiParamTypeClasses - , RecordWildCards - , ViewPatterns - #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios.ClauseManager - ( - -- * higher level interface for ClauseVector - ClauseManager (..) --- -- * vector of clauses --- , SimpleManager - -- * Manager with an extra Int (used as sort key or blocking literal) - , ClauseExtManager - , pushClauseWithKey - , getKeyVector - , markClause --- , purifyManager - -- * WatcherList - , WatcherList - , newWatcherList - , getNthWatcher - , garbageCollect --- , numberOfRegisteredClauses - ) - where - -import Control.Monad (forM, unless, when) -import qualified Data.IORef as IORef -import qualified Data.List as L -import qualified Data.Vector as V -import qualified Data.Vector.Mutable as MV -import SAT.Solver.Mios.Types -import qualified SAT.Solver.Mios.Clause as C - --- | resizable clause vector -class ClauseManager a where - newManager :: Int -> IO a - numberOfClauses :: a -> IO Int - clearManager :: a -> IO () - shrinkManager :: a -> Int -> IO () - getClauseVector :: a -> IO C.ClauseVector - pushClause :: a -> C.Clause -> IO () --- removeClause :: a -> C.Clause -> IO () --- removeNthClause :: a -> Int -> IO () - -{- --- | The Clause Container -data SimpleManager = SimpleManager - { - _nActives :: IntSingleton -- number of active clause - , _clauseVector :: IORef.IORef C.ClauseVector -- clause list - } - -instance ClauseManager SimpleManager where - {-# SPECIALIZE INLINE newManager :: Int -> IO SimpleManager #-} - newManager initialSize = do - i <- newInt 0 - v <- C.newClauseVector initialSize - SimpleManager i <$> IORef.newIORef v - {-# SPECIALIZE INLINE numberOfClauses :: SimpleManager -> IO Int #-} - numberOfClauses SimpleManager{..} = getInt _nActives - {-# SPECIALIZE INLINE clearManager :: SimpleManager -> IO () #-} - clearManager SimpleManager{..} = setInt _nActives 0 - {-# SPECIALIZE INLINE shrinkManager :: SimpleManager -> Int -> IO () #-} - shrinkManager SimpleManager{..} k = modifyInt _nActives (subtract k) - {-# SPECIALIZE INLINE getClauseVector :: SimpleManager -> IO C.ClauseVector #-} - getClauseVector SimpleManager{..} = IORef.readIORef _clauseVector - -- | O(1) inserter - {-# SPECIALIZE INLINE pushClause :: SimpleManager -> C.Clause -> IO () #-} - pushClause !SimpleManager{..} !c = do - !n <- getInt _nActives - !v <- IORef.readIORef _clauseVector - if MV.length v - 1 <= n - then do - v' <- MV.unsafeGrow v (max 8 (MV.length v)) - -- forM_ [n .. MV.length v' - 1] $ \i -> MV.unsafeWrite v' i C.NullClause - MV.unsafeWrite v' n c - IORef.writeIORef _clauseVector v' - else MV.unsafeWrite v n c - modifyInt _nActives (1 +) - -- | O(1) remove-and-compact function - {-# SPECIALIZE INLINE removeNthClause :: SimpleManager -> Int -> IO () #-} - removeNthClause SimpleManager{..} i = do - !n <- subtract 1 <$> getInt _nActives - !v <- IORef.readIORef _clauseVector - MV.unsafeWrite v i =<< MV.unsafeRead v n - setInt _nActives n - -- | O(n) but lightweight remove-and-compact function - -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it. - {-# SPECIALIZE INLINE removeClause :: SimpleManager -> C.Clause -> IO () #-} - removeClause SimpleManager{..} c = do - -- putStrLn =<< dump "@removeClause| remove " c - -- putStrLn =<< dump "@removeClause| from " m - !n <- subtract 1 <$> getInt _nActives - -- unless (0 <= n) $ error $ "removeClause catches " ++ show n - !v <- IORef.readIORef _clauseVector - let - seekIndex :: Int -> IO Int - seekIndex k = do - c' <- MV.unsafeRead v k - if c' == c then return k else seekIndex $ k + 1 - unless (n == -1) $ do - !i <- seekIndex 0 - MV.unsafeWrite v i =<< MV.unsafeRead v n - setInt _nActives n - -instance VectorFamily SimpleManager C.Clause where - dump mes SimpleManager{..} = do - n <- getInt _nActives - if n == 0 - then return $ mes ++ "empty clausemanager" - else do - l <- take n <$> (asList =<< IORef.readIORef _clauseVector) - sts <- mapM (dump ",") (l :: [C.Clause]) - return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts) --} - --------------------------------------------------------------------------------- - --- | Clause + Blocking Literal -data ClauseExtManager = ClauseExtManager - { - _nActives :: IntSingleton -- number of active clause - , _purged :: BoolSingleton -- whether it needs gc - , _clauseVector :: IORef.IORef C.ClauseVector -- clause list - , _keyVector :: IORef.IORef Vec -- Int list - } - -instance ClauseManager ClauseExtManager where - {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-} - newManager initialSize = do - i <- newInt 0 - v <- C.newClauseVector initialSize - b <- newVec (MV.length v) - ClauseExtManager i <$> newBool False <*> IORef.newIORef v <*> IORef.newIORef b - {-# SPECIALIZE INLINE numberOfClauses :: ClauseExtManager -> IO Int #-} - numberOfClauses ClauseExtManager{..} = getInt _nActives - {-# SPECIALIZE INLINE clearManager :: ClauseExtManager -> IO () #-} - clearManager ClauseExtManager{..} = setInt _nActives 0 - {-# SPECIALIZE INLINE shrinkManager :: ClauseExtManager -> Int -> IO () #-} - shrinkManager ClauseExtManager{..} k = modifyInt _nActives (subtract k) - {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-} - getClauseVector ClauseExtManager{..} = IORef.readIORef _clauseVector - -- | O(1) insertion function - {-# SPECIALIZE INLINE pushClause :: ClauseExtManager -> C.Clause -> IO () #-} - pushClause !ClauseExtManager{..} !c = do - -- checkConsistency m c - !n <- getInt _nActives - !v <- IORef.readIORef _clauseVector - !b <- IORef.readIORef _keyVector - if MV.length v - 1 <= n - then do - let len = max 8 $ MV.length v - v' <- MV.unsafeGrow v len - b' <- vecGrow b len - MV.unsafeWrite v' n c - setNth b' n 0 - IORef.writeIORef _clauseVector v' - IORef.writeIORef _keyVector b' - else MV.unsafeWrite v n c >> setNth b n 0 - modifyInt _nActives (1 +) -{- - -- | O(n) but lightweight remove-and-compact function - -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it. - {-# SPECIALIZE INLINE removeClause :: ClauseExtManager -> C.Clause -> IO () #-} - removeClause ClauseExtManager{..} c = do - !n <- subtract 1 <$> getInt _nActives - !v <- IORef.readIORef _clauseVector - !b <- IORef.readIORef _keyVector - let - seekIndex :: Int -> IO Int - seekIndex k = do - c' <- MV.unsafeRead v k - if c' == c then return k else seekIndex $ k + 1 - unless (n == -1) $ do - !i <- seekIndex 0 - MV.unsafeWrite v i =<< MV.unsafeRead v n - setNth b i =<< getNth b n - setInt _nActives n - removeNthClause = error "removeNthClause is not implemented on ClauseExtManager" --} - --- | sets the expire flag to a clause -{-# INLINE markClause #-} -markClause :: ClauseExtManager -> C.Clause -> IO () -markClause ClauseExtManager{..} c = do - !n <- getInt _nActives - !v <- IORef.readIORef _clauseVector - let - seekIndex :: Int -> IO () - seekIndex k = do - c' <- MV.unsafeRead v k - if c' == c then MV.unsafeWrite v k C.NullClause else seekIndex $ k + 1 - unless (n == 0) $ do - seekIndex 0 - setBool _purged True - -{-# INLINE purifyManager #-} -purifyManager :: ClauseExtManager -> IO () -purifyManager ClauseExtManager{..} = do - diry <- getBool _purged - when diry $ do - n <- getInt _nActives - vec <- IORef.readIORef _clauseVector - keys <- IORef.readIORef _keyVector - let - loop :: Int -> Int -> IO Int - loop ((< n) -> False) n' = return n' - loop i j = do - c <- C.getNthClause vec i - if c /= C.NullClause - then do - unless (i == j) $ do - C.setNthClause vec j c - setNth keys j =<< getNth keys i - loop (i + 1) (j + 1) - else loop (i + 1) j - setInt _nActives =<< loop 0 0 - setBool _purged False - --- | returns the associated Int vector -{-# INLINE getKeyVector #-} -getKeyVector :: ClauseExtManager -> IO Vec -getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector - --- | O(1) inserter -{-# INLINE pushClauseWithKey #-} -pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO () -pushClauseWithKey !ClauseExtManager{..} !c k = do - -- checkConsistency m c - !n <- getInt _nActives - !v <- IORef.readIORef _clauseVector - !b <- IORef.readIORef _keyVector - if MV.length v - 1 <= n - then do - let len = max 8 $ MV.length v - v' <- MV.unsafeGrow v len - b' <- vecGrow b len - MV.unsafeWrite v' n c - setNth b' n k - IORef.writeIORef _clauseVector v' - IORef.writeIORef _keyVector b' - else MV.unsafeWrite v n c >> setNth b n k - modifyInt _nActives (1 +) - -instance VectorFamily ClauseExtManager C.Clause where - dump mes ClauseExtManager{..} = do - n <- getInt _nActives - if n == 0 - then return $ mes ++ "empty ClauseExtManager" - else do - l <- take n <$> (asList =<< IORef.readIORef _clauseVector) - sts <- mapM (dump ",") (l :: [C.Clause]) - return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts) - --------------------------------------------------------------------------------- WatcherList - --- | Vector of 'ClauseExtManager' -type WatcherList = V.Vector ClauseExtManager - --- | /n/ is the number of 'Var', /m/ is default size of each watcher list --- | For /n/ vars, we need [0 .. 2 + 2 * n - 1] slots, namely /2 * (n + 1)/-length vector -newWatcherList :: Int -> Int -> IO WatcherList -newWatcherList n m = V.fromList <$> forM [0 .. int2lit (negate n) + 1] (\_ -> newManager m) - --- | returns the watcher List :: "ClauseManager" for "Literal" /l/ -{-# INLINE getNthWatcher #-} -getNthWatcher :: WatcherList -> Lit-> ClauseExtManager -getNthWatcher = V.unsafeIndex - -instance VectorFamily WatcherList C.Clause where - dump mes wl = (mes ++) . L.concat <$> forM [1 .. V.length wl - 1] (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i)) - --- | purges all expirable clauses in 'WatcherList' -{-# INLINE garbageCollect #-} -garbageCollect :: WatcherList -> IO () -garbageCollect wm = V.mapM_ purifyManager wm - -numberOfRegisteredClauses :: WatcherList -> IO Int -numberOfRegisteredClauses ws = sum <$> V.mapM numberOfClauses ws - -{- --------------------------------------------------------------------------------- debugging stuff - -checkConsistency :: ClauseManager a => a -> C.Clause -> IO () -checkConsistency manager c = do - nc <- numberOfClauses manager - vec <- getClauseVector manager - let - loop :: Int -> IO () - loop i = do - when (i < nc) $ do - c' <- MV.unsafeRead vec i - when (c' == c) $ error "insert a clause to a ClauseMananger twice" - loop $ i + 1 - loop 0 - -checkClauseOrder :: ClauseManager a => a -> IO () -checkClauseOrder manager = do - putStr "checking..." - nc <- numberOfClauses manager - vec <- getClauseVector manager - let - nthActivity :: Int -> IO Double - nthActivity i = getDouble . C.activity =<< MV.unsafeRead vec i - report :: Int -> Int -> IO () - report i j = (putStr . (++ ", ") . show =<< nthActivity i) >> when (i < j) (report (i + 1) j) - loop :: Int -> Double -> IO () - loop i v = do - when (i < nc) $ do - c <- MV.unsafeRead vec i - a <- getDouble (C.activity c) - when (c == C.NullClause) $ error "null is included" - when (v < a) $ report 0 i >> error ("unsorted clause vector: " ++ show (nc, i)) - loop (i + 1) a - loop 0 =<< nthActivity 0 - putStrLn "done" --} diff --git a/SAT/Solver/Mios/Data/Singleton.hs b/SAT/Solver/Mios/Data/Singleton.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Data/Singleton.hs +++ /dev/null @@ -1,196 +0,0 @@ --- | A fast(est) mutable data -{-# LANGUAGE - BangPatterns - #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios.Data.Singleton - ( - -- * Bool - BoolSingleton - , newBool - , getBool - , setBool - , modifyBool - -- * Int - , IntSingleton - , newInt - , getInt - , setInt - , modifyInt - -- * Double - , DoubleSingleton - , newDouble - , getDouble - , setDouble - , modifyDouble - ) - where -{- ----------------------------------------- --- Implementation 1. :: IORef ----------------------------------------- - -import Data.IORef - -type BoolSingleton = IORef Bool - -newBool :: Bool -> IO BoolSingleton -newBool = newIORef - -{-# INLINE getBool #-} -getBool :: BoolSingleton -> IO Bool -getBool = readIORef - -{-# INLINE setBool #-} -setBool :: BoolSingleton -> Bool -> IO () -setBool = writeIORef - -{-# INLINE modifyBool #-} -modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO () -modifyBool = modifyIORef' - -type IntSingleton = IORef Int - -newInt :: Int -> IO IntSingleton -newInt = newIORef - -{-# INLINE getInt #-} -getInt :: IntSingleton -> IO Int -getInt = readIORef - -{-# INLINE setInt #-} -setInt :: IntSingleton -> Int -> IO () -setInt = writeIORef - -{-# INLINE modifyInt #-} -modifyInt :: IntSingleton -> (Int -> Int) -> IO () -modifyInt = modifyIORef' - -type DoubleSingleton = IORef Double - -newDouble :: Double -> IO DoubleSingleton -newDouble = newIORef - -{-# INLINE getDouble #-} -getDouble :: DoubleSingleton -> IO Double -getDouble = readIORef - -{-# INLINE setDouble #-} -setDouble :: DoubleSingleton -> Double -> IO () -setDouble = writeIORef - -{-# INLINE modifyDouble #-} -modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO () -modifyDouble = modifyIORef' --} -{- ----------------------------------------- --- Implementation 2. :: Data.Mutable.IOURef ----------------------------------------- - -import qualified Data.Mutable as M - -newtype IntSingleton = IntSingleton - { - mutableInt :: M.IOURef Int - } - -newInt :: IO IntSingleton -newInt = IntSingleton <$> M.newRef 0 - -{-# INLINE getInt #-} -getInt :: IntSingleton -> IO Int -getInt !(IntSingleton val) = M.readRef val - -{-# INLINE setInt #-} -setInt :: IntSingleton -> Int -> IO () -setInt !(IntSingleton val) !x = M.writeRef val x - -{-# INLINE modifyInt #-} -modifyInt :: IntSingleton -> (Int -> Int) -> IO () -modifyInt !(IntSingleton val) !f = M.modifyRef' val f --} - --- {- ----------------------------------------- --- Implementation 3. :: Data.Vector.Unboxed.Mutable ----------------------------------------- - -import qualified Data.Vector.Unboxed.Mutable as UV - --- | mutable Int -type IntSingleton = UV.IOVector Int - --- | returns a new 'IntSingleton' -newInt :: Int -> IO IntSingleton -newInt k = do - s <- UV.new 1 - UV.unsafeWrite s 0 k - return s - --- | returns the value -{-# INLINE getInt #-} -getInt :: IntSingleton -> IO Int -getInt val = UV.unsafeRead val 0 - --- | sets the value -{-# INLINE setInt #-} -setInt :: IntSingleton -> Int -> IO () -setInt val !x = UV.unsafeWrite val 0 x - --- | modifies the value -{-# INLINE modifyInt #-} -modifyInt :: IntSingleton -> (Int -> Int) -> IO () -modifyInt val !f = UV.unsafeModify val f 0 - --- | mutable Bool -type BoolSingleton = UV.IOVector Bool - --- | returns a new 'BoolSingleton' -newBool :: Bool -> IO BoolSingleton -newBool b = do - s <- UV.new 1 - UV.unsafeWrite s 0 b - return s - --- | returns the value -{-# INLINE getBool #-} -getBool :: BoolSingleton -> IO Bool -getBool val = UV.unsafeRead val 0 - --- | sets the value -{-# INLINE setBool #-} -setBool :: BoolSingleton -> Bool -> IO () -setBool val !x = UV.unsafeWrite val 0 x - --- | modifies the value -{-# INLINE modifyBool #-} -modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO () -modifyBool val !f = UV.unsafeModify val f 0 - --- | mutable Double -type DoubleSingleton = UV.IOVector Double - --- | returns a new 'DoubleSingleton' -newDouble :: Double -> IO DoubleSingleton -newDouble d = do - s <- UV.new 1 - UV.unsafeWrite s 0 d - return s - --- | returns the value -{-# INLINE getDouble #-} -getDouble :: DoubleSingleton -> IO Double -getDouble val = UV.unsafeRead val 0 - --- | sets the value -{-# INLINE setDouble #-} -setDouble :: DoubleSingleton -> Double -> IO () -setDouble val !x = UV.unsafeWrite val 0 x - --- | modifies the value -{-# INLINE modifyDouble #-} -modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO () -modifyDouble val !f = UV.unsafeModify val f 0 --- -} diff --git a/SAT/Solver/Mios/Data/Stack.hs b/SAT/Solver/Mios/Data/Stack.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Data/Stack.hs +++ /dev/null @@ -1,93 +0,0 @@ --- | stack of Int, by adding the length field as the zero-th element to a 'Vec' -{-# LANGUAGE - BangPatterns - , FlexibleInstances - , MultiParamTypeClasses - #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios.Data.Stack - ( - Stack - , newStack - , clearStack - , sizeOfStack - , pushToStack - , popFromStack - , lastOfStack - , shrinkStack - , asSizedVec - , isoVec - ) - where - -import qualified Data.Vector.Unboxed.Mutable as UV -import SAT.Solver.Mios.Types - --- | Unboxed mutable stack for Int. -newtype Stack = Stack - { - ivec :: UV.IOVector Int - } - -instance VectorFamily Stack Int where - dump str v = (str ++) . show <$> asList v - {-# SPECIALIZE INLINE asVec :: Stack -> Vec #-} - asVec (Stack v) = UV.unsafeTail v - asList (Stack v) = do - (n : l) <- asList v - return $ take n l - --- | returns the number of elements -{-# INLINE sizeOfStack #-} -sizeOfStack :: Stack -> IO Int -sizeOfStack (Stack v) = UV.unsafeRead v 0 - --- | clear stack -{-# INLINE clearStack #-} -clearStack :: Stack -> IO () -clearStack (Stack v) = UV.unsafeWrite v 0 0 - --- | returns a new stack which size is @size@ -{-# INLINABLE newStack #-} -newStack :: Int -> IO Stack -newStack n = do - v <- UV.new $ n + 1 - UV.set v 0 - return $ Stack v - --- | pushs an int to 'Stack' -{-# INLINE pushToStack #-} -pushToStack :: Stack -> Int -> IO () -pushToStack (Stack v) !x = do - !i <- (+ 1) <$> UV.unsafeRead v 0 - UV.unsafeWrite v i x - UV.unsafeWrite v 0 i - --- | drops the first element from 'Stack' -{-# INLINE popFromStack #-} -popFromStack :: Stack -> IO () -popFromStack (Stack v) = UV.unsafeModify v (subtract 1) 0 - --- | peeks the last element in 'Stack' -{-# INLINE lastOfStack #-} -lastOfStack :: Stack -> IO Int -lastOfStack (Stack v) = UV.unsafeRead v =<< UV.unsafeRead v 0 - --- | Shrink the stack. The given arg means the number of discards. --- therefore, shrink s n == for [1 .. n] $ \_ -> pop s -{-# INLINE shrinkStack #-} -shrinkStack :: Stack -> Int -> IO () -shrinkStack (Stack v) k = UV.unsafeModify v (subtract k) 0 - --- | converts Stack to sized Vec; this is the method to get the internal vector -{-# INLINE asSizedVec #-} -asSizedVec :: Stack -> Vec -asSizedVec (Stack v) = v - --- | isomorphic conversion to 'Vec' --- --- Note: 'asVec' drops the 1st element and no copy (unsafe operation); 'isoVec' really copies the real elements -{-# INLINE isoVec #-} -isoVec :: Stack -> IO Vec -isoVec (Stack v) = UV.clone . flip UV.take v . (1 +) =<< UV.unsafeRead v 0 diff --git a/SAT/Solver/Mios/Data/Vec.hs b/SAT/Solver/Mios/Data/Vec.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Data/Vec.hs +++ /dev/null @@ -1,86 +0,0 @@ --- | The fundamental data structure: Fixed Mutable Unboxed Int Vector -{-# LANGUAGE - BangPatterns - #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios.Data.Vec - ( - Vec - , sizeOfVector - , getNth - , setNth - , swapBetween - , modifyNth - , setAll - , newVec - , newVecWith - , newSizedVecIntFromList - , newSizedVecIntFromUVector - , vecGrow - ) - where - -import qualified Data.Vector.Unboxed as U -import qualified Data.Vector.Unboxed.Mutable as UV - --- | Costs of all operations are /O/(/1/) -type Vec = UV.IOVector Int - --- | returns the size of 'Vec' -{-# INLINE sizeOfVector #-} -sizeOfVector :: Vec -> IO Int -sizeOfVector v = return $! UV.length v - --- | returns a new 'Vec' -{-# INLINE newVec #-} -newVec :: Int -> IO Vec -newVec = UV.new - --- | returns a new 'Vec' filled with an Int -{-# INLINE newVecWith #-} -newVecWith :: Int -> Int -> IO Vec -newVecWith n x = do - v <- UV.new n - UV.set v x - return v - --- | gets the nth value -{-# INLINE getNth #-} -getNth :: Vec -> Int -> IO Int -getNth = UV.unsafeRead - --- | sets the nth value -{-# INLINE setNth #-} -setNth :: Vec -> Int -> Int -> IO () -setNth = UV.unsafeWrite - --- | modify the nth value -{-# INLINE modifyNth #-} -modifyNth :: Vec -> (Int -> Int) -> Int -> IO () -modifyNth = UV.unsafeModify - --- | sets all elements -{-# INLINE setAll #-} -setAll :: Vec -> Int -> IO () -setAll = UV.set - --- | swaps two elements -{-# INLINE swapBetween #-} -swapBetween:: Vec -> Int -> Int -> IO () -swapBetween = UV.unsafeSwap - --- | returns a new 'Vec' from a @[Int]@ -{-# INLINE newSizedVecIntFromList #-} -newSizedVecIntFromList :: [Int] -> IO Vec -newSizedVecIntFromList !l = U.unsafeThaw $ U.fromList (length l : l) - --- | returns a new 'Vec' from a Unboxed Int Vector -{-# INLINE newSizedVecIntFromUVector #-} -newSizedVecIntFromUVector :: U.Vector Int -> IO Vec -newSizedVecIntFromUVector = U.unsafeThaw - --- | calls @unasfeGrow@ -{-# INLINE vecGrow #-} -vecGrow :: Vec -> Int -> IO Vec -vecGrow = UV.unsafeGrow diff --git a/SAT/Solver/Mios/Data/VecBool.hs b/SAT/Solver/Mios/Data/VecBool.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Data/VecBool.hs +++ /dev/null @@ -1,55 +0,0 @@ --- | Mutable Unboxed Boolean Vector --- --- * __VecBool@::UV.IOVector Bool@ -- data type that contains a mutable list of elements --- -{-# LANGUAGE - BangPatterns - , FlexibleInstances - , MultiParamTypeClasses - #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios.Data.VecBool - ( - VecBool - , newVecBool - , getNthBool - , setNthBool - , modifyNthBool - ) - where - -import Control.Monad (forM) -import qualified Data.Vector.Unboxed.Mutable as UV -import SAT.Solver.Mios.Types (VectorFamily(..)) - --- | Mutable unboxed Bool Vector -type VecBool = UV.IOVector Bool - --- | provides 'clear' and 'size' -instance VectorFamily VecBool Bool where - clear _ = error "VecBool.clear" - asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v - dump str v = (str ++) . show <$> asList v - --- | returns a new 'VecBool' -newVecBool :: Int -> Bool -> IO VecBool -newVecBool n x = do - v <- UV.new n - UV.set v x - return v - --- | returns the nth value in 'VecBool' -{-# INLINE getNthBool #-} -getNthBool :: VecBool -> Int -> IO Bool -getNthBool = UV.unsafeRead - --- | sets the nth value -{-# INLINE setNthBool #-} -setNthBool :: VecBool -> Int -> Bool -> IO () -setNthBool = UV.unsafeWrite - --- | sets the nth value -{-# INLINE modifyNthBool #-} -modifyNthBool :: VecBool -> (Bool -> Bool) -> Int -> IO () -modifyNthBool = UV.unsafeModify diff --git a/SAT/Solver/Mios/Data/VecDouble.hs b/SAT/Solver/Mios/Data/VecDouble.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Data/VecDouble.hs +++ /dev/null @@ -1,53 +0,0 @@ --- | Mutable Unboxed Double Vector -{-# LANGUAGE - BangPatterns - , FlexibleInstances - , MultiParamTypeClasses - #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios.Data.VecDouble - ( - VecDouble - , newVecDouble - , getNthDouble - , setNthDouble - , modifyNthDouble - ) - where - -import Control.Monad (forM) -import Data.List () -import qualified Data.Vector.Unboxed.Mutable as UV -import SAT.Solver.Mios.Types (VectorFamily(..)) - --- | Mutable unboxed Double Vector -type VecDouble = UV.IOVector Double - -instance VectorFamily VecDouble Double where - clear _ = error "VecDouble.clear" - asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v - dump str v = (str ++) . show <$> asList v - --- | returns a new 'VecDouble' -newVecDouble :: Int -> Double -> IO VecDouble -newVecDouble n 0 = UV.new n -newVecDouble n x = do - v <- UV.new n - UV.set v x - return v - --- | returns the nth value in 'VecDouble' -{-# INLINE getNthDouble #-} -getNthDouble :: Int -> VecDouble -> IO Double -getNthDouble !n v = UV.unsafeRead v n - --- | sets the nth value -{-# INLINE setNthDouble #-} -setNthDouble :: Int -> VecDouble -> Double -> IO () -setNthDouble !n v !x = UV.unsafeWrite v n x - --- | updates the nth value -{-# INLINE modifyNthDouble #-} -modifyNthDouble :: Int -> VecDouble -> (Double -> Double) -> IO () -modifyNthDouble !n v !f = UV.unsafeModify v f n diff --git a/SAT/Solver/Mios/Glucose.hs b/SAT/Solver/Mios/Glucose.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Glucose.hs +++ /dev/null @@ -1,72 +0,0 @@ --- | This is a part of MIOS -{-# LANGUAGE - BangPatterns - , RecordWildCards - , ScopedTypeVariables - , ViewPatterns - #-} -{-# LANGUAGE Safe #-} - -module SAT.Solver.Mios.Glucose - ( - computeLBD - , lbdOf - , setLBD - , updateLBD - , nextReduction - ) - where - -import Control.Monad (when) -import SAT.Solver.Mios.Types -import SAT.Solver.Mios.Clause -import SAT.Solver.Mios.Solver - --- | returns the LBD vaule for 'Vec[1 ..]' -computeLBD :: Solver -> Vec -> IO Int -computeLBD Solver{..} vec = do - key <- (1 +) <$> getInt lbd'key - setInt lbd'key key - nv <- getNth vec 0 - let - loop :: Int -> Int -> IO Int - loop ((<= nv) -> False) n = return n - loop !i !n = do - l <- getNth level . lit2var =<< getNth vec i - seen <- if l == 0 then return True else (key ==) <$> getNth lbd'seen l - if seen - then loop (i + 1) n - else setNth lbd'seen l key >> loop (i + 1) (n + 1) - loop 1 0 - --- | returns the LBD value of 'Clause' -{-# INLINE lbdOf #-} -lbdOf :: Solver -> Clause -> IO Int -lbdOf s (lits -> v) = computeLBD s v - --- | update the LBD field in 'Clause' -{-# INLINE setLBD #-} -setLBD :: Solver -> Clause -> IO () -setLBD s c = setInt (lbd c) =<< lbdOf s c - --- | update the lbd field of /c/ -{-# INLINE updateLBD #-} -updateLBD :: Solver -> Clause -> IO () -updateLBD _ NullClause = error "LBD71" -updateLBD _ (learnt -> False) = return () -updateLBD s c@Clause{..} = setInt lbd =<< lbdOf s c - --- | 0 based --- --- >>> nextReduction 0 --- 20000 --- >>> nextReduction 1 --- 40000 + 200 = 20000 + 20000 + 200 --- >>> nextReduction 2 --- 6000 + 600 = 20000 + 20200 + 20000 + 400 --- >>> nextReduction 3 --- 80000 + 1200 = 20000 + 20200 + 20400 + 20000 + 600 --- -nextReduction :: Int -> Int -> Int --- nextReduction _ n = 30000 + 10000 * n -nextReduction b n = b + 300 * n diff --git a/SAT/Solver/Mios/Internal.hs b/SAT/Solver/Mios/Internal.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Internal.hs +++ /dev/null @@ -1,34 +0,0 @@ --- | Internal Settings -module SAT.Solver.Mios.Internal - ( - versionId - , MiosConfiguration (..) - , defaultConfiguration - , module Plumbing - ) - where -import SAT.Solver.Mios.Data.VecBool as Plumbing -import SAT.Solver.Mios.Data.VecDouble as Plumbing -import SAT.Solver.Mios.Data.Stack as Plumbing - --- | version name -versionId :: String -versionId = "mios 1.2 " -- blocking literal + lbd + phase-saving - --- | solver's parameters; random decision rate was dropped. -data MiosConfiguration = MiosConfiguration - { - variableDecayRate :: Double -- ^ decay rate for variable activity - , clauseDecayRate :: Double -- ^ decay rate for clause activity - , collectStats :: Bool -- ^ whether collect and report statistics - } - --- | dafault configuration --- --- * Minisat-1.14 uses @(0.95, 0.999, 0.2 = 20 / 1000)@. --- * Minisat-2.20 uses @(0.95, 0.999, 0)@. --- * Gulcose-4.0 uses @(0.8 , 0.999, 0)@. --- * Mios-1.2 uses @(0.95, 0.999, 0)@. --- -defaultConfiguration :: MiosConfiguration -defaultConfiguration = MiosConfiguration 0.95 0.999 {- 0 -} False diff --git a/SAT/Solver/Mios/M114.hs b/SAT/Solver/Mios/M114.hs deleted file mode 100644 --- a/SAT/Solver/Mios/M114.hs +++ /dev/null @@ -1,816 +0,0 @@ --- | This is a part of MIOS -{-# LANGUAGE - BangPatterns - , RecordWildCards - , ScopedTypeVariables - , ViewPatterns - #-} -{-# LANGUAGE Safe #-} - -module SAT.Solver.Mios.M114 - ( - simplifyDB - , solve - ) - where - -import Control.Monad (forM_, unless, void, when) -import Data.Bits -import Data.Foldable (foldrM) -import SAT.Solver.Mios.Types -import SAT.Solver.Mios.Internal -import SAT.Solver.Mios.Clause -import SAT.Solver.Mios.ClauseManager -import SAT.Solver.Mios.Solver -import SAT.Solver.Mios.Glucose - --- | #114: __RemoveWatch__ -{-# INLINABLE removeWatch #-} -removeWatch :: Solver -> Clause -> IO () -removeWatch Solver{..} c = do - let lvec = asVec c - l1 <- negateLit <$> getNth lvec 0 - markClause (getNthWatcher watches l1) c - l2 <- negateLit <$> getNth lvec 1 - markClause (getNthWatcher watches l2) c - --------------------------------------------------------------------------------- --- Operations on 'Clause' --------------------------------------------------------------------------------- - --- | __Fig. 8. (p.12)__ create a new LEARNT clause and adds it to watcher lists --- This is a strippped-down version of 'newClause' in Solver -{-# INLINABLE newLearntClause #-} -newLearntClause :: Solver -> Vec -> IO () -newLearntClause s@Solver{..} ps = do - good <- getBool ok - when good $ do - -- ps is a 'SizedVectorInt'; ps[0] is the number of active literals - -- Since this solver must generate only healthy learnt clauses, we need not to run misc check in 'newClause' - k <- getNth ps 0 - case k of - 1 -> do - l <- getNth ps 1 - unsafeEnqueue s l NullClause - _ -> do - -- allocate clause: - c <- newClauseFromVec True ps - let vec = asVec c - -- Pick a second literal to watch: - let - findMax :: Int -> Int -> Int -> IO Int - findMax ((< k) -> False) j _ = return j - findMax i j val = do - v' <- lit2var <$> getNth vec i - a <- getNth assigns v' - b <- getNth level v' - if (a /= lBottom) && (val < b) - then findMax (i + 1) i b - else findMax (i + 1) j val - swapBetween vec 1 =<< findMax 0 0 0 -- Let @max_i@ be the index of the literal with highest decision level - -- Bump, enqueue, store clause: - claBumpActivity s c -- newly learnt clauses should be considered active - -- Add clause to all managers - pushClause learnts c - l <- getNth vec 0 - pushClauseWithKey (getNthWatcher watches (negateLit l)) c 0 - l1 <- negateLit <$> getNth vec 1 - pushClauseWithKey (getNthWatcher watches l1) c 0 - -- update the solver state by @l@ - unsafeEnqueue s l c - -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue - setLBD s c - --- | __Simplify.__ At the top-level, a constraint may be given the opportunity to --- simplify its representation (returns @False@) or state that the constraint is --- satisfied under the current assignment and can be removed (returns @True@). --- A constraint must /not/ be simplifiable to produce unit information or to be --- conflicting; in that case the propagation has not been correctly defined. --- --- MIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy. -{-# INLINABLE simplify #-} -simplify :: Solver -> Clause -> IO Bool -simplify s c = do - n <- sizeOfClause c - let - lvec = asVec c - loop ::Int -> IO Bool - loop ((< n) -> False) = return False - loop i = do - v <- valueLit s =<< getNth lvec i - if v == 1 then return True else loop (i + 1) - loop 0 - --------------------------------------------------------------------------------- --- MIOS NOTE on Minor methods: --- --- * no (meaningful) 'newVar' in mios --- * 'assume' is defined in 'Solver' --- * `cancelUntil` is defined in 'Solver' - --------------------------------------------------------------------------------- --- Major methods - --- | M114: __Fig. 10. (p.15)__ --- --- analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel :: int&) -> [void] --- --- __Description:_- --- Analzye confilct and produce a reason clause. --- --- __Pre-conditions:__ --- * 'out_learnt' is assumed to be cleared. --- * Corrent decision level must be greater than root level. --- --- __Post-conditions:__ --- * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. --- * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the --- rest of literals. There may be others from the same level though. --- --- @analyze@ is invoked from @search@ --- {-# INLINEABLE analyze #-} -analyze :: Solver -> Clause -> IO Int -analyze s@Solver{..} confl = do - -- litvec - clearStack litsLearnt - pushToStack litsLearnt 0 -- reserve the first place for the unassigned literal - dl <- decisionLevel s - let - litsVec = asVec litsLearnt - trailVec = asVec trail - loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int - loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level - when (learnt c) $ do - claBumpActivity s c - -- update LBD like #Glucose4.0 - d <- getInt (lbd c) - when (2 < d) $ do - nblevels <- lbdOf s c - when (nblevels + 1 < d) $ do -- improve the LBD - when (d <= 30) $ setBool (protected c) True -- 30 is `lbLBDFrozenClause` - -- seems to be interesting: keep it fro the next round - setInt (lbd c) nblevels -- Update it - sc <- sizeOfClause c - let - lvec = asVec c - loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int) - loopOnLiterals ((< sc) -> False) b pc = return (b, pc) -- b = btLevel, pc = pathC - loopOnLiterals j b pc = do - (q :: Lit) <- getNth lvec j - let v = lit2var q - sn <- getNth an'seen v - l <- getNth level v - if sn == 0 && 0 < l - then do - varBumpActivity s v - setNth an'seen v 1 - if dl <= l -- cancelUntil doesn't clear level of cancelled literals - then do - -- glucose heuristics - r <- getNthClause reason v - when (r /= NullClause && learnt r) $ pushToStack lastDL q - -- end of glucose heuristics - loopOnLiterals (j + 1) b (pc + 1) - else pushToStack litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc - else loopOnLiterals (j + 1) b pc - (b', pathC') <- loopOnLiterals (if p == bottomLit then 0 else 1) bl pathC - let - -- select next clause to look at - nextPickedUpLit :: Int -> IO Int - nextPickedUpLit i = do - x <- getNth an'seen . lit2var =<< getNth trailVec i - if x == 0 then nextPickedUpLit $ i - 1 else return i - ti' <- nextPickedUpLit ti - nextP <- getNth trailVec ti' - let nextV = lit2var nextP - confl' <- getNthClause reason nextV - setNth an'seen nextV 0 - if 1 < pathC' - then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1) - else setNth litsVec 0 (negateLit nextP) >> return b' - ti <- subtract 1 <$> sizeOfStack trail - levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0 - -- Simplify phase (implemented only @expensive_ccmin@ path) - n <- sizeOfStack litsLearnt - clearStack an'stack -- analyze_stack.clear(); - clearStack an'toClear -- out_learnt.copyTo(analyze_toclear); - pushToStack an'toClear =<< getNth litsVec 0 - let - merger :: Int -> Int -> IO Int - merger ((< n) -> False) b = return b - merger i b = do - l <- getNth litsVec i - pushToStack an'toClear l - -- restrict the search depth (range) to 32 - merger (i + 1) . setBit b . (31 .&.) =<< getNth level (lit2var l) - levels <- merger 1 0 - let - loopOnLits :: Int -> Int -> IO () - loopOnLits ((< n) -> False) n' = shrinkStack litsLearnt $ n - n' - loopOnLits i j = do - l <- getNth litsVec i - c1 <- (NullClause ==) <$> getNthClause reason (lit2var l) - if c1 - then setNth litsVec j l >> loopOnLits (i + 1) (j + 1) - else do - c2 <- not <$> analyzeRemovable s l levels - if c2 - then setNth litsVec j l >> loopOnLits (i + 1) (j + 1) - else loopOnLits (i + 1) j - loopOnLits 1 1 -- the first literal is specail - -- glucose heuristics - nld <- sizeOfStack lastDL - lbd' <- computeLBD s $ asSizedVec litsLearnt -- this is not the right value - let - vec = asVec lastDL - loopOnLastDL :: Int -> IO () - loopOnLastDL ((< nld) -> False) = return () - loopOnLastDL i = do - v <- lit2var <$> getNth vec i - d' <- getInt . lbd =<< getNthClause reason v - when (lbd' < d') $ varBumpActivity s v - loopOnLastDL $ i + 1 - loopOnLastDL 0 - clearStack lastDL - -- Clear seen - k <- sizeOfStack an'toClear - let - vec' = asVec an'toClear - cleaner :: Int -> IO () - cleaner ((< k) -> False) = return () - cleaner i = do - v <- lit2var <$> getNth vec' i - setNth an'seen v 0 - cleaner $ i + 1 - cleaner 0 - return levelToReturn - --- | #M114 --- Check if 'p' can be removed, 'abstract_levels' is used to abort early if the algorithm is --- visiting literals at levels that cannot be removed later. --- --- Implementation memo: --- --- * @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt'). --- This is used only in this function and @analyze@. --- -{-# INLINEABLE analyzeRemovable #-} -analyzeRemovable :: Solver -> Lit -> Int -> IO Bool -analyzeRemovable Solver{..} p minLevel = do - -- assert (reason[var(p)]!= NullCaulse); - clearStack an'stack -- analyze_stack.clear() - pushToStack an'stack p -- analyze_stack.push(p); - top <- sizeOfStack an'toClear - let - loopOnStack :: IO Bool - loopOnStack = do - k <- sizeOfStack an'stack -- int top = analyze_toclear.size(); - if 0 == k - then return True - else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL); - sl <- lastOfStack an'stack - popFromStack an'stack -- analyze_stack.pop(); - c <- getNthClause reason (lit2var sl) -- getRoot sl - nl <- sizeOfClause c - let - cvec = asVec c - loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){ - loopOnLit ((< nl) -> False) = loopOnStack - loopOnLit i = do - p' <- getNth cvec i -- valid range is [0 .. nl - 1] - let v' = lit2var p' - l' <- getNth level v' - c1 <- (1 /=) <$> getNth an'seen v' - if c1 && (0 /= l') -- if (!analyze_seen[var(p)] && level[var(p)] != 0){ - then do - c3 <- (NullClause /=) <$> getNthClause reason v' - if c3 && testBit minLevel (l' .&. 31) -- if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){ - then do - setNth an'seen v' 1 -- analyze_seen[var(p)] = 1; - pushToStack an'stack p' -- analyze_stack.push(p); - pushToStack an'toClear p' -- analyze_toclear.push(p); - loopOnLit $ i + 1 - else do - -- loopOnLit (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0; - top' <- sizeOfStack an'toClear - let vec = asVec an'toClear - forM_ [top .. top' - 1] $ \j -> do x <- getNth vec j; setNth an'seen (lit2var x) 0 - -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop - shrinkStack an'toClear $ top' - top - return False - else loopOnLit $ i + 1 - loopOnLit 1 - loopOnStack - --- | #114 --- analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void] --- --- __Description:__ --- Specialized analysis proceduce to express the final conflict in terms of assumptions. --- 'root_level' is allowed to point beyond end of trace (useful if called after conflict while --- making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed --- if conflict arose before search even started). --- -analyzeFinal :: Solver -> Clause -> Bool -> IO () -analyzeFinal Solver{..} confl skipFirst = do - clearStack conflict - rl <- getInt rootLevel - unless (rl == 0) $ do - n <- sizeOfClause confl - let - lvec = asVec confl - loopOnConfl :: Int -> IO () - loopOnConfl ((< n) -> False) = return () - loopOnConfl i = do - (x :: Var) <- lit2var <$> getNth lvec i - lvl <- getNth level x - when (0 < lvl) $ setNth an'seen x 1 - loopOnConfl $ i + 1 - loopOnConfl $ if skipFirst then 1 else 0 - tls <- sizeOfStack trailLim - trs <- sizeOfStack trail - tlz <- getNth (asVec trailLim) 0 - let - trailVec = asVec trail - loopOnTrail :: Int -> IO () - loopOnTrail ((tlz <=) -> False) = return () - loopOnTrail i = do - (l :: Lit) <- getNth trailVec i - let (x :: Var) = lit2var l - saw <- getNth an'seen x - when (saw == 1) $ do - (r :: Clause) <- getNthClause reason x - if r == NullClause - then pushToStack conflict (negateLit l) - else do - k <- sizeOfClause r - let - cvec = asVec r - loopOnLits :: Int -> IO () - loopOnLits ((< k) -> False) = return () - loopOnLits j = do - (v :: Var) <- lit2var <$> getNth cvec j - lv <- getNth level v - when (0 < lv) $ setNth an'seen v 1 - loopOnLits $ i + 1 - loopOnLits 1 - setNth an'seen x 0 - loopOnTrail $ i - 1 - loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth (asVec trailLim) rl - --- | M114: --- propagate : [void] -> [Clause+] --- --- __Description:__ --- Porpagates all enqueued facts. If a conflict arises, the cornflicting clause is returned. --- otherwise CRef_undef. --- --- __Post-conditions:__ --- * the propagation queue is empty, even if there was a conflict. --- --- memo: @propagate@ is invoked by @search@,`simpleDB` and `solve` -{-# INLINABLE propagate #-} -propagate :: Solver -> IO Clause -propagate s@Solver{..} = do - -- myVal <- getNth stats (fromEnum NumOfBackjump) - let -{- - myVal = 0 - bumpAllVar :: IO () -- not in use - bumpAllVar = do - let - loop :: Int -> IO () - loop ((<= nVars) -> False) = return () - loop i = do - c <- getNth pr'seen i - when (c == myVal) $ varBumpActivity s i - loop $ i + 1 - loop 1 --} - trailVec = asVec trail - while :: Clause -> Bool -> IO Clause - while confl False = {- bumpAllVar >> -} return confl - while confl True = do - (p :: Lit) <- getNth trailVec =<< getInt qHead - modifyInt qHead (+ 1) - let (ws :: ClauseExtManager) = getNthWatcher watches p - end <- numberOfClauses ws - cvec <- getClauseVector ws - bvec <- getKeyVector ws --- rc <- getNthClause reason $ lit2var p --- byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> getInt (lbd rc) else return False - let -{- - checkAllLiteralsIn :: Clause -> IO () -- not in use - checkAllLiteralsIn c = do - nc <- sizeOfClause c - let - vec = asVec c - loop :: Int -> IO () - loop((< nc) -> False) = return () - loop i = do - (v :: Var) <- lit2var <$> getNth vec i - setNth pr'seen v myVal - loop $ i + 1 - loop 0 --} - forClause :: Clause -> Int -> Int -> IO Clause - forClause confl i@((< end) -> False) j = do - shrinkManager ws (i - j) - while confl =<< ((<) <$> getInt qHead <*> sizeOfStack trail) - forClause confl i j = do - (l :: Lit) <- getNth bvec i - bv <- if l == 0 then return lFalse else valueLit s l - if bv == lTrue - then do - unless (i == j) $ do -- NOTE: if i == j, the path doesn't require accesses to cvec! - (c :: Clause) <- getNthClause cvec i - setNthClause cvec j c - setNth bvec j l - forClause confl (i + 1) (j + 1) - else do - -- checkAllLiteralsIn c - (c :: Clause) <- getNthClause cvec i - let - lits = asVec c - falseLit = negateLit p - -- Make sure the false literal is data[1] - ((falseLit ==) <$> getNth lits 0) >>= (`when` swapBetween lits 0 1) - -- if 0th watch is true, then clause is already satisfied. - (first :: Lit) <- getNth lits 0 - val <- valueLit s first - if val == lTrue - then setNthClause cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1) - else do - -- Look for new watch - cs <- sizeOfClause c - let - forLit :: Int -> IO Clause - forLit ((< cs) -> False) = do - -- Did not find watch; clause is unit under assignment: - setNthClause cvec j c - setNth bvec j 0 - result <- enqueue s first c - if not result - then do - ((== 0) <$> decisionLevel s) >>= (`when` setBool ok False) - setInt qHead =<< sizeOfStack trail - -- Copy the remaining watches: - let - copy i'@((< end) -> False) j' = forClause c i' j' - copy i' j' = do - setNthClause cvec j' =<< getNthClause cvec i' - setNth bvec j' =<< getNth bvec i' - copy (i' + 1) (j' + 1) - copy (i + 1) (j + 1) - else forClause confl (i + 1) (j + 1) - forLit k = do - (l :: Lit) <- getNth lits k - lv <- valueLit s l - if lv /= lFalse - then do - swapBetween lits 1 k - pushClauseWithKey (getNthWatcher watches (negateLit l)) c l - forClause confl (i + 1) j - else forLit $ k + 1 - forLit 2 - forClause confl 0 0 - while NullClause =<< ((<) <$> getInt qHead <*> sizeOfStack trail) - --- | #M22 --- reduceDB: () -> [void] --- --- __Description:__ --- Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked --- clauses are clauses that are reason to some assignment. Binary clauses are never removed. -{-# INLINABLE reduceDB #-} -reduceDB :: Solver -> IO () -reduceDB s@Solver{..} = do - n <- nLearnts s - vec <- getClauseVector learnts - let - loop :: Int -> IO () - loop ((< n) -> False) = return () - loop i = (removeWatch s =<< getNthClause vec i) >> loop (i + 1) - k <- sortClauses s learnts (div n 2) -- k is the number of clauses not to be purged - loop k -- CAVEAT: `vec` is a zero-based vector - garbageCollect watches - shrinkManager learnts (n - k) - --- | (Good to Bad) Quick sort the key vector based on their activities and returns number of privileged clauses. --- this function uses the same metrix as reduceDB_lt in glucose 4.0: --- 1. binary clause --- 2. smaller lbd --- 3. larger activity defined in MiniSat --- , where smaller value is better. --- --- they are coded into an Int as the following layout: --- --- * 14 bit: LBD or 0 for preserved clauses --- * 19 bit: converted activity --- * remain: clauseVector index --- -(lbdWidth :: Int, activityWidth :: Int, indexWidth :: Int) = (l, a, w - (l + a + 1)) - where - w = finiteBitSize (0:: Int) - (l, a) = case () of - _ | 64 <= w -> (16, 19) -- 28 bit => 256M clauses - _ | 60 <= w -> (14, 19) -- 26 bit => 32M clauses - _ | 32 <= w -> ( 7, 6) -- 18 bit => 256K clauses - _ | 29 <= w -> ( 6, 5) -- 17 bit => 128K clauses - _ -> error "Int on your CPU doesn't have sufficient bit width." - -{-# INLINABLE sortClauses #-} -sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int -sortClauses s cm nneeds = do - -- constants - let - lbdMax :: Int - lbdMax = 2 ^ lbdWidth - 1 - activityMax :: Int - activityMax = 2 ^ activityWidth - 1 - activityScale :: Double - activityScale = fromIntegral activityMax - indexMax :: Int - indexMax = (2 ^ indexWidth - 1) -- 67,108,863 for 26 - n <- numberOfClauses cm - when (indexMax < n) $ error $ "## The number of learnt clauses " ++ show n ++ " exceeds mios's " ++ show indexWidth ++" bit manage capacity" - vec <- getClauseVector cm - keys <- getKeyVector cm - -- 1: assign keys - let - assignKey :: Int -> Int -> IO Int - assignKey ((< n) -> False) m = return m - assignKey i m = do - c <- getNthClause vec i - k <- (\k -> if k == 2 then return k else fromEnum <$> getBool (protected c)) =<< sizeOfClause c - case k of - 1 -> setBool (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1) - 2 -> setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1) - _ -> do - l <- locked s c -- this is expensive - if l - then setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1) - else do - d <- getInt $ lbd c - b <- floor . (activityScale *) . (1 -) . logBase 1e100 . max 1 <$> getDouble (activity c) - setNth keys i $ shiftL (min lbdMax d) (activityWidth + indexWidth) + shiftL b indexWidth + i - assignKey (i + 1) m - limit <- min n . (+ nneeds) <$> assignKey 0 0 - -- 2: sort keyVector - let - sortOnRange :: Int -> Int -> IO () - sortOnRange left right - | limit < left = return () - | left >= right = return () - | left + 1 == right = do - a <- getNth keys left - b <- getNth keys right - unless (a < b) $ swapBetween keys left right - | otherwise = do - let p = div (left + right) 2 - pivot <- getNth keys p - swapBetween keys p left -- set a sentinel for r' - let - nextL :: Int -> IO Int - nextL i@((<= right) -> False) = return i - nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 1) else return i - nextR :: Int -> IO Int - -- nextR i@((left <=) -> False) = return i - nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 1) else return i - divide :: Int -> Int -> IO Int - divide l r = do - l' <- nextL l - r' <- nextR r - if l' < r' then swapBetween keys l' r' >> divide (l' + 1) (r' - 1) else return r' - m <- divide (left + 1) right - swapBetween keys left m - sortOnRange left (m - 1) - sortOnRange (m + 1) right - sortOnRange 0 (n - 1) - -- 3: place clauses - let - seek :: Int -> IO () - seek ((< limit) -> False) = return () - seek i = do - bits <- getNth keys i - when (indexMax < bits) $ do - c <- getNthClause vec i - let - sweep k = do - k' <- (indexMax .&.) <$> getNth keys k - setNth keys k k - if k' == i - then setNthClause vec k c - else getNthClause vec k' >>= setNthClause vec k >> sweep k' - sweep i - seek $ i + 1 - seek 0 - return limit - --- | #M22 --- --- simplify : [void] -> [bool] --- --- __Description:__ --- Simplify the clause database according to the current top-level assigment. Currently, the only --- thing done here is the removal of satisfied clauses, but more things can be put here. --- -{-# INLINABLE simplifyDB #-} -simplifyDB :: Solver -> IO Bool -simplifyDB s@Solver{..} = do - good <- getBool ok - if good - then do - p <- propagate s - if p /= NullClause - then setBool ok False >> return False - else do - -- Clear watcher lists: - n <- sizeOfStack trail - let - vec = asVec trail - loopOnLit ((< n) -> False) = return () - loopOnLit i = do - l <- getNth vec i - clearManager . getNthWatcher watches $ l - clearManager . getNthWatcher watches $ negateLit l - loopOnLit $ i + 1 - loopOnLit 0 - -- Remove satisfied clauses: - let - for :: Int -> IO Bool - for ((< 2) -> False) = return True - for t = do - let ptr = if t == 0 then learnts else clauses - vec' <- getClauseVector ptr - n' <- numberOfClauses ptr - let - loopOnVector :: Int -> Int -> IO Bool - loopOnVector ((< n') -> False) j = shrinkManager ptr (n' - j) >> return True - loopOnVector i j = do - c <- getNthClause vec' i - l <- locked s c - r <- simplify s c - if not l && r - then removeWatch s c >> loopOnVector (i + 1) j - else setNthClause vec' j c >> loopOnVector (i + 1) (j + 1) - loopOnVector 0 0 - ret <- for 0 - garbageCollect watches - return ret - else return False - --- | #M22 --- --- search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] --- --- __Description:__ --- Search for a model the specified number of conflicts. --- NOTE: Use negative value for 'nof_conflicts' indicate infinity. --- --- __Output:__ --- 'l_True' if a partial assigment that is consistent with respect to the clause set is found. If --- all variables are decision variables, that means that the clause set is satisfiable. 'l_False' --- if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. -{-# INLINABLE search #-} -search :: Solver -> Int -> Int -> IO LiftedBool -search s@Solver{..} nOfConflicts nOfLearnts = do - -- clear model - let - loop :: Int -> IO LiftedBool - loop conflictC = do - !confl <- propagate s - d <- decisionLevel s - if confl /= NullClause - then do - -- CONFLICT - incrementStat s NumOfBackjump 1 - r <- getInt rootLevel - if d == r - then do - -- Contradiction found: - analyzeFinal s confl False - return LFalse - else do --- u <- (== 0) . (flip mod 5000) <$> getNth stats (fromEnum NumOfBackjump) --- when u $ do --- d <- getDouble varDecay --- when (d < 0.95) $ modifyDouble varDecay (+ 0.01) - backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself - (s `cancelUntil`) . max backtrackLevel =<< getInt rootLevel - newLearntClause s $ asSizedVec litsLearnt - k <- sizeOfStack litsLearnt - when (k == 1) $ do - (v :: Var) <- lit2var <$> getNth (asVec litsLearnt) 0 - setNth level v 0 - varDecayActivity s - claDecayActivity s - loop $ conflictC + 1 - else do -- NO CONFLICT - -- Simplify the set of problem clauses: - when (d == 0) . void $ simplifyDB s -- our simplifier cannot return @False@ here - k1 <- numberOfClauses learnts - k2 <- nAssigns s - when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses - case () of - _ | k2 == nVars -> do - -- Model found: - forM_ [0 .. nVars - 1] $ \i -> setNthBool model i . (lTrue ==) =<< getNth assigns (i + 1) - return LTrue - _ | conflictC >= nOfConflicts -> do - -- Reached bound on number of conflicts - (s `cancelUntil`) =<< getInt rootLevel -- force a restart - incrementStat s NumOfRestart 1 - return Bottom - _ -> do - -- New variable decision: - v <- select s -- many have heuristic for polarity here - -- << #phasesaving - oldVal <- getNth phases v - unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@ - -- >> #phasesaving - loop conflictC - good <- getBool ok - if good then loop 0 else return LFalse - --- | __Fig. 16. (p.20)__ --- Main solve method. --- --- __Pre-condition:__ If assumptions are used, 'simplifyDB' must be --- called right before using this method. If not, a top-level conflict (resulting in a --- non-usable internal state) cannot be distinguished from a conflict under assumptions. -solve :: (Foldable t) => Solver -> t Lit -> IO Bool -solve s@Solver{..} assumps = do - -- PUSH INCREMENTAL ASSUMPTIONS: - let - injector :: Lit -> Bool -> IO Bool - injector _ False = return False - injector a True = do - b <- assume s a - if not b - then do -- conflict analyze - (confl :: Clause) <- getNthClause reason (lit2var a) - analyzeFinal s confl True - pushToStack conflict (negateLit a) - cancelUntil s 0 - return False - else do - confl <- propagate s - if confl /= NullClause - then do - analyzeFinal s confl True - cancelUntil s 0 - return False - else return True - good <- simplifyDB s - x <- if good then foldrM injector True assumps else return False - if not x - then return False - else do - setInt rootLevel =<< decisionLevel s - -- SOLVE: - nc <- fromIntegral <$> nClauses s - let - while :: Double -> Double -> IO Bool - while nOfConflicts nOfLearnts = do - status <- search s (floor nOfConflicts) (floor nOfLearnts) - if status == Bottom - then while (1.5 * nOfConflicts) (1.1 * nOfLearnts) - else cancelUntil s 0 >> return (status == LTrue) - while 100 (nc / 3.0) - - --- --- 'enqueue' is defined in 'Solver'; functions in M114 use 'unsafeEnqueue' --- -{-# INLINABLE unsafeEnqueue #-} -unsafeEnqueue :: Solver -> Lit -> Clause -> IO () -unsafeEnqueue s@Solver{..} p from = do - let v = lit2var p - setNth assigns v $! if positiveLit p then lTrue else lFalse - setNth level v =<< decisionLevel s - setNthClause reason v from -- NOTE: @from@ might be NULL! - pushToStack trail p - --- __Pre-condition:__ propagation queue is empty -{-# INLINE unsafeAssume #-} -unsafeAssume :: Solver -> Lit -> IO () -unsafeAssume s@Solver{..} p = do - pushToStack trailLim =<< sizeOfStack trail - unsafeEnqueue s p NullClause - -{- --- | for debug -fromAssigns :: Vec -> IO [Int] -fromAssigns as = zipWith f [1 .. ] . tail <$> asList as - where - f n x - | x == lTrue = n - | x == lFalse = negate n - | otherwise = 0 - --- | for debug -dumpAssignment :: String -> Vec -> IO String -dumpAssignment mes v = (mes ++) . show <$> fromAssigns v --} diff --git a/SAT/Solver/Mios/OptionParser.hs b/SAT/Solver/Mios/OptionParser.hs deleted file mode 100644 --- a/SAT/Solver/Mios/OptionParser.hs +++ /dev/null @@ -1,132 +0,0 @@ -{-# LANGUAGE Safe #-} --- | command line option parser for mios -module SAT.Solver.Mios.OptionParser - ( - MiosConfiguration (..) - , defaultConfiguration - , MiosProgramOption (..) - , miosDefaultOption - , miosOptions - , miosUsage - , miosParseOptions - , miosParseOptionsFromArgs - , toMiosConf - ) - where - -import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo) -import System.Environment (getArgs) -import SAT.Solver.Mios.Internal (MiosConfiguration (..), defaultConfiguration) - --- | configuration swithces -data MiosProgramOption = MiosProgramOption - { - _targetFile :: Maybe String - , _outputFile :: Maybe String - , _confVariableDecayRate :: Double - , _confClauseDecayRate :: Double --- , _confRandomDecisionRate :: Int - , _confCheckAnswer :: Bool - , _confVerbose :: Bool - , _confTimeProbe :: Bool - , _confStatProbe :: Bool - , _confNoAnswer :: Bool - , _validateAssignment :: Bool - , _displayHelp :: Bool - , _displayVersion :: Bool - } - --- | default option settings -miosDefaultOption :: MiosProgramOption -miosDefaultOption = MiosProgramOption - { - _targetFile = Just "" - , _outputFile = Nothing - , _confVariableDecayRate = variableDecayRate defaultConfiguration - , _confClauseDecayRate = clauseDecayRate defaultConfiguration --- , _confRandomDecisionRate = randomDecisionRate defaultConfiguration - , _confCheckAnswer = False - , _confVerbose = False - , _confTimeProbe = False - , _confStatProbe = collectStats defaultConfiguration - , _confNoAnswer = False - , _validateAssignment = False - , _displayHelp = False - , _displayVersion = False - } - --- | definition of mios option -miosOptions :: [OptDescr (MiosProgramOption -> MiosProgramOption)] -miosOptions = - [ - Option ['d'] ["variable-decay-rate"] - (ReqArg (\v c -> c { _confVariableDecayRate = read v }) (show (_confVariableDecayRate miosDefaultOption))) - "[solver] variable activity decay rate (0.0 - 1.0)" - , Option ['c'] ["clause-decay-rate"] - (ReqArg (\v c -> c { _confClauseDecayRate = read v }) (show (_confClauseDecayRate miosDefaultOption))) - "[solver] clause activity decay rate (0.0 - 1.0)" --- , Option ['r'] ["random-decision-rate"] --- (ReqArg (\v c -> c { _confRandomDecisionRate = read v }) (show (_confRandomDecisionRate miosDefaultOption))) --- "[solver] random selection rate (0 - 1000)" - , Option [':'] ["validate-assignment"] - (NoArg (\c -> c { _validateAssignment = True })) - "[solver] read an assignment from STDIN and validate it" - , Option [] ["validate"] - (NoArg (\c -> c { _confCheckAnswer = True })) - "[solver] self-check the (satisfied) answer" - , Option ['o'] ["output"] - (ReqArg (\v c -> c { _outputFile = Just v })"file") - "[option] filename to store the result" -{- - , Option [] ["stdin"] - (NoArg (\c -> c { _targetFile = Nothing })) - "[option] read a CNF from STDIN instead of a file" --} - , Option ['v'] ["verbose"] - (NoArg (\c -> c { _confVerbose = True })) - "[option] display misc information" - , Option ['X'] ["hide-solution"] - (NoArg (\c -> c { _confNoAnswer = True })) - "[option] hide the solution" - , Option [] ["time"] - (NoArg (\c -> c { _confTimeProbe = True })) - "[option] display execution time" - , Option [] ["stat"] - (NoArg (\c -> c { _confStatProbe = True })) - "[option] display statistics information" - , Option ['h'] ["help"] - (NoArg (\c -> c { _displayHelp = True })) - "[misc] display this help message" - , Option [] ["version"] - (NoArg (\c -> c { _displayVersion = True })) - "[misc] display program ID" - ] - --- | generates help message -miosUsage :: String -> String -miosUsage mes = usageInfo mes miosOptions - --- | builds "MiosProgramOption" from string given as command option -miosParseOptions :: String -> [String] -> IO MiosProgramOption -miosParseOptions mes argv = - case getOpt Permute miosOptions argv of - (o, [], []) -> do - return $ foldl (flip id) miosDefaultOption o - (o, (n:_), []) -> do - let conf = foldl (flip id) miosDefaultOption o - return $ conf { _targetFile = Just n } - (_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes)) - --- | builds "MiosProgramOption" from a String -miosParseOptionsFromArgs :: String -> IO MiosProgramOption -miosParseOptionsFromArgs mes = miosParseOptions mes =<< getArgs - --- | converts "MiosProgramOption" into "SIHConfiguration" -toMiosConf :: MiosProgramOption -> MiosConfiguration -toMiosConf opts = MiosConfiguration - { - variableDecayRate = _confVariableDecayRate opts - , clauseDecayRate = _confClauseDecayRate opts --- , randomDecisionRate = _confRandomDecisionRate opts - , collectStats = _confStatProbe opts - } diff --git a/SAT/Solver/Mios/Solver.hs b/SAT/Solver/Mios/Solver.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Solver.hs +++ /dev/null @@ -1,554 +0,0 @@ --- | This is a part of MIOS -{-# LANGUAGE - BangPatterns - , RecordWildCards - , ScopedTypeVariables - , TupleSections - , ViewPatterns - #-} -{-# LANGUAGE Safe #-} - -module SAT.Solver.Mios.Solver - ( - -- * Solver - Solver (..) - , newSolver - -- * Misc Accessors - , nAssigns - , nClauses - , nLearnts - , decisionLevel - , valueVar - , valueLit - , locked - , VarHeap - -- * State Modifiers - , addClause - , enqueue - , assume - , cancelUntil - , getModel - -- * Activities - , claBumpActivity - , claDecayActivity - , varBumpActivity - , varDecayActivity - -- * Stats - , StatIndex (..) - , incrementStat - , getStats - ) - where - -import Control.Monad ((<=<), forM_, unless, when) -import SAT.Solver.Mios.Types -import SAT.Solver.Mios.Internal -import SAT.Solver.Mios.Clause -import SAT.Solver.Mios.ClauseManager - --- | __Fig. 2.(p.9)__ Internal State of the solver -data Solver = Solver - { - -- Public Interface - model :: !VecBool -- ^ If found, this vector has the model - , conflict :: !Stack -- ^ set of literals in the case of conflicts - -- Clause Database - , clauses :: !ClauseExtManager -- ^ List of problem constraints. - , learnts :: !ClauseExtManager -- ^ List of learnt clauses. - , watches :: !WatcherList -- ^ a list of constraint wathing 'p', literal-indexed - -- Assignment Management - , assigns :: !Vec -- ^ The current assignments indexed on variables; var-indexed - , phases :: !Vec -- ^ The last assignments indexed on variables; var-indexed - , trail :: !Stack -- ^ List of assignments in chronological order; var-indexed - , trailLim :: !Stack -- ^ Separator indices for different decision levels in 'trail'. - , qHead :: !IntSingleton -- ^ 'trail' is divided at qHead; assignments and queue - , reason :: !ClauseVector -- ^ For each variable, the constraint that implied its value; var-indexed - , level :: !Vec -- ^ For each variable, the decision level it was assigned; var-indexed - -- Variable Order - , activities :: !VecDouble -- ^ Heuristic measurement of the activity of a variable; var-indexed - , order :: !VarHeap -- ^ Keeps track of the dynamic variable order. - -- Configuration - , config :: !MiosConfiguration -- ^ search paramerters - , nVars :: !Int -- ^ number of variables - , claInc :: !DoubleSingleton -- ^ Clause activity increment amount to bump with. --- , varDecay :: !DoubleSingleton -- ^ used to set 'varInc' - , varInc :: !DoubleSingleton -- ^ Variable activity increment amount to bump with. - , rootLevel :: !IntSingleton -- ^ Separates incremental and search assumptions. - -- Working Memory - , ok :: !BoolSingleton -- ^ return value holder - , an'seen :: !Vec -- ^ scratch var for 'analyze'; var-indexed - , an'toClear :: !Stack -- ^ ditto - , an'stack :: !Stack -- ^ ditto - , pr'seen :: !Vec -- ^ used in propagate - , lbd'seen :: !Vec -- ^ used in lbd computation - , lbd'key :: !IntSingleton -- ^ used in lbd computation - , litsLearnt :: !Stack -- ^ used to create a learnt clause - , lastDL :: !Stack -- ^ last decision level used in analyze - , stats :: !Vec -- ^ statistics information holder - } - --- | returns an everything-is-initialized solver from the arguments -newSolver :: MiosConfiguration -> CNFDescription -> IO Solver -newSolver conf (CNFDescription nv nc _) = do - Solver - -- Public Interface - <$> newVecBool nv False -- model - <*> newStack nv -- coflict - -- Clause Database - <*> newManager nc -- clauses - <*> newManager nc -- learnts - <*> newWatcherList nv 2 -- watches - -- Assignment Management - <*> newVecWith (nv + 1) lBottom -- assigns - <*> newVecWith (nv + 1) lBottom -- phases - <*> newStack nv -- trail - <*> newStack nv -- trailLim - <*> newInt 0 -- qHead - <*> newClauseVector (nv + 1) -- reason - <*> newVecWith (nv + 1) (-1) -- level - -- Variable Order - <*> newVecDouble (nv + 1) 0 -- activities - <*> newVarHeap nv -- order - -- Configuration - <*> return conf -- config - <*> return nv -- nVars - <*> newDouble 1.0 -- claInc --- <*> newDouble (variableDecayRate conf) -- varDecay - <*> newDouble 1.0 -- varInc - <*> newInt 0 -- rootLevel - -- Working Memory - <*> newBool True -- ok - <*> newVec (nv + 1) -- an'seen - <*> newStack nv -- an'toClear - <*> newStack nv -- an'stack - <*> newVecWith (nv + 1) (-1) -- pr'seen - <*> newVec nv -- lbd'seen - <*> newInt 0 -- lbd'key - <*> newStack nv -- litsLearnt - <*> newStack nv -- lastDL - <*> newVec (1 + fromEnum (maxBound :: StatIndex)) -- stats - --------------------------------------------------------------------------------- --- Accessors - --- | returns the number of current assigments -{-# INLINE nAssigns #-} -nAssigns :: Solver -> IO Int -nAssigns = sizeOfStack . trail - --- | returns the number of constraints (clauses) -{-# INLINE nClauses #-} -nClauses :: Solver -> IO Int -nClauses = numberOfClauses . clauses - --- | returns the number of learnt clauses -{-# INLINE nLearnts #-} -nLearnts :: Solver -> IO Int -nLearnts = numberOfClauses . learnts - --- | return the model as a list of literal -getModel :: Solver -> IO [Int] -getModel s = zipWith (\n b -> if b then n else negate n) [1 .. ] <$> asList (model s) - --- | returns the current decision level -{-# INLINE decisionLevel #-} -decisionLevel :: Solver -> IO Int -decisionLevel Solver{..} = sizeOfStack trailLim - --- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Var' -{-# INLINE valueVar #-} -valueVar :: Solver -> Var -> IO Int -valueVar s !x = getNth (assigns s) x - --- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit' -{-# INLINE valueLit #-} -valueLit :: Solver -> Lit -> IO Int -- FIXME: LiftedBool -valueLit Solver{..} !p = if positiveLit p then getNth assigns (lit2var p) else negate <$> getNth assigns (lit2var p) - --- | __Fig. 7. (p.11)__ --- returns @True@ if the clause is locked (used as a reason). __Learnt clauses only__ -{-# INLINE locked #-} -locked :: Solver -> Clause -> IO Bool -locked Solver{..} c@Clause{..} = (c ==) <$> (getNthClause reason . lit2var =<< getNth lits 1) - --- | stats -data StatIndex = - NumOfBackjump - | NumOfRestart - deriving (Bounded, Enum, Eq, Ord, Read, Show) - --- | increments a stat data corresponding to 'StatIndex' -incrementStat :: Solver -> StatIndex -> Int -> IO () -incrementStat (config -> collectStats -> False) _ _ = return () -incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i - --- | returns the statistics as list -getStats :: Solver -> IO [(StatIndex, Int)] -getStats (config -> collectStats -> False) = return [] -getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex] - --------------------------------------------------------------------------------- State Modifiers - --- | returns @False@ if a conflict has occured. --- This function is called only before the solving phase to register the given clauses. -{-# INLINABLE addClause #-} -addClause :: Solver -> Vec -> IO Bool -addClause s@Solver{..} vecLits = do - result <- clauseNew s vecLits False - case result of - (False, _) -> return False -- Conflict occured - (True, c) -> do - unless (c == NullClause) $ pushClause clauses c - return True -- No conflict - --- | __Fig. 8. (p.12)__ create a new clause and adds it to watcher lists --- Constructor function for clauses. Returns @False@ if top-level conflict is determined. --- @outClause@ may be set to Null if the new clause is already satisfied under the current --- top-level assignment. --- --- __Post-condition:__ @ps@ is cleared. For learnt clauses, all --- literals will be false except @lits[0]@ (this by design of the 'analyze' method). --- For the propagation to work, the second watch must be put on the literal which will --- first be unbound by backtracking. (Note that none of the learnt-clause specific things --- needs to done for a user defined contraint type.) -{-# INLINABLE clauseNew #-} -clauseNew :: Solver -> Vec -> Bool -> IO (Bool, Clause) -clauseNew s@Solver{..} ps isLearnt = do - -- now ps[0] is the number of living literals - exit <- do - let - handle :: Int -> Int -> Int -> IO Bool - handle j l n -- removes duplicates, but returns @True@ if this clause is satisfied - | j > n = return False - | otherwise = do - y <- getNth ps j - case () of - _ | y == l -> do -- finds a duplicate - swapBetween ps j n - modifyNth ps (subtract 1) 0 - handle j l (n - 1) - _ | - y == l -> setNth ps 0 0 >> return True -- p and negateLit p occurs in ps - _ -> handle (j + 1) l n - loopForLearnt :: Int -> IO Bool - loopForLearnt i = do - n <- getNth ps 0 - if n < i - then return False - else do - l <- getNth ps i - sat <- handle (i + 1) l n - if sat - then return True - else loopForLearnt $ i + 1 - loop :: Int -> IO Bool - loop i = do - n <- getNth ps 0 - if n < i - then return False - else do - l <- getNth ps i -- check the i-th literal's satisfiability - sat <- valueLit s l -- any literal in ps is true - case sat of - 1 -> setNth ps 0 0 >> return True - -1 -> do - swapBetween ps i n - modifyNth ps (subtract 1) 0 - loop i - _ -> do - sat' <- handle (i + 1) l n - if sat' - then return True - else loop $ i + 1 - if isLearnt then loopForLearnt 1 else loop 1 - k <- getNth ps 0 - case k of - 0 -> return (exit, NullClause) - 1 -> do - l <- getNth ps 1 - (, NullClause) <$> enqueue s l NullClause - _ -> do - -- allocate clause: - c <- newClauseFromVec isLearnt ps - let vec = asVec c - when isLearnt $ do - -- Pick a second literal to watch: - let - findMax :: Int -> Int -> Int -> IO Int - findMax ((< k) -> False) j _ = return j - findMax i j val = do - v' <- lit2var <$> getNth vec i - a <- getNth assigns v' - b <- getNth level v' - if (a /= lBottom) && (val < b) - then findMax (i + 1) i b - else findMax (i + 1) j val - -- Let @max_i@ be the index of the literal with highest decision level - max_i <- findMax 0 0 0 - swapBetween vec 1 max_i - -- check literals occurences - -- x <- asList c - -- unless (length x == length (nub x)) $ error "new clause contains a element doubly" - -- Bumping: - claBumpActivity s c -- newly learnt clauses should be considered active - forM_ [0 .. k -1] $ varBumpActivity s . lit2var <=< getNth vec -- variables in conflict clauses are bumped - -- Add clause to watcher lists: - l0 <- negateLit <$> getNth vec 0 - pushClauseWithKey (getNthWatcher watches l0) c 0 - l1 <- negateLit <$> getNth vec 1 - pushClauseWithKey (getNthWatcher watches l1) c 0 - return (True, c) - --- | __Fig. 9 (p.14)__ --- Puts a new fact on the propagation queue, as well as immediately updating the variable's value --- in the assignment vector. If a conflict arises, @False@ is returned and the propagation queue is --- cleared. The parameter 'from' contains a reference to the constraint from which 'p' was --- propagated (defaults to @Nothing@ if omitted). -{-# INLINABLE enqueue #-} -enqueue :: Solver -> Lit -> Clause -> IO Bool -enqueue s@Solver{..} p from = do - -- putStrLn . ("ssigns " ++) . show . map lit2int =<< asList trail - -- putStrLn =<< dump ("enqueue " ++ show (lit2int p) ++ " ") from - let signumP = if positiveLit p then lTrue else lFalse - let v = lit2var p - val <- valueVar s v - if val /= lBottom - then do -- Existing consistent assignment -- don't enqueue - return $ val == signumP - else do - -- New fact, store it - setNth assigns v $! signumP - setNth level v =<< decisionLevel s - setNthClause reason v from -- NOTE: @from@ might be NULL! - pushToStack trail p - return True - --- | __Fig. 12 (p.17)__ --- returns @False@ if immediate conflict. --- --- __Pre-condition:__ propagation queue is empty -{-# INLINE assume #-} -assume :: Solver -> Lit -> IO Bool -assume s@Solver{..} p = do - pushToStack trailLim =<< sizeOfStack trail - enqueue s p NullClause - --- | #M22: Revert to the states at given level (keeping all assignment at 'level' but not beyond). -{-# INLINABLE cancelUntil #-} -cancelUntil :: Solver -> Int -> IO () -cancelUntil s@Solver{..} lvl = do - dl <- decisionLevel s - when (lvl < dl) $ do - let tr = asVec trail - let tl = asVec trailLim - lim <- getNth tl lvl - ts <- sizeOfStack trail - ls <- sizeOfStack trailLim - let - loopOnTrail :: Int -> IO () - loopOnTrail ((lim <=) -> False) = return () - loopOnTrail c = do - x <- lit2var <$> getNth tr c - setNth phases x =<< getNth assigns x - setNth assigns x lBottom - -- #reason to set reason Null - -- if we don't clear @reason[x] :: Clause@ here, @reason[x]@ remains as locked. - -- This means we can't reduce it from clause DB and affects the performance. - setNthClause reason x NullClause -- 'analyze` uses reason without checking assigns - -- FIXME: #polarity https://github.com/shnarazk/minisat/blosb/master/core/Solver.cc#L212 - undo s x - -- insertHeap s x -- insertVerOrder - loopOnTrail $ c - 1 - loopOnTrail $ ts - 1 - shrinkStack trail (ts - lim) - shrinkStack trailLim (ls - lvl) - setInt qHead =<< sizeOfStack trail - --------------------------------------------------------------------------------- VarOrder - --- | Interfate to select a decision var based on variable activity. -instance VarOrder Solver where - -- | __Fig. 6. (p.10)__ - -- Creates a new SAT variable in the solver. - newVar _ = return 0 - -- i <- nVars s - -- Version 0.4:: push watches =<< newVec -- push' - -- Version 0.4:: push watches =<< newVec -- push' - -- push undos =<< newVec -- push' - -- push reason NullClause -- push' - -- push assigns lBottom - -- push level (-1) - -- push activities (0.0 :: Double) - -- newVar order - -- growQueueSized (i + 1) propQ - -- return i - {-# SPECIALIZE INLINE update :: Solver -> Var -> IO () #-} - update = increaseHeap - {-# SPECIALIZE INLINE undo :: Solver -> Var -> IO () #-} - undo s v = inHeap s v >>= (`unless` insertHeap s v) - {-# SPECIALIZE INLINE select :: Solver -> IO Var #-} - select s = do - let - asg = assigns s - -- | returns the most active var (heap-based implementation) - loop :: IO Var - loop = do - n <- numElementsInHeap s - if n == 0 - then return 0 - else do - v <- getHeapRoot s - x <- getNth asg v - if x == lBottom then return v else loop - loop - --------------------------------------------------------------------------------- Activities - --- | __Fig. 14 (p.19)__ Bumping of clause activity -{-# INLINE varBumpActivity #-} -varBumpActivity :: Solver -> Var -> IO () -varBumpActivity s@Solver{..} !x = do - !a <- (+) <$> getNthDouble x activities <*> getDouble varInc - if 1e100 < a - then varRescaleActivity s - else setNthDouble x activities a - update s x - --- | __Fig. 14 (p.19)__ -{-# INLINE varDecayActivity #-} -varDecayActivity :: Solver -> IO () -varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config) --- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay - --- | __Fig. 14 (p.19)__ -{-# INLINE varRescaleActivity #-} -varRescaleActivity :: Solver -> IO () -varRescaleActivity Solver{..} = do - forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (* 1e-100) - modifyDouble varInc (* 1e-100) - --- | __Fig. 14 (p.19)__ -{-# INLINE claBumpActivity #-} -claBumpActivity :: Solver -> Clause -> IO () -claBumpActivity s@Solver{..} Clause{..} = do - a <- (+) <$> getDouble activity <*> getDouble claInc - if 1e100 < a - then claRescaleActivity s - else setDouble activity a - --- | __Fig. 14 (p.19)__ -{-# INLINE claDecayActivity #-} -claDecayActivity :: Solver -> IO () -claDecayActivity Solver{..} = modifyDouble claInc (/ clauseDecayRate config) - --- | __Fig. 14 (p.19)__ -{-# INLINE claRescaleActivity #-} -claRescaleActivity :: Solver -> IO () -claRescaleActivity Solver{..} = do - vec <- getClauseVector learnts - n <- numberOfClauses learnts - let - loopOnVector :: Int -> IO () - loopOnVector ((< n) -> False) = return () - loopOnVector i = do - c <- getNthClause vec i - modifyDouble (activity c) (* 1e-20) -- not 1e-100 - loopOnVector $ i + 1 - loopOnVector 0 - modifyDouble claInc (* 1e-20) -- not 1e-100 - --------------------------------------------------------------------------------- VarHeap - --- | 'VarHeap' is a heap tree built from two 'Vec' --- This implementation is identical wtih that in Minisat-1.14 --- Note: the zero-th element of @heap@ is used for holding the number of elements --- Note: VarHeap itself is not a @VarOrder@, because it requires a pointer to solver -data VarHeap = VarHeap - { - heap :: Vec -- order to var - , idxs :: Vec -- var to order (index) - } - -newVarHeap :: Int -> IO VarHeap -newVarHeap n = VarHeap <$> newSizedVecIntFromList lst <*> newSizedVecIntFromList lst - where - lst = [1 .. n] - -{-# INLINE numElementsInHeap #-} -numElementsInHeap :: Solver -> IO Int -numElementsInHeap (order -> heap -> h) = getNth h 0 - -{-# INLINE inHeap #-} -inHeap :: Solver -> Var -> IO Bool -inHeap (order -> idxs -> at) n = (/= 0) <$> getNth at n - -{-# INLINE increaseHeap #-} -increaseHeap :: Solver -> Int -> IO () -increaseHeap s@(order -> idxs -> at) n = inHeap s n >>= (`when` (percolateUp s =<< getNth at n)) - -{-# INLINABLE percolateUp #-} -percolateUp :: Solver -> Int -> IO () -percolateUp Solver{..} start = do - let VarHeap to at = order - v <- getNth to start - ac <- getNthDouble v activities - let - loop :: Int -> IO () - loop i = do - let iP = div i 2 -- parent - if iP == 0 - then setNth to i v >> setNth at v i -- end - else do - v' <- getNth to iP - acP <- getNthDouble v' activities - if ac > acP - then setNth to i v' >> setNth at v' i >> loop iP -- loop - else setNth to i v >> setNth at v i -- end - loop start - -{-# INLINABLE percolateDown #-} -percolateDown :: Solver -> Int -> IO () -percolateDown Solver{..} start = do - let (VarHeap to at) = order - n <- getNth to 0 - v <- getNth to start - ac <- getNthDouble v activities - let - loop :: Int -> IO () - loop i = do - let iL = 2 * i -- left - if iL <= n - then do - let iR = iL + 1 -- right - l <- getNth to iL - r <- getNth to iR - acL <- getNthDouble l activities - acR <- getNthDouble r activities - let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL) - if ac' > ac - then setNth to i child >> setNth at child i >> loop ci - else setNth to i v >> setNth at v i -- end - else setNth to i v >> setNth at v i -- end - loop start - -{-# INLINE insertHeap #-} -insertHeap :: Solver -> Var -> IO () -insertHeap s@(order -> VarHeap to at) v = do - n <- (1 +) <$> getNth to 0 - setNth at v n - setNth to n v - setNth to 0 n - percolateUp s n - --- | renamed from 'getmin' -{-# INLINE getHeapRoot #-} -getHeapRoot :: Solver -> IO Int -getHeapRoot s@(order -> VarHeap to at) = do - r <- getNth to 1 - l <- getNth to =<< getNth to 0 -- the last element's value - setNth to 1 l - setNth at l 1 - setNth at r 0 - modifyNth to (subtract 1) 0 -- pop - n <- getNth to 0 - when (1 < n) $ percolateDown s 1 - return r diff --git a/SAT/Solver/Mios/Types.hs b/SAT/Solver/Mios/Types.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Types.hs +++ /dev/null @@ -1,269 +0,0 @@ --- | Basic data types used throughout mios. -{-# LANGUAGE - BangPatterns - , FlexibleContexts - , FlexibleInstances - , FunctionalDependencies - , MultiParamTypeClasses - #-} -{-# LANGUAGE Trustworthy #-} - -module SAT.Solver.Mios.Types - ( - -- Singleton - module SAT.Solver.Mios.Data.Singleton - -- Fixed Unboxed Mutable Int Vector - , module SAT.Solver.Mios.Data.Vec - -- Abstract interfaces - , VectorFamily (..) - -- * Variable - , Var - , bottomVar - , int2var - -- * Internal encoded Literal - , Lit - , lit2int - , int2lit - , bottomLit - , newLit - , positiveLit - , lit2var - , var2lit - , negateLit - -- * Assignment - , LiftedBool (..) - , lbool - , lFalse - , lTrue - , lBottom - , VarOrder (..) - -- * CNF - , CNFDescription (..) - ) - where - -import Control.Monad (forM) -import Data.Bits -import qualified Data.Vector.Unboxed.Mutable as UV -import SAT.Solver.Mios.Data.Singleton -import SAT.Solver.Mios.Data.Vec - --- | Public interface as /Container/ -class VectorFamily s t | s -> t where - -- * Size operations - -- | erases all elements in it - clear :: s -> IO () - clear = error "no default method for clear" - -- * Debug - -- | dump the contents - dump :: Show t => String -> s -> IO String - dump msg _ = error $ msg ++ ": no defalut method for dump" - -- | get a raw data - asVec :: s -> UV.IOVector Int - asVec = error "asVector undefined" - -- | converts into a list - asList :: s -> IO [t] - asList = error "asList undefined" - {-# MINIMAL dump #-} - --- | provides 'clear' and 'size' -instance VectorFamily Vec Int where - clear = error "Vec.clear" - {-# SPECIALIZE INLINE asList :: Vec -> IO [Int] #-} - asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v - dump str v = (str ++) . show <$> asList v - {-# SPECIALIZE INLINE asVec :: Vec -> Vec #-} - asVec = id - --- | represents "Var" -type Var = Int - --- | Special constant in 'Var' (p.7) -bottomVar :: Var -bottomVar = 0 - --- | converts a usual Int as literal to an internal 'Var' presentation --- --- >>> int2var 1 --- 1 -- the first literal is the first variable --- >>> int2var 2 --- 2 -- literal @2@ is variable 2 --- >>> int2var (-2) --- 2 -- literal @-2@ is corresponding to variable 2 --- -{-# INLINE int2var #-} -int2var = abs - --- | The literal data has an 'index' method which converts the literal to --- a "small" integer suitable for array indexing. The 'var' method returns --- the underlying variable of the literal, and the 'sign' method if the literal --- is signed (False for /x/ and True for /-x/). -type Lit = Int - --- | Special constant in 'Lit' (p.7) -bottomLit :: Lit -bottomLit = 0 - --- | converts "Var" into 'Lit' -newLit :: Var -> Lit -newLit = error "newLit undefined" - --- | returns @True@ if the literal is positive -{-# INLINE positiveLit #-} -positiveLit :: Lit -> Bool -positiveLit = even - --- | negates literal --- --- >>> negateLit 2 --- 3 --- >>> negateLit 3 --- 2 --- >>> negateLit 4 --- 5 --- >>> negateLit 5 --- 4 -{-# INLINE negateLit #-} -negateLit :: Lit -> Lit -negateLit !l = complementBit l 0 -- if even l then l + 1 else l - 1 - ----------------------------------------- ------------------ Var ----------------------------------------- - --- | converts 'Lit' into 'Var' --- --- >>> lit2var 2 --- 1 --- >>> lit2var 3 --- 1 --- >>> lit2var 4 --- 2 --- >>> lit2var 5 --- 2 -{-# INLINE lit2var #-} -lit2var :: Lit -> Var -lit2var !n = shiftR n 1 - --- | converts a 'Var' to the corresponing literal --- --- >>> var2lit 1 True --- 2 --- >>> var2lit 1 False --- 3 --- >>> var2lit 2 True --- 4 --- >>> var2lit 2 False --- 5 -{-# INLINE var2lit #-} -var2lit :: Var -> Bool -> Lit -var2lit !v True = shiftL v 1 -var2lit !v _ = shiftL v 1 + 1 - ----------------------------------------- ------------------ Int ----------------------------------------- - --- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@ --- --- >>> int2lit 1 --- 2 --- >>> int2lit (-1) --- 3 --- >>> int2lit 2 --- 4 --- >>> int2lit (-2) --- 5 --- -{-# INLINE int2lit #-} -int2lit :: Int -> Lit -int2lit n - | 0 < n = 2 * n - | otherwise = -2 * n + 1 - --- | converts `Lit' into 'Int' as @int2lit . lit2int == id@ --- --- >>> lit2int 2 --- 1 --- >>> lit2int 3 --- -1 --- >>> lit2int 4 --- 2 --- >>> lit2int 5 --- -2 -{-# INLINE lit2int #-} -lit2int :: Lit -> Int -lit2int l = case divMod l 2 of - (i, 0) -> i - (i, _) -> - i - --- | Lifted Boolean domain (p.7) that extends 'Bool' with "⊥" means /undefined/ --- design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2. -data LiftedBool = Bottom | LFalse | LTrue - deriving (Bounded, Eq, Ord, Read, Show) - -instance Enum LiftedBool where - {-# SPECIALIZE INLINE toEnum :: Int -> LiftedBool #-} - toEnum 1 = LTrue - toEnum (-1) = LFalse - toEnum _ = Bottom - {-# SPECIALIZE INLINE fromEnum :: LiftedBool -> Int #-} - fromEnum Bottom = 0 - fromEnum LFalse = 1 - fromEnum LTrue = 2 - --- | converts 'Bool' into 'LBool' -{-# INLINE lbool #-} -lbool :: Bool -> LiftedBool -lbool True = LTrue -lbool False = LFalse - --- | A contant representing False -lFalse:: Int -lFalse = -1 - --- | A constant representing True -lTrue :: Int -lTrue = 1 - --- | A constant for "undefined" -lBottom :: Int -lBottom = 0 - --- | Assisting ADT for the dynamic variable ordering of the solver. --- The constructor takes references to the assignment vector and the activity --- vector of the solver. The method 'select' will return the unassigned variable --- with the highest activity. -class VarOrder o where - -- | constructor - newVarOrder :: (VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO o - newVarOrder _ _ = error "newVarOrder undefined" - - -- | Called when a new variable is created. - newVar :: o -> IO Var - newVar = error "newVar undefined" - - -- | Called when variable has increased in activity. - update :: o -> Var -> IO () - update _ = error "update undefined" - - -- | Called when all variables have been assigned new activities. - updateAll :: o -> IO () - updateAll = error "updateAll undefined" - - -- | Called when variable is unbound (may be selected again). - undo :: o -> Var -> IO () - undo _ _ = error "undo undefined" - - -- | Called to select a new, unassigned variable. - select :: o -> IO Var - select = error "select undefined" - --- | misc information on CNF -data CNFDescription = CNFDescription - { - _numberOfVariables :: !Int -- ^ number of variables - , _numberOfClauses :: !Int -- ^ number of clauses - , _pathname :: Maybe FilePath -- ^ given filename - } - deriving (Eq, Ord, Show) diff --git a/SAT/Solver/Mios/Validator.hs b/SAT/Solver/Mios/Validator.hs deleted file mode 100644 --- a/SAT/Solver/Mios/Validator.hs +++ /dev/null @@ -1,47 +0,0 @@ --- | validate an assignment -{-# LANGUAGE - ViewPatterns - #-} -{-# LANGUAGE Safe #-} -module SAT.Solver.Mios.Validator - ( - validate - ) - where - -import Data.Foldable (toList) -import SAT.Solver.Mios.Types -import SAT.Solver.Mios.Clause -import SAT.Solver.Mios.ClauseManager -import SAT.Solver.Mios.Solver - --- | validates the assignment even if the implementation of 'Solver' is wrong; we re-implement some functions here. -validate :: Traversable t => Solver -> t Int -> IO Bool -validate s (toList -> map int2lit -> lst) = do - assignment <- newVec $ 1 + nVars s - vec <- getClauseVector (clauses s) - nc <- numberOfClauses (clauses s) - let - inject :: Lit -> IO () - inject l = setNth assignment (lit2var l) $ if positiveLit l then lTrue else lFalse - -- return True if the literal is satisfied under the assignment - satisfied :: Lit -> IO Bool - satisfied l - | positiveLit l = (lTrue ==) <$> getNth assignment (lit2var l) - | otherwise = (lFalse ==) <$> getNth assignment (lit2var l) - -- return True is any literal in the given list - satAny :: [Lit] -> IO Bool - satAny [] = return False - satAny (l:ls) = do - sat' <- satisfied l - if sat' then return True else satAny ls - -- traverse all clauses in 'clauses' - loopOnVector :: Int -> IO Bool - loopOnVector ((< nc) -> False) = return True - loopOnVector i = do - c <- getNthClause vec i - sat' <- satAny =<< asList c - if sat' then loopOnVector (i + 1) else return False - if null lst - then error "validator got an empty assignment." - else mapM_ inject lst >> loopOnVector 0 diff --git a/SAT/Util/BoolExp.hs b/SAT/Util/BoolExp.hs deleted file mode 100644 --- a/SAT/Util/BoolExp.hs +++ /dev/null @@ -1,244 +0,0 @@ -{-# LANGUAGE BangPatterns, FlexibleInstances, ViewPatterns, UndecidableInstances #-} -{-# LANGUAGE Safe #-} - --- | Boolean Expression module to build CNF from arbitrary expressions --- Tseitin translation: http://en.wikipedia.org/wiki/Tseitin_transformation -module SAT.Util.BoolExp - ( - -- * Class & Type - BoolComponent (..) - , BoolForm (..) - -- * Expression contructors - , (-|-) - , (-&-) - , (-=-) - , (-!-) - , (->-) - , neg - -- * List Operation - , disjunctionOf - , (-|||-) - , conjunctionOf - , (-&&&-) - -- * Convert function - , asList - , asList_ - , asLatex - , asLatex_ - , numberOfVariables - , numberOfClauses - , tseitinBase - ) - where - -import Data.List (foldl', intercalate) - --- | the start index for the generated variables by Tseitin encoding -tseitinBase :: Int -tseitinBase = 1600000 - -data L = L Int - --- | class of objects that can be interpeted as a bool expression -class BoolComponent a where - toBF :: a -> BoolForm -- lift to BoolForm - --- | CNF expression -data BoolForm = Cnf (Int, Int) [[Int]] - deriving (Eq, Show) - -instance BoolComponent Int where - toBF a = Cnf (abs a, max tseitinBase (abs a)) [[a]] - -instance BoolComponent L where - toBF (L a) = Cnf (abs a, max tseitinBase (abs a)) [[a]] - -instance BoolComponent [Char] where - toBF (read -> a) = Cnf (abs a, max tseitinBase (abs a)) [[a]] - -instance BoolComponent BoolForm where - toBF = id - --- | returns the number of variables in the 'BoolForm' -numberOfVariables :: BoolForm -> Int -numberOfVariables (Cnf (a, b) _) = a + b - tseitinBase - --- | returns the number of clauses in the 'BoolForm' -numberOfClauses :: BoolForm -> Int -numberOfClauses (Cnf _ l) = length l - -boolFormTrue = Cnf (-1, 1) [] -boolFormFalse = Cnf (-1, -1) [] - -instance BoolComponent Bool where - toBF True = boolFormTrue - toBF False = boolFormFalse - -isTrue :: BoolForm -> Bool -isTrue = (== boolFormTrue) - -isFalse :: BoolForm -> Bool -isFalse = (== boolFormFalse) - --- | return a 'clause' list only if it contains some real clause (not a literal) -clausesOf :: BoolForm -> [[Int]] -clausesOf cnf@(Cnf _ [[]]) = [] -clausesOf cnf@(Cnf _ [[x]]) = [] -clausesOf cnf@(Cnf _ l) = l - -maxRank :: BoolForm -> Int -maxRank (Cnf (n, _) _) = n - --- | returns the number of valiable used as the output of this expression. --- and returns itself it the expression is a literal. --- Otherwise the number is a integer larger than 'tseitinBase'. --- Therefore @1 + max tseitinBase the-returned-value@ is the next literal variable for future. -tseitinNumber :: BoolForm -> Int -tseitinNumber (Cnf (m, n) [[x]]) = x -tseitinNumber (Cnf (_, n) _) = n - -renumber :: Int -> BoolForm -> (BoolForm, Int) -renumber base (Cnf (m, n) l) - | l == [] = (Cnf (m, n) l, 0) - | tseitinBase < base = (Cnf (m, n') l', n') - | otherwise = (Cnf (n', tseitinBase) l', n') - where - l' = map (map f) l - n' = maximum $ map maximum l' - offset = base - tseitinBase - 1 - f x = if abs x < tseitinBase then x else signum x * (abs x + offset) - -instance Ord BoolForm where - compare (Cnf _ a) (Cnf _ b) = compare a b - --- | disjunction constructor --- --- >>> asList $ "3" -|- "4" --- [[3,4,-5],[-3,5],[-4,5]] --- --- >>> asList (("3" -|- "4") -|- "-1") --- [[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]] --- -(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm -(toBF -> e1) -|- (toBF -> e2') - | isTrue e1 || isTrue e2' = boolFormTrue - | isFalse e1 && isFalse e2' = boolFormFalse - | isFalse e1 = e2' - | isFalse e2' = e1 - | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[a, b, - c], [- a, c], [- b, c]] - where - a = tseitinNumber e1 - (e2, b) = renumber (1 + max tseitinBase a) e2' - m = max (maxRank e1) (maxRank e2) - c = 1 + max tseitinBase (max a b) - --- | conjunction constructor --- --- >>> asList $ "3" -&- "-2" --- [[-3,2,4],[3,-4],[-2,-4]] --- --- >>> asList $ "3" -|- ("1" -&- "2") --- [[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]] --- -(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm -(toBF -> e1) -&- (toBF -> e2') - | isTrue e1 && isTrue e2' = boolFormTrue - | isFalse e1 || isFalse e2' = boolFormFalse - | isTrue e1 = e2' - | isTrue e2' = e1 - | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[- a, - b, c], [a, - c], [b, - c]] - where - a = tseitinNumber e1 - (e2, b) = renumber (1 + max tseitinBase a) e2' - m = max (maxRank e1) (maxRank e2) - c = 1 + max tseitinBase (max a b) - --- | negate a form --- --- >>> asList $ neg ("1" -|- "2") --- [[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]] -neg :: (BoolComponent a) => a -> BoolForm -neg (toBF -> e) = - Cnf (m, c) $ clausesOf e ++ [[- a, - c], [a, c]] - where - a = tseitinNumber e - m = maxRank e - c = 1 + max tseitinBase a - --- | equal on BoolForm -(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm -(toBF -> e1) -=- (toBF -> e2) = (e1 -&- e2) -|- (neg e1 -&- neg e2) - --- | negation on BoolForm -(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm -(toBF -> e1) -!- (toBF -> e2) = (neg e1 -&- e2) -|- (e1 -&- neg e2) - --- | implication as a short cut --- --- >>> asList ("1" ->- "2") --- [[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]] -(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm -(toBF -> a) ->- (toBF -> b) = (neg a) -|- b - --- | merge [BoolForm] by '(-|-)' -disjunctionOf :: [BoolForm] -> BoolForm -disjunctionOf [] = boolFormFalse -disjunctionOf (x:l) = foldl' (-|-) x l - --- | an alias of 'disjunctionOf' -(-|||-) = disjunctionOf - --- | merge [BoolForm] by '(-&-)' -conjunctionOf :: [BoolForm] -> BoolForm -conjunctionOf [] = boolFormTrue -conjunctionOf (x:l) = foldl' (-&-) x l - --- | an alias of 'conjunctionOf' -(-&&&-) = conjunctionOf - --- | converts a BoolForm to "[[Int]]" -asList_ :: BoolForm -> [[Int]] -asList_ cnf@(Cnf (m,_) _) - | isTrue cnf = [] - | isFalse cnf = [[]] - | otherwise = l' - where - (Cnf _ l', _) = renumber (m + 1) cnf - --- | converts a *satisfied* BoolForm to "[[Int]]" -asList :: BoolForm -> [[Int]] -asList cnf@(Cnf (m,n) l) - | isTrue cnf = [] - | isFalse cnf = [[]] - | n <= tseitinBase = l - | otherwise = [m'] : l' - where - (Cnf (m', _) l', _) = renumber (m + 1) cnf - --- | make latex string from CNF, using 'asList_' --- --- >>> asLatex $ "3" -|- "4" --- "\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n" --- -asLatex_ :: BoolForm -> String -asLatex_ b = beg ++ s ++ end - where - beg = "\\begin{displaymath}\n" - end = "\n\\end{displaymath}\n" - s = intercalate " \\wedge " [ makeClause c | c <- asList_ b] - makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")" - makeLiteral l - | 0 < l = " x_{" ++ show l ++ "} " - | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} " - --- | make latex string from CNF, using 'asList' -asLatex :: BoolForm -> String -asLatex b = beg ++ s ++ end - where - beg = "\\begin{displaymath}\n" - end = "\n\\end{displaymath}\n" - s = intercalate " \\wedge " [ makeClause c | c <- asList b] - makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")" - makeLiteral l - | 0 < l = " x_{" ++ show l ++ "} " - | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} " diff --git a/SAT/Util/CNFIO.hs b/SAT/Util/CNFIO.hs deleted file mode 100644 --- a/SAT/Util/CNFIO.hs +++ /dev/null @@ -1,31 +0,0 @@ -{-# LANGUAGE Safe #-} - --- | Read/Write a CNF file only with ghc standard libraries -module SAT.Util.CNFIO - ( - -- * Input - fromFile - , clauseListFromFile - , fromMinisatOutput - , clauseListFromMinisatOutput - -- * Output - , toFile - , toCNFString - , asCNFString - , asCNFString_ - -- * Bool Operation - , module SAT.Util.BoolExp - ) - where -import SAT.Util.CNFIO.Reader -import SAT.Util.CNFIO.Writer -import SAT.Util.CNFIO.MinisatReader -import SAT.Util.BoolExp - --- | String from BoolFrom -asCNFString :: BoolForm -> String -asCNFString = toCNFString . asList - --- | String from BoolFrom -asCNFString_ :: BoolForm -> String -asCNFString_ = toCNFString . asList_ diff --git a/SAT/Util/CNFIO/MinisatReader.hs b/SAT/Util/CNFIO/MinisatReader.hs deleted file mode 100644 --- a/SAT/Util/CNFIO/MinisatReader.hs +++ /dev/null @@ -1,73 +0,0 @@ -{-# LANGUAGE Safe #-} - --- | Read an output file of minisat -module SAT.Util.CNFIO.MinisatReader - ( - -- * Interface - fromMinisatOutput - , clauseListFromMinisatOutput - ) - where --- import Control.Applicative ((<$>), (<*>), (<*), (*>)) -import Data.Char -import Text.ParserCombinators.ReadP - --- parser --- |parse a non-signed integer -{-# INLINE pint #-} -pint = do - n <- munch isDigit - return (read n :: Int) - -{-# INLINE mint #-} -mint = do - char '-' - n <- munch isDigit - return (- (read n::Int)) - --- |parse a (signed) integer -{-# INLINE int #-} -int = mint <++ pint - --- |return integer list that terminates at zero -{-# INLINE seqNums #-} -seqNums = do - skipSpaces - x <- int - skipSpaces - if (x == 0) then return [] else (x :) <$> seqNums - --- |top level interface for parsing CNF -{-# INLINE parseMinisatOutput #-} -parseMinisatOutput :: ReadP ((Int, Int), [Int]) -parseMinisatOutput = do - string "SAT" - skipSpaces - l <- seqNums - return ((length l,0), l) - --- |read a minisat output: --- ((numbefOfVariables, 0), [Literal]) --- --- >>> fromFile "result" --- ((3, 0), [1, -2, 3]) --- -{-# INLINE fromMinisatOutput #-} -fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int])) -fromMinisatOutput f = do - c <- readFile f - case readP_to_S parseMinisatOutput c of - [(a, _)] -> return $ Just a - _ -> return Nothing - --- | return clauses as [[Int]] from 'file' --- --- >>> clauseListFromMinisatOutput "result" --- [1,-2,3] --- -clauseListFromMinisatOutput :: FilePath -> IO [Int] -clauseListFromMinisatOutput l = do - res <- fromMinisatOutput l - case res of - Just p -> return (snd p) - _ -> return [] diff --git a/SAT/Util/CNFIO/Reader.hs b/SAT/Util/CNFIO/Reader.hs deleted file mode 100644 --- a/SAT/Util/CNFIO/Reader.hs +++ /dev/null @@ -1,130 +0,0 @@ -{-# LANGUAGE Safe #-} - --- | Read a CNF file without haskell-platform -module SAT.Util.CNFIO.Reader - ( - -- * Interface - fromFile - , clauseListFromFile - ) - where -import Control.Applicative ((<$>), (<*>), (<*), (*>)) -import Data.Char -import Text.ParserCombinators.ReadP - --- parser -{-# INLINE newline #-} -newline = char '\n' - -{-# INLINE digit #-} -digit = satisfy isDigit - -{-# INLINE spaces #-} -spaces = munch (`elem` " \t") - -{-# INLINE noneOf #-} -noneOf s = satisfy (`notElem` s) - --- |parse a non-signed integer -{-# INLINE pint #-} -pint = do - n <- munch isDigit - return (read n :: Int) - -{-# INLINE mint #-} -mint = do - char '-' - n <- munch isDigit - return (- (read n::Int)) - --- |parse a (signed) integer -{-# INLINE int #-} -int = mint <++ pint - --- |Parse something like: p FORMAT VARIABLES CLAUSES -{-# INLINE problemLine #-} -problemLine = do - char 'p' - skipSpaces - (string "cnf" <++ string "CNF") - skipSpaces - vars <- pint - skipSpaces - clas <- pint - spaces - newline - return (vars, clas) - --- |Parse something like: c This in an example of a comment line. -{-# INLINE commentLines #-} -commentLines = do - l <- look - if (head l) == 'c' - then do - munch ('\n' /=) - newline - commentLines - else return () - -_commentLines = do - char 'c' - munch ('\n' /=) - newline - l <- look - if (head l) == 'c' then commentLines else return () - --- |Parse the preamble part -{-# INLINE preambleCNF #-} -preambleCNF = do - commentLines - problemLine - --- |return integer list that terminates at zero -{-# INLINE seqNums #-} -seqNums = do - skipSpaces - x <- int - skipSpaces - if (x == 0) then return [] else (x :) <$> seqNums - --- |Parse something like: 1 -2 0 4 0 -3 0 -{-# INLINE parseClauses #-} -parseClauses :: Int -> ReadP [[Int]] -parseClauses n = count n seqNums - --- |top level interface for parsing CNF -{-# INLINE parseCNF #-} -parseCNF :: ReadP ((Int, Int), [[Int]]) -parseCNF = do - a <- preambleCNF - b <- parseClauses (snd a) - return (a, b) - --- |driver:: String -> Either ParseError Int -driver input = readP_to_S (parseClauses 1) input - --- |read a CNF file and return: --- ((numbefOfVariables, numberOfClauses), [Literal]) --- --- >>> fromFile "acnf" --- ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]] --- -{-# INLINE fromFile #-} -fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]])) -fromFile f = do - c <- readFile f - case readP_to_S parseCNF c of - [(a, _)] -> return $ Just a - _ -> return Nothing - --- | return clauses as [[Int]] from 'file' --- --- >>> clauseListFromFile "a.cnf" --- [[1, 2], [-2, 3], [-1, 2, -3], [3]] --- -clauseListFromFile :: FilePath -> IO [[Int]] -clauseListFromFile l = do - res <- fromFile l - case res of - Just (_, l) -> return l - _ -> return [] diff --git a/SAT/Util/CNFIO/Writer.hs b/SAT/Util/CNFIO/Writer.hs deleted file mode 100644 --- a/SAT/Util/CNFIO/Writer.hs +++ /dev/null @@ -1,58 +0,0 @@ -{-# LANGUAGE Safe #-} - --- | Write SAT data to CNF file -module SAT.Util.CNFIO.Writer - ( - -- * Interface - toFile - , toCNFString - , toString - , toLatexString - ) - where -import Data.List (intercalate, nub, sort) -import System.IO - --- | Write the CNF to file 'f', using 'toCNFString' -toFile :: FilePath -> [[Int]] -> IO () -toFile f l = writeFile f $ toCNFString l - --- | Convert [Clause] to String, where Clause is [Int] --- --- >>> toCNFString [] --- "p cnf 0 0\n" --- --- >>> toCNFString [[-1, 2], [-3, -4]] --- "p cnf 4 2\n-1 2 0\n-3 -4 0\n" --- --- >>> toCNFString [[1], [-2], [-3, -4], [1,2,3,4]] --- "p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n" --- -toCNFString :: [[Int]] -> String -toCNFString l = hdr ++ str - where - hdr = "p cnf " ++ show numV ++ " " ++ show numC ++ "\n" - numC = length l - numV = last $ nub $ sort $ map abs $ concat l - str = concat [intercalate " " (map show c) ++ " 0\n" | c <- l] - --- | converts @[[Int]]@ to a String -toString :: [[Int]] -> String -> String -> String -toString l and' or' = intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] - where - lit x - | 0 <= x = "X" ++ show x - | otherwise = "-X" ++ show (abs x) - a = pad and' - o = pad or' - pad s = " " ++ s ++ " " - --- | converts @[[Int]]@ to a LaTeX expression -toLatexString :: [[Int]] -> String -toLatexString l = "\\begin{eqnarray*}\n" ++ intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] ++ "\n\\end{eqnarray*}" - where - lit x - | 0 <= x = "X_{" ++ show x ++ "}" - | otherwise = "\\overline{X_{" ++ show (abs x) ++ "}}" - a = " \n\\wedge " - o = " \\vee " diff --git a/app/mios.hs b/app/mios.hs --- a/app/mios.hs +++ b/app/mios.hs @@ -5,7 +5,7 @@ ) where -import SAT.Solver.Mios +import SAT.Mios -- | main main :: IO () diff --git a/mios.cabal b/mios.cabal --- a/mios.cabal +++ b/mios.cabal @@ -2,14 +2,14 @@ -- see http://haskell.org/cabal/users-guide/ name: mios -version: 1.2.1 +version: 1.3.0 synopsis: A Minisat-based SAT solver in Haskell description: A modern and fast SAT solver written in Haskell, based on Minisat-1.14 and 2.2. - By using CDCL, watch literals, VSIDS, restart, blocking-literals, LBD and so on, - the current version is only 1.8 time slower than Minisat-1.14. - "Mios" is an abbreviation of /Minisat-based Implementation and Optimization Study on SAT solver/. + By using CDCL, watch literals, VSIDS, restart, blocking-literals, LBD and so on. + The current version is only 2.0 time slower than Minisat-2.2. + 'Mios' is an abbreviation of 'Minisat-based Implementation and Optimization Study on SAT solver'. . homepage: https://github.com/shnarazk/mios @@ -17,7 +17,7 @@ license-file: LICENSE author: Shuji Narazaki maintainer: Shuji Narazaki -category: Artificial Intelligence, Constraint Solver +category: Artificial Intelligence, Constraints build-type: Simple cabal-version: >=1.16 @@ -25,36 +25,43 @@ Description: Compile with llvm Default: False +Flag lib + Description: Build the solver library + Default: True + library - buildable: True + if flag(lib) + buildable: True + else + buildable: False default-language: Haskell2010 default-extensions: Strict exposed-modules: - SAT.Solver.Mios - SAT.Solver.Mios.Clause - SAT.Solver.Mios.ClauseManager - SAT.Solver.Mios.Data.VecBool - SAT.Solver.Mios.Data.VecDouble - SAT.Solver.Mios.Data.Vec - SAT.Solver.Mios.Data.Singleton - SAT.Solver.Mios.Data.Stack - SAT.Solver.Mios.Internal - SAT.Solver.Mios.Glucose - SAT.Solver.Mios.M114 - SAT.Solver.Mios.OptionParser - SAT.Solver.Mios.Solver - SAT.Solver.Mios.Types - SAT.Solver.Mios.Validator - SAT.Util.CNFIO - SAT.Util.CNFIO.MinisatReader - SAT.Util.CNFIO.Reader - SAT.Util.CNFIO.Writer - SAT.Util.BoolExp + SAT.Mios + SAT.Mios.Clause + SAT.Mios.ClauseManager + SAT.Mios.Data.VecBool + SAT.Mios.Data.VecDouble + SAT.Mios.Data.Vec + SAT.Mios.Data.Singleton + SAT.Mios.Data.Stack + SAT.Mios.Internal + SAT.Mios.Main + SAT.Mios.OptionParser +-- SAT.Mios.Ranking + SAT.Mios.Solver + SAT.Mios.Types + SAT.Mios.Validator + SAT.Mios.Util.CNFIO + SAT.Mios.Util.CNFIO.MinisatReader + SAT.Mios.Util.CNFIO.Reader + SAT.Mios.Util.CNFIO.Writer + SAT.Mios.Util.BoolExp build-depends: base ==4.9.*, vector >=0.11, containers >=0.5, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6 if flag(llvm) - ghc-options: -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3 + ghc-options: -O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3 else - ghc-options: -ignore-asserts -funbox-strict-fields -msse4.2 + ghc-options: -O2 -ignore-asserts -funbox-strict-fields -msse4.2 executable mios main-is: app/mios.hs @@ -63,27 +70,27 @@ default-extensions: Strict build-depends: base ==4.9.*, vector >=0.11, containers >=0.5, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6 if flag(llvm) - ghc-options: -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3 + ghc-options: -O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3 else - ghc-options: -ignore-asserts -funbox-strict-fields -msse4.2 + ghc-options: -O2 -ignore-asserts -funbox-strict-fields -msse4.2 other-modules: - SAT.Solver.Mios - SAT.Solver.Mios.Clause - SAT.Solver.Mios.ClauseManager - SAT.Solver.Mios.Data.VecBool - SAT.Solver.Mios.Data.VecDouble - SAT.Solver.Mios.Data.Vec - SAT.Solver.Mios.Data.Singleton - SAT.Solver.Mios.Data.Stack - SAT.Solver.Mios.Internal - SAT.Solver.Mios.Glucose - SAT.Solver.Mios.M114 - SAT.Solver.Mios.OptionParser - SAT.Solver.Mios.Solver - SAT.Solver.Mios.Types - SAT.Solver.Mios.Validator - SAT.Util.CNFIO - SAT.Util.CNFIO.MinisatReader - SAT.Util.CNFIO.Reader - SAT.Util.CNFIO.Writer - SAT.Util.BoolExp + SAT.Mios + SAT.Mios.Clause + SAT.Mios.ClauseManager + SAT.Mios.Data.VecBool + SAT.Mios.Data.VecDouble + SAT.Mios.Data.Vec + SAT.Mios.Data.Singleton + SAT.Mios.Data.Stack + SAT.Mios.Internal + SAT.Mios.Main + SAT.Mios.OptionParser +-- SAT.Mios.Ranking + SAT.Mios.Solver + SAT.Mios.Types + SAT.Mios.Validator + SAT.Mios.Util.CNFIO + SAT.Mios.Util.CNFIO.MinisatReader + SAT.Mios.Util.CNFIO.Reader + SAT.Mios.Util.CNFIO.Writer + SAT.Mios.Util.BoolExp