diff --git a/MultiConflict/utils/averagecsv.hs b/MultiConflict/utils/averagecsv.hs new file mode 100644 --- /dev/null +++ b/MultiConflict/utils/averagecsv.hs @@ -0,0 +1,13 @@ +-- | Usage: +-- > mios-averagecsv < a.csv > ave.csv +module Main where + +import Data.List (sort) +import SAT.Mios.Util.Stat + +main :: IO () +main = do + putStrLn $ fst (header :: (String, MergedDump)) + d <- parseBy [(fst (header :: (String, MiosDump)), fromCSV)] <$> getContents + mapM_ (putStrLn . toCSV) . sort =<< merge d + diff --git a/MultiConflict/utils/dump2csv.hs b/MultiConflict/utils/dump2csv.hs new file mode 100644 --- /dev/null +++ b/MultiConflict/utils/dump2csv.hs @@ -0,0 +1,10 @@ +-- | Usage: +-- > mios --dump ... | mios-dump2csv > a.csv +module Main where + +import SAT.Mios.Util.Stat + +main :: IO () +main = do + putStrLn $ fst (header :: (String, MiosDump)) + mapM_ (putStrLn . toCSV) =<< parseBy [("", fromDump)] <$> getContents diff --git a/MultiConflict/utils/numbers.hs b/MultiConflict/utils/numbers.hs new file mode 100644 --- /dev/null +++ b/MultiConflict/utils/numbers.hs @@ -0,0 +1,119 @@ +-- | Usage: +-- > mios-summary < average.csv > summary.tbl (for org-mode or github-flavored markdown) +{-# LANGUAGE ViewPatterns #-} +module Main where + +import Data.List (intercalate, lookup, minimumBy, nub) +import Data.Maybe (fromMaybe) +import Data.Ord (comparing) +import Numeric (showFFloat) +import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo) +import System.Environment (getArgs) +import SAT.Mios.Types +import SAT.Mios.Util.Stat + +data Opt = Opt + { + threshold :: Double + , p1 :: (Double, Double) + , p2 :: (Double, Double) + , p3 :: (Int, Int) + , p4 :: (Int, Int) + , message :: String + , help :: Bool + } + +optDefault :: Opt +optDefault = Opt 0 (0, 10) (0, 10) (0, 10) (0, 10) "#-*-mode:org-*-" False + +options ::[OptDescr (Opt -> Opt)] +options = + [ + Option ['t'] ["threshold"] + (ReqArg (\v c -> c { threshold = read v }) "0.0") "threshold for p1" + , Option [] ["UF250"] + (NoArg (\c -> c { threshold = 12109075.01 })) "threshold for UF250; 12109075.01 (7.083)" + , Option [] ["38bits"] + (NoArg (\c -> c { threshold = 191761341.00 })) "threshold for 38bits; 191761341.00 (8.283)" + , Option [] ["44bits"] + (NoArg (\c -> c { threshold = 5204447789.00 })) "threshold for 44bits; 5204447789.00 (9.716)" + , Option ['1'] ["p1"] + (ReqArg (\v c -> c { p1 = read v }) "\"(0,10)\"") "range of p1" + , Option ['2'] ["p2"] + (ReqArg (\v c -> c { p2 = read v }) "\"(0,10)\"") "range of p2" + , Option ['3'] ["p3"] + (ReqArg (\v c -> c { p3 = read v }) "\"(0,10)\"") "range of p3" + , Option ['4'] ["p4"] + (ReqArg (\v c -> c { p4 = read v }) "\"(0,10)\"") "range of p4" + , Option ['m'] ["message"] + (ReqArg (\v c -> c { message = undecodeNewline v }) "\"\"") "extra message embeded into output" + , Option ['h'] ["help"] + (NoArg (\c -> c { help = True })) "display help message" + ] + +parseOptions :: String -> [String] -> IO Opt +parseOptions mes argv = + case getOpt Permute options argv of + (o, [], []) -> return $ foldl (flip id) optDefault o + (o, _, []) -> return $ foldl (flip id) optDefault o + (_, _, err) -> ioError (userError (concat err ++ usageInfo mes options)) + +-- | builds "MiosProgramOption" from a String +parseOptionsFromArgs :: String -> IO Opt +parseOptionsFromArgs mes = parseOptions mes =<< getArgs + +undecodeNewline :: String -> String +undecodeNewline [] = [] +undecodeNewline [a] = [a] +undecodeNewline ('\\' : 'n' : x) = '\n' : undecodeNewline x +undecodeNewline (a : x) = a : undecodeNewline x + +showf :: Double -> String +showf x = showFFloat (Just 2) x "" + +main :: IO () +main = do + opts <- parseOptionsFromArgs "gp-summary" + if help opts + then putStrLn $ usageInfo "" options + else do putStrLn $ message opts + putStrLn "" + putStrLn "| p1 | good | bad |" + putStrLn "| ---- | ---- | --- |" + result <- pickup opts . parseBy [(fst (header :: (String, MergedDump)), fromMergedCSV)] <$> getContents + mapM_ (putStrLn . toString) result + let ngs = sum $ map (fst . snd) result + nbs = sum $ map (snd . snd) result + putStrLn $ intercalate "," [showf (fromIntegral ngs / fromIntegral (ngs + nbs)), show (ngs + nbs) ++ "/" ++ show (ngs, nbs)] + +toString :: (Double, (Int, Int)) -> String +toString (p1, (ng, nb)) = "| " ++ intercalate " | " [showf p1, show ng, show nb] ++ " |" + +pickup :: Opt -> [MergedDump] -> [(Double, (Int, Int))] +pickup opts l = filter notEmpty $ map gather keys + where + notEmpty (_, (0, 0)) = False + notEmpty _ = True + thr = threshold opts + keys = nub $ map (gpParameter1 . snd. _mergedConf) l + gather :: Double -> (Double, (Int, Int)) + gather key = (key, (ng, length targets - ng)) + where + targets' :: [MergedDump] + targets' = filter ((key ==) . gpParameter1 . snd. _mergedConf) l + inBand :: MergedDump -> Bool + inBand (_mergedConf -> snd -> conf) = c1 && c2 && c3 && c4 + where + c1 = inPair (p1 opts) (gpParameter1 conf) + c2 = inPair (p2 opts) (gpParameter2 conf) + c3 = inPair (p3 opts) (extraParameter3 conf) + c4 = inPair (p4 opts) (extraParameter4 conf) + inPair :: (Num a, Ord a) => (a, a) -> a -> Bool + inPair (b, t) x = b <= x && x <= t + targets = filter inBand targets' + ng = length $ filter (< thr) (map value targets) + value :: MergedDump -> Double + value m = case lookup PropagationS . (\(MiosStats s) -> s) . _mergedStat $ m of + Just (Right v) -> fromIntegral v + Just (Left v) -> v + Nothing -> 10000000 diff --git a/MultiConflict/utils/pickup.hs b/MultiConflict/utils/pickup.hs new file mode 100644 --- /dev/null +++ b/MultiConflict/utils/pickup.hs @@ -0,0 +1,123 @@ +-- | Usage: +-- > mios-summary < average.csv > summary.tbl (for org-mode or github-flavored markdown) +module Main where + +import Data.List (intercalate, lookup, maximumBy, minimumBy, nub) +import Data.Maybe (fromMaybe) +import Data.Ord (comparing) +import Numeric (showFFloat) +import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo) +import System.Environment (getArgs) +import SAT.Mios.Types +import SAT.Mios.Util.Stat + +data Opt = Opt + { + message :: String + , useLog :: Bool + , help :: Bool + } + +optDefault :: Opt +optDefault = Opt "#-*-mode:org-*-" False False + +options ::[OptDescr (Opt -> Opt)] +options = + [ + Option ['m'] ["message"] + (ReqArg (\v c -> c { message = undecodeNewline v }) "\"string\"") "extra message embeded into output" + , Option ['l'] ["useLog"] + (NoArg (\c -> c { useLog = True })) "use Logarithmic value for propagation" + , Option ['h'] ["help"] + (NoArg (\c -> c { help = True })) "display help message" + ] + +parseOptions :: String -> [String] -> IO Opt +parseOptions mes argv = + case getOpt Permute options argv of + (o, [], []) -> return $ foldl (flip id) optDefault o + (o, _, []) -> return $ foldl (flip id) optDefault o + (_, _, err) -> ioError (userError (concat err ++ usageInfo mes options)) + +-- | builds "MiosProgramOption" from a String +parseOptionsFromArgs :: String -> IO Opt +parseOptionsFromArgs mes = parseOptions mes =<< getArgs + +undecodeNewline :: String -> String +undecodeNewline [] = [] +undecodeNewline [a] = [a] +undecodeNewline ('\\' : 'n' : x) = '\n' : undecodeNewline x +undecodeNewline (a : x) = a : undecodeNewline x + +showf :: Double -> String +showf x = showFFloat (Just 2) x "" + +showi :: Int -> String +showi x + | 3 <= length s = s + | otherwise = reverse . take 3 . (++ " ") . reverse $ s + where s = show x + +showl :: Either Double Int -> String +showl (Left x) = showf x +showl (Right x) = showf (fromIntegral x) + +main :: IO () +main = do + opts <- parseOptionsFromArgs "gp-summary" + if help opts + then putStrLn $ usageInfo "" options + else do let parsers = [ (fst (header :: (String, MiosDump)), toMerge <$> fromCSV) + , (fst (header :: (String, MergedDump)), fromMergedCSV)] + putStrLn $ message opts + putStrLn "" + if useLog opts + then do putStrLn "| n | p1 | p2 | p3 | p4 | log(P) | conflict | learnt | backjump | re-st | rate | extra | pr/bj |" + putStrLn "| --- | ---- | ---- | --- | --- | ------ | -------- | -------- | -------- | ----- | ---- | ----- | ----- |" + else do putStrLn "| n | p1 | p2 | p3 | p4 | propagation | conflict | learnt | backjump | re-st | rate | extra | pr/bj |" + putStrLn "| --- | ---- | ---- | --- | --- | ----------- | -------- | -------- | -------- | ----- | ---- | ----- | ----- |" + d <- parseBy parsers <$> getContents + mapM_ (putStrLn . toSummary (useLog opts)) $ pickup True d + putStrLn "" + mapM_ (putStrLn . toSummary (useLog opts)) $ pickup False d + putStrLn "" + +toSummary :: Bool -> MergedDump -> String +toSummary uLog (MergedDump (_, MiosConfiguration _ _ p1 p2 p3 p4) n (MiosStats l) _) = + "| " ++ intercalate " | " [show n, m', s', showf pr] ++ " |" + where + m' = intercalate " | " [showf p1, showf p2, showi p3, showi p4] + s' = intercalate " | " $ map (showl . snd) (convert uLog l) -- (tail . init $ l) + convert :: Bool -> [DumpedValue] -> [DumpedValue] + convert uL ks + | uL = logOf PropagationS : map valOf [ConflictS .. ExtraS] + | otherwise = map valOf [PropagationS .. ExtraS] + where + logOf :: DumpTag -> DumpedValue + logOf key = (key, Left $ logBase 10 (val key)) + valOf key = (key, Left $ val key) + val :: DumpTag -> Double + val key + | Just (Left x) <- lookup key ks = x + | Just (Right x) <- lookup key ks = fromIntegral x + | otherwise = 0 + pr = fromMaybe 0 $ div' <$> lookup PropagationS l <*> lookup BackjumpS l + div' :: Either Double Int -> Either Double Int -> Double + div' (Right a) (Right b) = fromIntegral a / fromIntegral b + div' (Right a) (Left b) = fromIntegral a / b + div' (Left a) (Right b) = a / fromIntegral b + div' (Left a) (Left b) = a / b + +pickup :: Bool -> [MergedDump] -> [MergedDump] +pickup good l = map selectData keys + where + keys = nub $ map (gpParameter1 . snd. _mergedConf) l + selectData :: Double -> MergedDump + selectData key + | good = minimumBy (comparing value) $ filter ((key ==) . gpParameter1 . snd. _mergedConf) l + | otherwise = maximumBy (comparing value) $ filter ((key ==) . gpParameter1 . snd. _mergedConf) l + value :: MergedDump -> Double + value m = case lookup PropagationS . (\(MiosStats s) -> s) . _mergedStat $ m of + Just (Right v) -> fromIntegral v + Just (Left v) -> v + Nothing -> 10000000 diff --git a/MultiConflict/utils/stat2csv.hs b/MultiConflict/utils/stat2csv.hs new file mode 100644 --- /dev/null +++ b/MultiConflict/utils/stat2csv.hs @@ -0,0 +1,10 @@ +-- | Usage: +-- > mios --stat -X ... | mios-stat2csv > a.csv +module Main where + +import SAT.Mios.Util.Stat + +main :: IO () +main = do + putStrLn $ fst (header :: (String, MiosDump)) + mapM_ (putStrLn . toCSV) =<< parseBy [("", fromStat)] <$> getContents diff --git a/MultiConflict/utils/summary.hs b/MultiConflict/utils/summary.hs new file mode 100644 --- /dev/null +++ b/MultiConflict/utils/summary.hs @@ -0,0 +1,104 @@ +-- | Usage: +-- > mios-summary < average.csv > summary.tbl (for org-mode or github-flavored markdown) +module Main where + +import Data.List (intercalate, lookup) +import Data.Maybe (fromMaybe) +import Numeric (showFFloat) +import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo) +import System.Environment (getArgs) +import SAT.Mios.Types +import SAT.Mios.Util.Stat + +data Opt = Opt + { + message :: String + , useLog :: Bool + , help :: Bool + } + +optDefault :: Opt +optDefault = Opt "#-*-mode:org-*-" False False + +options ::[OptDescr (Opt -> Opt)] +options = + [ + Option ['m'] ["message"] + (ReqArg (\v c -> c { message = undecodeNewline v }) "\"string\"") "extra message embeded into output" + , Option ['l'] ["useLog"] + (NoArg (\c -> c { useLog = True })) "use Logarithmic value for propagation" + , Option ['h'] ["help"] + (NoArg (\c -> c { help = True })) "display help message" + ] + +parseOptions :: String -> [String] -> IO Opt +parseOptions mes argv = + case getOpt Permute options argv of + (o, [], []) -> return $ foldl (flip id) optDefault o + (o, _, []) -> return $ foldl (flip id) optDefault o + (_, _, err) -> ioError (userError (concat err ++ usageInfo mes options)) + +-- | builds "MiosProgramOption" from a String +parseOptionsFromArgs :: String -> IO Opt +parseOptionsFromArgs mes = parseOptions mes =<< getArgs + +undecodeNewline :: String -> String +undecodeNewline [] = [] +undecodeNewline [a] = [a] +undecodeNewline ('\\' : 'n' : x) = '\n' : undecodeNewline x +undecodeNewline (a : x) = a : undecodeNewline x + +showf :: Double -> String +showf x = showFFloat (Just 2) x "" + +showi :: Int -> String +showi x + | 3 <= length s = s + | otherwise = reverse . take 3 . (++ " ") . reverse $ s + where s = show x + +showl :: Either Double Int -> String +showl (Left x) = showf x +showl (Right x) = showf (fromIntegral x) + +main :: IO () +main = do + opts <- parseOptionsFromArgs "gp-summary" + if help opts + then putStrLn $ usageInfo "" options + else do let parsers = [ (fst (header :: (String, MiosDump)), toMerge <$> fromCSV) + , (fst (header :: (String, MergedDump)), fromMergedCSV)] + putStrLn $ message opts + putStrLn "" + if useLog opts + then do putStrLn "| n | p1 | p2 | p3 | p4 | log(P) | conflict | learnt | backjump | re-st | rate | extra | pr/bj |" + putStrLn "| --- | ---- | ---- | --- | --- | ------ | -------- | -------- | -------- | ----- | ---- | ----- | ----- |" + else do putStrLn "| n | p1 | p2 | p3 | p4 | propagation | conflict | learnt | backjump | re-st | rate | extra | pr/bj |" + putStrLn "| --- | ---- | ---- | --- | --- | ----------- | -------- | -------- | -------- | ----- | ---- | ----- | ----- |" + mapM_ (putStrLn . toSummary (useLog opts)) . parseBy parsers =<< getContents + +toSummary :: Bool -> MergedDump -> String +toSummary uLog (MergedDump (_, MiosConfiguration _ _ p1 p2 p3 p4) n (MiosStats l) _) = + "| " ++ intercalate " | " [show n, m', s', showf pr] ++ " |" + where + m' = intercalate " | " [showf p1, showf p2, showi p3, showi p4] + s' = intercalate " | " $ map (showl . snd) (convert uLog l) -- (tail . init $ l) + convert :: Bool -> [DumpedValue] -> [DumpedValue] + convert uL ks + | uL = logOf PropagationS : map valOf [ConflictS .. ExtraS] + | otherwise = map valOf [PropagationS .. ExtraS] + where + logOf :: DumpTag -> DumpedValue + logOf key = (key, Left $ logBase 10 (val key)) + valOf key = (key, Left $ val key) + val :: DumpTag -> Double + val key + | Just (Left x) <- lookup key ks = x + | Just (Right x) <- lookup key ks = fromIntegral x + | otherwise = 0 + pr = fromMaybe 0 $ div' <$> lookup PropagationS l <*> lookup BackjumpS l + div' :: Either Double Int -> Either Double Int -> Double + div' (Right a) (Right b) = fromIntegral a / fromIntegral b + div' (Right a) (Left b) = fromIntegral a / b + div' (Left a) (Right b) = a / fromIntegral b + div' (Left a) (Left b) = a / b diff --git a/SAT/Mios.hs b/SAT/Mios.hs deleted file mode 100644 --- a/SAT/Mios.hs +++ /dev/null @@ -1,293 +0,0 @@ -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE Safe #-} - --- | Minisat-based Implementation and Optimization Study on SAT solver -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.Solver -import SAT.Mios.Main -import SAT.Mios.OptionParser -import SAT.Mios.Validator - --- | version name -versionId :: String -versionId = "mios 1.4.0 -- https://github.com/shnarazk/mios" - -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`) <=< (newStackFromList . map int2lit)) c - noConf <- simplifyDB s - if noConf - then do - x <- solve s [] - if x - then Right <$> getModel s - else Left . map lit2int <$> asList (conflicts 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`) <=< (newStackFromList . 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`) <=< (newStackFromList . 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 -> 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) 0 - polvec <- newVec (maxLit + 1) 0 - 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 <- getNth polvec $ var2lit v True - n <- getNth polvec $ var2lit v False - when (p == lFalse || n == lFalse) $ setNth asg v p - 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 -> Stack -> Vec Int -> B.ByteString -> IO B.ByteString -readClause s buffer bvec 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 - void $ addClause s buffer - return b' - else do - let l = int2lit k - setNth buffer i l - setNth bvec l lTrue - loop (i + 1) b' - loop 1 . skipComments . skipWhitespace $ stream - -showPath :: FilePath -> String -showPath str = replicate (len - length basename) ' ' ++ if elem '/' str then basename else 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 deleted file mode 100644 --- a/SAT/Mios/Clause.hs +++ /dev/null @@ -1,145 +0,0 @@ -{-# LANGUAGE - BangPatterns - , FlexibleInstances - , MagicHash - , MultiParamTypeClasses - , RecordWildCards - , ViewPatterns - #-} -{-# LANGUAGE Trustworthy #-} - --- | Clause, supporting pointer-based equality -module SAT.Mios.Clause - ( - Clause (..) --- , isLit --- , getLit - , newClauseFromStack - -- * Vector of Clause - , ClauseVector - , newClauseVector - ) - where - -import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#) -import qualified Data.Vector as V -import qualified Data.Vector.Mutable as MV --- import Data.List (intercalate) -import SAT.Mios.Types - --- | __Fig. 7.(p.11)__ --- normal, null (and binary) clause. --- This matches both of @Clause@ and @GClause@ in MiniSat. -data Clause = Clause - { - learnt :: !Bool -- ^ whether this is a learnt clause --- , rank :: !Int' -- ^ goodness like LBD; computed in 'Ranking' - , activity :: !Double' -- ^ activity of this clause - , protected :: !Bool' -- ^ protected from reduce - , lits :: !Stack -- ^ 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" - --- | 'Clause' is a 'VecFamily' of 'Lit'. -instance VecFamily Clause Lit where - {-# SPECIALIZE INLINE getNth :: Clause -> Int -> IO Int #-} - getNth Clause{..} n = error "no getNth for Clause" - {-# SPECIALIZE INLINE setNth :: Clause -> Int -> Int -> IO () #-} - setNth Clause{..} n x = error "no setNth for Clause" - -- | returns a vector of literals in it. - {-# SPECIALIZE INLINE asUVector :: Clause -> UVector Int #-} - asUVector = asUVector . lits - asList NullClause = return [] - asList Clause{..} = take <$> get' lits <*> asList lits - -- dump mes NullClause = return $ mes ++ "Null" - -- dump mes Clause{..} = return $ mes ++ "a clause" -{- - dump mes Clause{..} = do - a <- show <$> get' activity - n <- get' lits - l <- asList lits - return $ mes ++ "C" ++ show n ++ "{" ++ intercalate "," [show learnt, a, show (map lit2int l)] ++ "}" --} - --- | 'Clause' is a 'SingleStorage' on the number of literals in it. -instance SingleStorage Clause Int where - -- | returns the number of literals in a clause, even if the given clause is a binary clause - {-# SPECIALIZE INLINE get' :: Clause -> IO Int #-} - get' = get' . lits - -- getSize (BinaryClause _) = return 1 - -- | sets the number of literals in a clause, even if the given clause is a binary clause - {-# SPECIALIZE INLINE set' :: Clause -> Int -> IO () #-} - set' c n = set' (lits c) n - -- getSize (BinaryClause _) = return 1 - --- | 'Clause' is a 'Stackfamily'on literals since literals in it will be discared if satisifed at level = 0. -instance StackFamily Clause Lit where - -- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals - {-# SPECIALIZE INLINE shrinkBy :: Clause -> Int -> IO () #-} - shrinkBy c n = modifyNth (lits c) (subtract n) 0 - --- 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. -{-# INLINABLE newClauseFromStack #-} -newClauseFromStack :: Bool -> Stack -> IO Clause -newClauseFromStack l vec = do - n <- get' vec - v <- newStack n - let - loop ((<= n) -> False) = return () - loop i = (setNth v i =<< getNth vec i) >> loop (i + 1) - loop 0 - Clause l <$> {- new' 0 <*> -} new' 0.0 <*> new' False <*> return v - --------------------------------------------------------------------------------- Clause Vector - --- | Mutable 'Clause' Vector -type ClauseVector = MV.IOVector Clause - --- | 'ClauseVector' is a vector of 'Clause'. -instance VecFamily ClauseVector Clause where - {-# SPECIALIZE INLINE getNth :: ClauseVector -> Int -> IO Clause #-} - getNth = MV.unsafeRead - {-# SPECIALIZE INLINE setNth :: ClauseVector -> Int -> Clause -> IO () #-} - setNth = MV.unsafeWrite - {-# SPECIALIZE INLINE swapBetween :: ClauseVector -> Int -> Int -> IO () #-} - swapBetween = MV.unsafeSwap - 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 diff --git a/SAT/Mios/ClauseManager.hs b/SAT/Mios/ClauseManager.hs deleted file mode 100644 --- a/SAT/Mios/ClauseManager.hs +++ /dev/null @@ -1,234 +0,0 @@ -{-# LANGUAGE - BangPatterns - , FlexibleInstances - , MultiParamTypeClasses - , RecordWildCards - , ViewPatterns - #-} -{-# LANGUAGE Trustworthy #-} - --- | A shrinkable vector of 'C.Clause' -module SAT.Mios.ClauseManager - ( - -- * higher level interface for ClauseVector - ClauseManager (..) - -- * Manager with an extra Int (used as sort key or blocking literal) - , ClauseExtManager - , pushClauseWithKey - , getKeyVector - , markClause --- , purifyManager - -- * WatcherList - , WatcherList - , newWatcherList - , getNthWatcher - ) - where - -import Control.Monad (unless, when) -import qualified Data.IORef as IORef -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 vector of 'C.Clause'. -class ClauseManager a where - newManager :: Int -> IO a - getClauseVector :: a -> IO C.ClauseVector --- removeClause :: a -> C.Clause -> IO () --- removeNthClause :: a -> Int -> IO () - --------------------------------------------------------------------------------- - --- | Clause + Blocking Literal -data ClauseExtManager = ClauseExtManager - { - _nActives :: !Int' -- number of active clause - , _purged :: !Bool' -- whether it needs gc - , _clauseVector :: IORef.IORef C.ClauseVector -- clause list - , _keyVector :: IORef.IORef (UVector Int) -- Int list - } - --- | 'ClauseExtManager' is a 'SingleStorage` on the numeber of clauses in it. -instance SingleStorage ClauseExtManager Int where - {-# SPECIALIZE INLINE get' :: ClauseExtManager -> IO Int #-} - get' m = get' (_nActives m) - {-# SPECIALIZE INLINE set' :: ClauseExtManager -> Int -> IO () #-} - set' m = set' (_nActives m) - --- | 'ClauseExtManager' is a 'StackFamily` on clauses. -instance StackFamily ClauseExtManager C.Clause where - {-# SPECIALIZE INLINE shrinkBy :: ClauseExtManager -> Int -> IO () #-} - shrinkBy m k = modify' (_nActives m) (subtract k) - pushTo ClauseExtManager{..} c = do - -- checkConsistency m c - !n <- get' _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' <- growBy 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 - modify' _nActives (1 +) - --- | 'ClauseExtManager' is a 'ClauseManager' -instance ClauseManager ClauseExtManager where - -- | returns a new instance. - {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-} - newManager initialSize = do - i <- new' 0 - v <- C.newClauseVector initialSize - b <- newVec (MV.length v) 0 - ClauseExtManager i <$> new' False <*> IORef.newIORef v <*> IORef.newIORef b - -- | returns the internal 'C.ClauseVector'. - {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-} - getClauseVector !m = IORef.readIORef (_clauseVector m) -{- - -- | O(1) insertion function - pushClause !ClauseExtManager{..} !c = do - -- checkConsistency m c - !n <- get' _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' <- growBy 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 - modify' _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 <$> get' _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 - set' _nActives n - removeNthClause = error "removeNthClause is not implemented on ClauseExtManager" --} - --- | sets the expire flag to a clause. -{-# INLINABLE markClause #-} -markClause :: ClauseExtManager -> C.Clause -> IO () -markClause ClauseExtManager{..} c = do - !n <- get' _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 - set' _purged True - -{-# INLINABLE purifyManager #-} -purifyManager :: ClauseExtManager -> IO () -purifyManager ClauseExtManager{..} = do - diry <- get' _purged - when diry $ do - n <- get' _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 <- getNth vec i - if c /= C.NullClause - then do - unless (i == j) $ do - setNth vec j c - setNth keys j =<< getNth keys i - loop (i + 1) (j + 1) - else loop (i + 1) j - set' _nActives =<< loop 0 0 - set' _purged False - --- | returns the associated Int vector, which holds /blocking literals/. -{-# INLINE getKeyVector #-} -getKeyVector :: ClauseExtManager -> IO (UVector Int) -getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector - --- | O(1) inserter -{-# INLINABLE pushClauseWithKey #-} -pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO () -pushClauseWithKey !ClauseExtManager{..} !c k = do - -- checkConsistency m c - !n <- get' _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' <- growBy 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 - modify' _nActives (1 +) - --- | 'ClauseExtManager' is a collection of 'C.Clause' -instance VecFamily ClauseExtManager C.Clause where - getNth = error "no getNth method for ClauseExtManager" - setNth = error "no setNth method for ClauseExtManager" - {-# SPECIALIZE INLINE reset :: ClauseExtManager -> IO () #-} - reset m = set' (_nActives m) 0 -{- - dump mes ClauseExtManager{..} = do - n <- get' _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 - --- | Immutable 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 <$> mapM (\_ -> newManager m) [0 .. int2lit (negate n) + 1] - --- | returns the watcher List for "Literal" /l/. -{-# INLINE getNthWatcher #-} -getNthWatcher :: WatcherList -> Lit -> ClauseExtManager -getNthWatcher = V.unsafeIndex - --- | 'WatcherList' is an 'Lit'-indexed collection of 'C.Clause'. -instance VecFamily WatcherList C.Clause where - getNth = error "no getNth method for WatcherList" -- getNthWatcher is a pure function - setNth = error "no setNth method for WatcherList" - {-# SPECIALIZE INLINE reset :: WatcherList -> IO () #-} - reset = V.mapM_ purifyManager --- dump _ _ = (mes ++) . concat <$> mapM (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i)) [1 .. V.length wl - 1] diff --git a/SAT/Mios/Main.hs b/SAT/Mios/Main.hs deleted file mode 100644 --- a/SAT/Mios/Main.hs +++ /dev/null @@ -1,817 +0,0 @@ -{-# 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 (unless, void, when) -import Data.Bits -import Data.Foldable (foldrM) -import SAT.Mios.Types -import SAT.Mios.Clause -import SAT.Mios.ClauseManager -import SAT.Mios.Solver - --- | returns a rank of 'Clause'. Smaller value is better. -{-# INLINE rankOf #-} -rankOf :: Clause -> IO Int -rankOf = get' - --- | #114: __RemoveWatch__ -{-# INLINABLE removeWatch #-} -removeWatch :: Solver -> Clause -> IO () -removeWatch (watches -> w) c = do - let lvec = asUVector 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)__ creates a new LEARNT clause and adds it to watcher lists. --- This is a strippped-down version of 'newClause' in Solver. -{-# INLINABLE newLearntClause #-} -newLearntClause :: Solver -> Stack -> IO () -newLearntClause s@Solver{..} ps = do - good <- get' 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 <- get' ps - case k of - 1 -> do - l <- getNth ps 1 - unsafeEnqueue s l NullClause - _ -> do - -- allocate clause: - c <- newClauseFromStack True ps - let vec = asUVector 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: - set' (activity c) . fromIntegral =<< decisionLevel s -- newly learnt clauses should be considered active - -- Add clause to all managers - pushTo 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 - set' (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 <- get' c - let - lvec = asUVector 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@ -{-# INLINABLE analyze #-} -analyze :: Solver -> Clause -> IO Int -analyze s@Solver{..} confl = do - -- litvec - reset litsLearnt - pushTo litsLearnt 0 -- reserve the first place for the unassigned literal - dl <- decisionLevel s - let - litsVec = asUVector litsLearnt - trailVec = asUVector 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 <- get' (lbd c) - when (2 < d) $ do - nblevels <- lbdOf s c - when (nblevels + 1 < d) $ do -- improve the LBD - when (d <= 30) $ set' (protected c) True -- 30 is `lbLBDFrozenClause` - -- seems to be interesting: keep it fro the next round - set' (lbd c) nblevels -- Update it --} - sc <- get' c - let - lvec = asUVector 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 <- getNth reason v - when (r /= NullClause && learnt r) $ pushTo an'lastDL q - -- end of glucose heuristics - loopOnLiterals (j + 1) b (pc + 1) - else pushTo 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' <- getNth 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 <$> get' trail - levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0 - -- Simplify phase (implemented only @expensive_ccmin@ path) - n <- get' litsLearnt - reset an'stack -- analyze_stack.clear(); - reset an'toClear -- out_learnt.copyTo(analyze_toclear); - pushTo 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 - pushTo 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' = shrinkBy litsLearnt $ n - n' - loopOnLits i j = do - l <- getNth litsVec i - c1 <- (NullClause ==) <$> getNth 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 <- get' an'lastDL - r <- get' litsLearnt -- this is not the right value - let - vec = asUVector an'lastDL - loopOnLastDL :: Int -> IO () - loopOnLastDL ((< nld) -> False) = return () - loopOnLastDL i = do - v <- lit2var <$> getNth vec i - r' <- rankOf =<< getNth reason v - when (r < r') $ varBumpActivity s v - loopOnLastDL $ i + 1 - loopOnLastDL 0 - reset an'lastDL - -- Clear seen - k <- get' an'toClear - let - vec' = asUVector 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@. --- -{-# INLINABLE analyzeRemovable #-} -analyzeRemovable :: Solver -> Lit -> Int -> IO Bool -analyzeRemovable Solver{..} p minLevel = do - -- assert (reason[var(p)]!= NullCaulse); - reset an'stack -- analyze_stack.clear() - pushTo an'stack p -- analyze_stack.push(p); - top <- get' an'toClear - let - loopOnStack :: IO Bool - loopOnStack = do - k <- get' an'stack -- int top = analyze_toclear.size(); - if 0 == k - then return True - else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL); - sl <- lastOf an'stack - popFrom an'stack -- analyze_stack.pop(); - c <- getNth reason (lit2var sl) -- getRoot sl - nl <- get' c - let - cvec = asUVector 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 /=) <$> getNth 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; - pushTo an'stack p' -- analyze_stack.push(p); - pushTo 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' <- get' an'toClear - let - vec = asUVector an'toClear - clearAll :: Int -> IO () - clearAll ((< top') -> False) = return () - clearAll j = do x <- getNth vec j; setNth an'seen (lit2var x) 0; clearAll (j + 1) - clearAll top - -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop - shrinkBy 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). --- -{-# INLINABLE analyzeFinal #-} -analyzeFinal :: Solver -> Clause -> Bool -> IO () -analyzeFinal Solver{..} confl skipFirst = do - reset conflicts - rl <- get' rootLevel - unless (rl == 0) $ do - n <- get' confl - let - lvec = asUVector 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 <- get' trailLim - trs <- get' trail - tlz <- getNth (asUVector trailLim) 0 - let - trailVec = asUVector 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) <- getNth reason x - if r == NullClause - then pushTo conflicts (negateLit l) - else do - k <- get' r - let - cvec = asUVector 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 (asUVector 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 = asUVector trail - while :: Clause -> Bool -> IO Clause - while confl False = {- bumpAllVar >> -} return confl - while confl True = do - (p :: Lit) <- getNth trailVec =<< get' qHead - modify' qHead (+ 1) - let (ws :: ClauseExtManager) = getNthWatcher watches p - end <- get' ws - cvec <- getClauseVector ws - bvec <- getKeyVector ws --- rc <- getNth reason $ lit2var p --- byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> get' (lbd rc) else return False - let -{- - checkAllLiteralsIn :: Clause -> IO () -- not in use - checkAllLiteralsIn c = do - nc <- sizeOfClause c - let - vec = asuVector 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 - shrinkBy ws (i - j) - while confl =<< ((<) <$> get' qHead <*> get' 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) <- getNth cvec i - setNth cvec j c - setNth bvec j l - forClause confl (i + 1) (j + 1) - else do - -- checkAllLiteralsIn c - (c :: Clause) <- getNth cvec i - let - lits = asUVector 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 setNth cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1) - else do - -- Look for new watch - cs <- get' c - let - forLit :: Int -> IO Clause - forLit ((< cs) -> False) = do - -- Did not find watch; clause is unit under assignment: - setNth cvec j c - setNth bvec j 0 - result <- enqueue s first c - if not result - then do - ((== 0) <$> decisionLevel s) >>= (`when` set' ok False) - -- #BBCP - set' qHead =<< get' trail - -- Copy the remaining watches: - let - copy i'@((< end) -> False) j' = forClause c i' j' - copy i' j' = do - setNth cvec j' =<< getNth 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 =<< ((<) <$> get' qHead <*> get' 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 =<< getNth 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 - reset watches - shrinkBy 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 <- get' 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 <- getNth vec i - k <- (\k -> if k == 2 then return k else fromEnum <$> get' (protected c)) =<< get' c - case k of - 1 -> set' (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 <- rankOf c - b <- floor . (activityScale *) . (1 -) . logBase claActivityThreshold . max 1 <$> get' (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 <- getNth vec i - let - sweep k = do - k' <- (indexMax .&.) <$> getNth keys k - setNth keys k k - if k' == i - then setNth vec k c - else getNth vec k' >>= setNth 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 <- get' ok - if good - then do - p <- propagate s - if p /= NullClause - then set' ok False >> return False - else do - -- Clear watcher lists: - n <- get' trail - let - vec = asUVector trail - loopOnLit ((< n) -> False) = return () - loopOnLit i = do - l <- getNth vec i - reset . getNthWatcher watches $ l - reset . 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' <- get' ptr - let - loopOnVector :: Int -> Int -> IO Bool - loopOnVector ((< n') -> False) j = shrinkBy ptr (n' - j) >> return True - loopOnVector i j = do - c <- getNth vec' i - l <- locked s c - r <- simplify s c - if not l && r - then removeWatch s c >> loopOnVector (i + 1) j - else setNth vec' j c >> loopOnVector (i + 1) (j + 1) - loopOnVector 0 0 - ret <- for 0 - reset 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 Int -search s@Solver{..} nOfConflicts nOfLearnts = do - -- clear model - let - loop :: Int -> IO Int - loop conflictC = do - !confl <- propagate s - d <- decisionLevel s - if confl /= NullClause - then do - -- CONFLICT - incrementStat s NumOfBackjump 1 - r <- get' 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 <- get' varDecay --- when (d < 0.95) $ modify' varDecay (+ 0.01) - backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself - (s `cancelUntil`) . max backtrackLevel =<< get' rootLevel - newLearntClause s litsLearnt - k <- get' litsLearnt - when (k == 1) $ do - (v :: Var) <- lit2var <$> getNth (asUVector 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 <- get' learnts - k2 <- nAssigns s - when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses - case () of - _ | k2 == nVars -> do - -- Model found: - let - toInt :: Var -> IO Lit - toInt v = (\p -> if lTrue == p then v else negate v) <$> valueVar s v - setModel :: Int -> IO () - setModel ((<= nVars) -> False) = return () - setModel v = (setNth model v =<< toInt v) >> setModel (v + 1) - setModel 1 - return lTrue - _ | conflictC >= nOfConflicts -> do - -- Reached bound on number of conflicts - (s `cancelUntil`) =<< get' rootLevel -- force a restart - claRescaleActivityAfterRestart s - incrementStat s NumOfRestart 1 - return lBottom - _ -> 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 <- get' 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. -{-# INLINABLE solve #-} -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) <- getNth reason (lit2var a) - analyzeFinal s confl True - pushTo conflicts (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 - set' 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 == lBottom - then while (1.5 * nOfConflicts) (1.1 * nOfLearnts) - else cancelUntil s 0 >> return (status == lTrue) - while 100 (nc / 3.0) - --- | Though '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 - setNth reason v from -- NOTE: @from@ might be NULL! - pushTo trail p - --- | __Pre-condition:__ propagation queue is empty. -{-# INLINE unsafeAssume #-} -unsafeAssume :: Solver -> Lit -> IO () -unsafeAssume s@Solver{..} p = do - pushTo trailLim =<< get' trail - unsafeEnqueue s p NullClause diff --git a/SAT/Mios/OptionParser.hs b/SAT/Mios/OptionParser.hs deleted file mode 100644 --- a/SAT/Mios/OptionParser.hs +++ /dev/null @@ -1,132 +0,0 @@ -{-# 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.Types (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 deleted file mode 100644 --- a/SAT/Mios/Solver.hs +++ /dev/null @@ -1,633 +0,0 @@ -{-# LANGUAGE - BangPatterns - , RecordWildCards - , ScopedTypeVariables - , TupleSections - , ViewPatterns - #-} -{-# LANGUAGE Safe #-} - --- | This is a part of MIOS; main data -module SAT.Mios.Solver - ( - -- * Solver - Solver (..) - , VarHeap - , newSolver - , getModel - -- * Misc Accessors - , nAssigns - , nClauses - , nLearnts - , decisionLevel - , valueVar - , valueLit --- , oldLit - , locked - -- * State Modifiers - , addClause - , enqueue - , assume - , cancelUntil - -- * Activities - , claBumpActivity --- , claDecayActivity - , claRescaleActivityAfterRestart - , varBumpActivity - , varDecayActivity - , claActivityThreshold - -- * Stats - , StatIndex (..) - , getStat - , setStat - , incrementStat - , getStats - ) - where - -import Control.Monad (unless, when) -import SAT.Mios.Types -import SAT.Mios.Clause -import SAT.Mios.ClauseManager - --- | __Fig. 2.(p.9)__ Internal State of the solver -data Solver = Solver - { -{- Public Interface -} - model :: !(Vec Int) -- ^ If found, this vector has the model - , conflicts :: !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 -- ^ list of constraint wathing 'p', literal-indexed -{- Assignment Management -} - , assigns :: !(Vec Int) -- ^ The current assignments indexed on variables - , phases :: !(Vec Int) -- ^ The last assignments indexed on variables - , trail :: !Stack -- ^ List of assignments in chronological order - , trailLim :: !Stack -- ^ Separator indices for different decision levels in 'trail'. - , qHead :: !Int' -- ^ 'trail' is divided at qHead; assignment part and queue part - , reason :: !ClauseVector -- ^ For each variable, the constraint that implied its value - , level :: !(Vec Int) -- ^ For each variable, the decision level it was assigned -{- Variable Order -} - , activities :: !(Vec Double) -- ^ Heuristic measurement of the activity of a variable - , order :: !VarHeap -- ^ Keeps track of the dynamic variable order. -{- Configuration -} - , config :: !MiosConfiguration -- ^ search paramerters - , nVars :: !Int -- ^ number of variables -{- - -- , claInc :: !Double' -- ^ Clause activity increment amount to bump with. - -- , varDecay :: !Double' -- ^ used to set 'varInc' --} - , varInc :: !Double' -- ^ Variable activity increment amount to bump with. - , rootLevel :: !Int' -- ^ Separates incremental and search assumptions. -{- Working Memory -} - , ok :: !Bool' -- ^ /return value/ holder - , an'seen :: !(Vec Int) -- ^ used in 'SAT.Mios.Main.analyze' - , an'toClear :: !Stack -- ^ used in 'SAT.Mios.Main.analyze' - , an'stack :: !Stack -- ^ used in 'SAT.Mios.Main.analyze' - , an'lastDL :: !Stack -- ^ last decision level used in 'SAT.Mios.Main.analyze' - , litsLearnt :: !Stack -- ^ used in 'SAT.Mios.Main.analyze' and 'SAT.Mios.Main.search' to create a learnt clause - -{- - -- , pr'seen :: !(Vec Int) -- ^ used in 'SAT.Mios.Main.propagate' --} - , stats :: !(UVector Int) -- ^ statistics information holder -{- - , lbd'seen :: !Vec -- ^ used in lbd computation - , lbd'key :: !Int' -- ^ 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 - <$> newVec nv 0 -- model - <*> newStack nv -- coflict - -- Clause Database - <*> newManager nc -- clauses - <*> newManager nc -- learnts - <*> newWatcherList nv 2 -- watches - -- Assignment Management - <*> newVec nv lBottom -- assigns - <*> newVec nv lBottom -- phases - <*> newStack nv -- trail - <*> newStack nv -- trailLim - <*> new' 0 -- qHead - <*> newClauseVector (nv + 1) -- reason - <*> newVec nv (-1) -- level - -- Variable Order - <*> newVec nv 0 -- activities - <*> newVarHeap nv -- order - -- Configuration - <*> return conf -- config - <*> return nv -- nVars --- <*> new' 1.0 -- claInc --- <*> new' (variableDecayRate conf) -- varDecay - <*> new' 1.0 -- varInc - <*> new' 0 -- rootLevel - -- Working Memory - <*> new' True -- ok - <*> newVec nv 0 -- an'seen - <*> newStack nv -- an'toClear - <*> newStack nv -- an'stack --- <*> newVec nv (-1) -- pr'seen - <*> newStack nv -- litsLearnt - <*> newStack nv -- lastDL - <*> newVec (fromEnum EndOfStatIndex) 0 -- stats -{- --- <*> newVec nv -- lbd'seen --- <*> newInt 0 -- lbd'key --} - --------------------------------------------------------------------------------- --- Accessors - --- | returns the number of current assigments. -{-# INLINE nAssigns #-} -nAssigns :: Solver -> IO Int -nAssigns = get' . trail - --- | returns the number of constraints (clauses). -{-# INLINE nClauses #-} -nClauses :: Solver -> IO Int -nClauses = get' . clauses - --- | returns the number of learnt clauses. -{-# INLINE nLearnts #-} -nLearnts :: Solver -> IO Int -nLearnts = get' . learnts - --- | returns the model as a list of literal. -getModel :: Solver -> IO [Int] -getModel = asList . model - --- | returns the current decision level. -{-# INLINE decisionLevel #-} -decisionLevel :: Solver -> IO Int -decisionLevel = get' . 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 -valueLit (assigns -> a) p = (\x -> if positiveLit p then x else negate x) <$> getNth a (lit2var p) - -{- --- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit' in phases. -{-# INLINE oldLit #-} -oldLit :: Solver -> Lit -> IO Lit -oldLit (phases -> a) (lit2var -> v) = (var2lit v . (== 1)) <$> getNth a v --} - --- | __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 ==) <$> (getNth (reason s) . lit2var =<< getNth (lits c) 1) - --------------------------------------------------------------------------------- Statistics - --- | stat index -data StatIndex = - NumOfBackjump -- ^ the number of backjump - | NumOfRestart -- ^ the number of restart - | EndOfStatIndex -- ^ Don't use this dummy. - 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 a 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 -> Stack -> IO Bool -addClause s@Solver{..} vecLits = do - result <- clauseNew s vecLits False - case result of - Left b -> return b -- No new clause was returned becaues a confilct occured or the clause is a literal - Right c -> pushTo clauses c >> return True - --- | __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.) --- --- * @Left False@ if the clause is in a confilct --- * @Left True@ if the clause is satisfied --- * @Right clause@ if the clause is enqueued successfully -{-# INLINABLE clauseNew #-} -clauseNew :: Solver -> Stack -> Bool -> IO (Either 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 -> reset ps >> return True -- p and negateLit p occurs in ps - _ -> handle (j + 1) l n - loopForLearnt :: Int -> IO Bool - loopForLearnt i = do - n <- get' ps - 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 <- get' ps - 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 -> reset ps >> 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 <- get' ps - case k of - 0 -> return (Left exit) - 1 -> do - l <- getNth ps 1 - Left <$> enqueue s l NullClause - _ -> do - -- allocate clause: - c <- newClauseFromStack isLearnt ps - let vec = asUVector 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 - varBumpActivity s v' -- this is a just good chance to bump activities of literals in this clause - 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 - -- 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 (Right 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 <- get' (lbd from) - k <- (12 +) <$> decisionLevel s - when (k < l) $ set' (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 - setNth reason v from -- NOTE: @from@ might be NULL! - pushTo 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 - pushTo (trailLim s) =<< get' (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 = asUVector trail - let tl = asUVector trailLim - lim <- getNth tl lvl - ts <- get' trail - ls <- get' 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. - setNth 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 - shrinkBy trail (ts - lim) - shrinkBy trailLim (ls - lvl) - set' qHead =<< get' 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 - --- | value for rescaling clause activity. -claActivityThreshold :: Double -claActivityThreshold = 1e20 - --- | __Fig. 14 (p.19)__ Bumping of clause activity -{-# INLINE varBumpActivity #-} -varBumpActivity :: Solver -> Var -> IO () -varBumpActivity s@Solver{..} x = do - !a <- (+) <$> getNth activities x <*> get' varInc - setNth activities x a - when (varActivityThreshold < a) $ varRescaleActivity s - update s x -- update the position in heap - --- | __Fig. 14 (p.19)__ -{-# INLINABLE varDecayActivity #-} -varDecayActivity :: Solver -> IO () -varDecayActivity Solver{..} = modify' varInc (/ variableDecayRate config) --- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay - --- | __Fig. 14 (p.19)__ -{-# INLINABLE varRescaleActivity #-} -varRescaleActivity :: Solver -> IO () -varRescaleActivity Solver{..} = do - let - loop ((<= nVars) -> False) = return () - loop i = modifyNth activities (/ varActivityThreshold) i >> loop (i + 1) - loop 1 - modify' varInc (/ varActivityThreshold) - --- | __Fig. 14 (p.19)__ -{-# INLINE claBumpActivity #-} -claBumpActivity :: Solver -> Clause -> IO () -claBumpActivity s Clause{..} = do - dl <- decisionLevel s - a <- (fromIntegral dl +) <$> get' activity - set' activity a - -- set' 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)__ -{-# INLINABLE claRescaleActivity #-} -claRescaleActivity :: Solver -> IO () -claRescaleActivity Solver{..} = do - vec <- getClauseVector learnts - n <- get' learnts - let - loopOnVector :: Int -> IO () - loopOnVector ((< n) -> False) = return () - loopOnVector i = do - c <- getNth vec i - modify' (activity c) (/ claActivityThreshold) - loopOnVector $ i + 1 - loopOnVector 0 - -- modifyDouble claInc (/ claActivityThreshold) - --- | __Fig. 14 (p.19)__ -{-# INLINABLE claRescaleActivityAfterRestart #-} -claRescaleActivityAfterRestart :: Solver -> IO () -claRescaleActivityAfterRestart Solver{..} = do - vec <- getClauseVector learnts - n <- get' learnts - let - loopOnVector :: Int -> IO () - loopOnVector ((< n) -> False) = return () - loopOnVector i = do - c <- getNth vec i - d <- get' c - if d < 9 - then modify' (activity c) sqrt - else set' (activity c) 0 - set' (protected c) False - loopOnVector $ i + 1 - loopOnVector 0 - --------------------------------------------------------------------------------- VarHeap - --- | 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 :: !Stack -- order to var - , idxs :: !Stack -- var to order (index) - } - -newVarHeap :: Int -> IO VarHeap -newVarHeap n = do - v1 <- newVec n 0 - v2 <- newVec n 0 - let - loop :: Int -> IO () - loop ((<= n) -> False) = set' v1 n >> set' v2 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 = get' . heap . order - -{-# 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 <- getNth activities v - 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 <- getNth activities v' - 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 <- getNth activities v - 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 <- getNth activities l - acR <- getNth activities r - 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 - -{-# INLINABLE 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 - set' to n - percolateUp s n - --- | returns the value on the root (renamed from @getmin@). -{-# INLINABLE 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 deleted file mode 100644 --- a/SAT/Mios/Types.hs +++ /dev/null @@ -1,257 +0,0 @@ -{-# LANGUAGE - BangPatterns - , MultiParamTypeClasses - #-} -{-# LANGUAGE Safe #-} - --- | Basic data types used throughout mios. -module SAT.Mios.Types - ( - module SAT.Mios.Vec - -- * Variable - , Var - , bottomVar - , int2var - -- * Internal encoded Literal - , Lit - , lit2int - , int2lit - , bottomLit --- , newLit - , positiveLit - , lit2var - , var2lit - , negateLit - -- * Assignment on the lifted Bool domain --- , LiftedBool (..) --- , lbool - , lFalse - , lTrue - , lBottom - , VarOrder (..) - -- * CNF - , CNFDescription (..) - -- * Solver Configuration - , MiosConfiguration (..) - , defaultConfiguration - ) - where - -import Data.Bits -import SAT.Mios.Vec - --- | 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 :: Int -> Int -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 --} - --- | /FALSE/ on the Lifted Bool domain -lFalse:: Int -lFalse = -1 - --- | /TRUE/ on the Lifted Bool domain -lTrue :: Int -lTrue = 1 - --- | /UNDEFINED/ on the Lifted Bool domain -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 :: (VecFamily v1 Bool, VecFamily 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" --} - -- | should be called when a variable has increased in activity. - update :: o -> Var -> IO () - update _ = error "update undefined" -{- - -- | should be called when all variables have been assigned. - updateAll :: o -> IO () - updateAll = error "updateAll undefined" --} - -- | should be called when a variable becomes unbound (may be selected again). - undo :: o -> Var -> IO () - undo _ _ = error "undo undefined" - - -- | returns a new, unassigned var as the next decision. - select :: o -> IO Var - select = error "select undefined" - --- | Misc information on a CNF -data CNFDescription = CNFDescription - { - _numberOfVariables :: !Int -- ^ the number of variables - , _numberOfClauses :: !Int -- ^ the number of clauses - , _pathname :: Maybe FilePath -- ^ given filename - } - deriving (Eq, Ord, Show) - --- | 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/Util/BoolExp.hs b/SAT/Mios/Util/BoolExp.hs deleted file mode 100644 --- a/SAT/Mios/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.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/DIMACS.hs b/SAT/Mios/Util/DIMACS.hs deleted file mode 100644 --- a/SAT/Mios/Util/DIMACS.hs +++ /dev/null @@ -1,31 +0,0 @@ -{-# LANGUAGE Safe #-} - --- | Read/Write a CNF file only with ghc standard libraries -module SAT.Mios.Util.DIMACS - ( - -- * Input - fromFile - , clauseListFromFile - , fromMinisatOutput - , clauseListFromMinisatOutput - -- * Output - , toFile - , toDIMACSString - , asDIMACSString - , asDIMACSString_ - -- * Bool Operation - , module SAT.Mios.Util.BoolExp - ) - where -import SAT.Mios.Util.DIMACS.Reader -import SAT.Mios.Util.DIMACS.Writer -import SAT.Mios.Util.DIMACS.MinisatReader -import SAT.Mios.Util.BoolExp - --- | String from BoolFrom -asDIMACSString :: BoolForm -> String -asDIMACSString = toDIMACSString . asList - --- | String from BoolFrom -asDIMACSString_ :: BoolForm -> String -asDIMACSString_ = toDIMACSString . asList_ diff --git a/SAT/Mios/Util/DIMACS/MinisatReader.hs b/SAT/Mios/Util/DIMACS/MinisatReader.hs deleted file mode 100644 --- a/SAT/Mios/Util/DIMACS/MinisatReader.hs +++ /dev/null @@ -1,73 +0,0 @@ -{-# LANGUAGE Safe #-} - --- | Read an output file of minisat -module SAT.Mios.Util.DIMACS.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/DIMACS/Reader.hs b/SAT/Mios/Util/DIMACS/Reader.hs deleted file mode 100644 --- a/SAT/Mios/Util/DIMACS/Reader.hs +++ /dev/null @@ -1,130 +0,0 @@ -{-# LANGUAGE Safe #-} - --- | Read a CNF file without haskell-platform -module SAT.Mios.Util.DIMACS.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/DIMACS/Writer.hs b/SAT/Mios/Util/DIMACS/Writer.hs deleted file mode 100644 --- a/SAT/Mios/Util/DIMACS/Writer.hs +++ /dev/null @@ -1,58 +0,0 @@ -{-# LANGUAGE Safe #-} - --- | Write SAT data to DIMACS file -module SAT.Mios.Util.DIMACS.Writer - ( - -- * Interface - toFile - , toDIMACSString - , toString - , toLatexString - ) - where -import Data.List (intercalate, nub, sort) -import System.IO - --- | Write the DIMACS to file 'f', using 'toDIMACSString' -toFile :: FilePath -> [[Int]] -> IO () -toFile f l = writeFile f $ toDIMACSString l - --- | Convert [Clause] to String, where Clause is [Int] --- --- >>> toDIMACSString [] --- "p cnf 0 0\n" --- --- >>> toDIMACSString [[-1, 2], [-3, -4]] --- "p cnf 4 2\n-1 2 0\n-3 -4 0\n" --- --- >>> toDIMACSString [[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" --- -toDIMACSString :: [[Int]] -> String -toDIMACSString 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 deleted file mode 100644 --- a/SAT/Mios/Validator.hs +++ /dev/null @@ -1,47 +0,0 @@ -{-# 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) (0 :: Int) :: IO (Vec Int) - vec <- getClauseVector (clauses s) - nc <- get' (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 - sat' <- satAny =<< asList =<< getNth vec i - 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/Mios/Vec.hs b/SAT/Mios/Vec.hs deleted file mode 100644 --- a/SAT/Mios/Vec.hs +++ /dev/null @@ -1,276 +0,0 @@ -{-# LANGUAGE - BangPatterns - , FlexibleContexts - , FlexibleInstances - , FunctionalDependencies - , MultiParamTypeClasses - , TypeFamilies - #-} -{-# LANGUAGE Trustworthy #-} - --- | Abstraction Layer for Mutable Vectors -module SAT.Mios.Vec - ( - -- * Vector class - VecFamily (..) - -- * Vectors - , UVector - , Vec (..) - -- * SingleStorage - , SingleStorage (..) - , Bool' - , Double' - , Int' - -- * Stack - , StackFamily (..) - , Stack - , newStackFromList - ) - where - -import qualified Data.Vector.Unboxed as U -import qualified Data.Vector.Unboxed.Mutable as UV - --- | Interface on vectors. -class VecFamily v a | v -> a where - -- | returns the /n/-th value. - getNth ::v -> Int -> IO a - -- | sets the /n/-th value. - setNth :: v -> Int -> a -> IO () - -- | erases all elements in it. - reset:: v -> IO () - -- | converts to an Int vector. - asUVector :: (a ~ Int) => v -> UVector Int - -- | returns the /n/-th value (index starts from zero in any case). - -- | swaps two elements. - swapBetween :: v -> Int -> Int -> IO () - -- | calls the update function. - modifyNth :: v -> (a -> a) -> Int -> IO () - -- | returns a new vector. - newVec :: Int -> a -> IO v - -- | sets all elements. - setAll :: v -> a -> IO () - -- | extends the size of stack by /n/; note: values in new elements aren't initialized maybe. - growBy :: v -> Int -> IO v - -- | converts to a list. - asList :: v -> IO [a] - {-# MINIMAL getNth, setNth #-} - reset = error "no default method: reset" - asUVector = error "no default method: asUVector" - swapBetween = error "no default method: swapBetween" - modifyNth = error "no default method: modifyNth" - newVec = error "no default method: newVec" - setAll = error "no default method: setAll" - asList = error "no default method: asList" - growBy = error "no default method: growBy" -{- - -- | (FOR DEBUG) dump the contents. - dump :: Show a => String -> v -> IO String - dump msg v = (msg ++) . show <$> asList v --} - --------------------------------------------------------------------------------- UVector - --- | A thin abstract layer for Mutable unboxed Vector -type UVector a = UV.IOVector a - -instance VecFamily (UVector Int) Int where - {-# SPECIALIZE INLINE getNth :: UVector Int -> Int -> IO Int #-} - getNth = UV.unsafeRead - {-# SPECIALIZE INLINE setNth :: UVector Int -> Int -> Int -> IO () #-} - setNth = UV.unsafeWrite - {-# SPECIALIZE INLINE modifyNth :: UVector Int -> (Int -> Int) -> Int -> IO () #-} - modifyNth = UV.unsafeModify - {-# SPECIALIZE INLINE swapBetween:: UVector Int -> Int -> Int -> IO () #-} - swapBetween = UV.unsafeSwap - {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO (UVector Int) #-} - newVec n 0 = UV.new n - newVec n x = do - v <- UV.new n - UV.set v x - return v - {-# SPECIALIZE INLINE setAll :: UVector Int -> Int -> IO () #-} - setAll = UV.set - {-# SPECIALIZE INLINE growBy :: UVector Int -> Int -> IO (UVector Int) #-} - growBy = UV.unsafeGrow - asList v = mapM (UV.unsafeRead v) [0 .. UV.length v - 1] - -instance VecFamily (UVector Double) Double where - {-# SPECIALIZE INLINE getNth :: UVector Double -> Int -> IO Double #-} - getNth = UV.unsafeRead - {-# SPECIALIZE INLINE setNth :: UVector Double -> Int -> Double -> IO () #-} - setNth = UV.unsafeWrite - {-# SPECIALIZE INLINE modifyNth :: UVector Double -> (Double -> Double) -> Int -> IO () #-} - modifyNth = UV.unsafeModify - {-# SPECIALIZE INLINE swapBetween:: UVector Double -> Int -> Int -> IO () #-} - swapBetween = UV.unsafeSwap - {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO (UVector Double) #-} - newVec n x = do - v <- UV.new n - UV.set v x - return v - {-# SPECIALIZE INLINE setAll :: UVector Double -> Double -> IO () #-} - setAll = UV.set - {-# SPECIALIZE INLINE growBy :: UVector Double -> Int -> IO (UVector Double) #-} - growBy = UV.unsafeGrow - asList v = mapM (UV.unsafeRead v) [0 .. UV.length v - 1] - --------------------------------------------------------------------------------- Vec - --- | Another abstraction layer on 'UVector'. --- --- __Note__: the 0-th element of @Vec Int@ is reserved for internal tasks. If you want to use it, use @UVector Int@. -newtype Vec a = Vec (UVector a) - -instance VecFamily (Vec Int) Int where - {-# SPECIALIZE INLINE getNth :: Vec Int -> Int -> IO Int #-} - getNth (Vec v) = UV.unsafeRead v - {-# SPECIALIZE INLINE setNth :: Vec Int -> Int -> Int -> IO () #-} - setNth (Vec v) = UV.unsafeWrite v - {-# SPECIALIZE INLINE reset :: Vec Int -> IO () #-} - reset (Vec v) = setNth v 0 0 - {-# SPECIALIZE INLINE asUVector :: Vec Int -> UVector Int #-} - asUVector (Vec a) = UV.unsafeTail a - {-# SPECIALIZE INLINE modifyNth :: Vec Int -> (Int -> Int) -> Int -> IO () #-} - modifyNth (Vec v) = UV.unsafeModify v - {-# SPECIALIZE INLINE swapBetween :: Vec Int -> Int -> Int -> IO () #-} - swapBetween (Vec v) = UV.unsafeSwap v - {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO (Vec Int) #-} - newVec n x = Vec <$> newVec (n + 1) x - {-# SPECIALIZE INLINE setAll :: Vec Int -> Int -> IO () #-} - setAll (Vec v) = UV.set v - {-# SPECIALIZE INLINE growBy :: Vec Int -> Int -> IO (Vec Int) #-} - growBy (Vec v) n = Vec <$> UV.unsafeGrow v n - asList (Vec v) = mapM (getNth v) [1 .. UV.length v - 1] - -instance VecFamily (Vec Double) Double where - {-# SPECIALIZE INLINE getNth :: Vec Double -> Int -> IO Double #-} - getNth (Vec v) = UV.unsafeRead v - {-# SPECIALIZE INLINE setNth :: Vec Double -> Int -> Double -> IO () #-} - setNth (Vec v) = UV.unsafeWrite v - {-# SPECIALIZE INLINE modifyNth :: Vec Double -> (Double -> Double) -> Int -> IO () #-} - modifyNth (Vec v) = UV.unsafeModify v - {-# SPECIALIZE INLINE swapBetween :: Vec Double -> Int -> Int -> IO () #-} - swapBetween (Vec v) = UV.unsafeSwap v - {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO (Vec Double) #-} - newVec n x = Vec <$> newVec (n + 1) x - {-# SPECIALIZE INLINE setAll :: Vec Double -> Double -> IO () #-} - setAll (Vec v) = UV.set v - {-# SPECIALIZE INLINE growBy :: Vec Double -> Int -> IO (Vec Double) #-} - growBy (Vec v) n = Vec <$> UV.unsafeGrow v n - --------------------------------------------------------------------------------- SingleStorage - --- | Interface for single mutable data -class SingleStorage s t | s -> t where - -- | allocates and returns an new data. - new' :: t -> IO s - -- | gets the value. - get' :: s -> IO t - -- | sets the value. - set' :: s -> t -> IO () - -- | calls an update function on it. - modify' :: s -> (t -> t) -> IO () - {-# MINIMAL get', set' #-} - new' = undefined - modify' = undefined - --- | Mutable Int --- __Note:__ Int' is the same with 'Stack' -type Int' = UV.IOVector Int - -instance SingleStorage Int' Int where - {-# SPECIALIZE INLINE new' :: Int -> IO Int' #-} - new' k = do - s <- UV.new 1 - UV.unsafeWrite s 0 k - return s - {-# SPECIALIZE INLINE get' :: Int' -> IO Int #-} - get' val = UV.unsafeRead val 0 - {-# SPECIALIZE INLINE set' :: Int' -> Int -> IO () #-} - set' val !x = UV.unsafeWrite val 0 x - {-# SPECIALIZE INLINE modify' :: Int' -> (Int -> Int) -> IO () #-} - modify' val f = UV.unsafeModify val f 0 - --- | Mutable Bool -type Bool' = UV.IOVector Bool - -instance SingleStorage Bool' Bool where - {-# SPECIALIZE INLINE new' :: Bool -> IO Bool' #-} - new' k = do - s <- UV.new 1 - UV.unsafeWrite s 0 k - return s - {-# SPECIALIZE INLINE get' :: Bool' -> IO Bool #-} - get' val = UV.unsafeRead val 0 - {-# SPECIALIZE INLINE set' :: Bool' -> Bool -> IO () #-} - set' val !x = UV.unsafeWrite val 0 x - {-# SPECIALIZE INLINE modify' :: Bool' -> (Bool -> Bool) -> IO () #-} - modify' val f = UV.unsafeModify val f 0 - --- | Mutable Double -type Double' = UV.IOVector Double - -instance SingleStorage Double' Double where - {-# SPECIALIZE INLINE new' :: Double -> IO Double' #-} - new' k = do - s <- UV.new 1 - UV.unsafeWrite s 0 k - return s - {-# SPECIALIZE INLINE get' :: Double' -> IO Double #-} - get' val = UV.unsafeRead val 0 - {-# SPECIALIZE INLINE set' :: Double' -> Double -> IO () #-} - set' val !x = UV.unsafeWrite val 0 x - {-# SPECIALIZE INLINE modify' :: Double' -> (Double -> Double) -> IO () #-} - modify' val f = UV.unsafeModify val f 0 - --------------------------------------------------------------------------------- Stack - --- | Interface on stacks -class SingleStorage s Int => StackFamily s t | s -> t where - -- | returns a new stack. - newStack :: Int -> IO s - -- | pushs an value to the tail of the stack. - pushTo :: s -> t-> IO () - -- | pops the last element. - popFrom :: s -> IO () - -- | peeks the last element. - lastOf :: s -> IO t - -- | shrinks the stack. - shrinkBy :: s -> Int -> IO () - newStack = undefined - pushTo = undefined - popFrom = undefined - lastOf = undefined - shrinkBy = undefined - --- | Alias of @Vec Int@. The 0-th element holds the number of elements. -type Stack = Vec Int - -instance SingleStorage Stack Int where - {-# SPECIALIZE INLINE get' :: Stack -> IO Int #-} - get' (Vec v) = UV.unsafeRead v 0 - {-# SPECIALIZE INLINE set' :: Stack -> Int -> IO () #-} - set' (Vec v) !x = UV.unsafeWrite v 0 x - {-# SPECIALIZE INLINE modify' :: Stack -> (Int -> Int) -> IO () #-} - modify' (Vec v) f = UV.unsafeModify v f 0 - -instance StackFamily Stack Int where - {-# SPECIALIZE INLINE newStack :: Int -> IO Stack #-} - newStack n = newVec n 0 - {-# SPECIALIZE INLINE pushTo :: Stack -> Int -> IO () #-} - pushTo (Vec v) x = do - i <- (+ 1) <$> UV.unsafeRead v 0 - UV.unsafeWrite v i x - UV.unsafeWrite v 0 i - {-# SPECIALIZE INLINE popFrom :: Stack -> IO () #-} - popFrom (Vec v) = UV.unsafeModify v (subtract 1) 0 - {-# SPECIALIZE INLINE lastOf :: Stack -> IO Int #-} - lastOf (Vec v) = UV.unsafeRead v =<< UV.unsafeRead v 0 - {-# SPECIALIZE INLINE shrinkBy :: Stack -> Int -> IO () #-} - shrinkBy (Vec v) k = UV.unsafeModify v (subtract k) 0 - --- | returns a new 'Stack' from @[Int]@. -{-# INLINABLE newStackFromList #-} -newStackFromList :: [Int] -> IO Stack -newStackFromList !l = Vec <$> U.unsafeThaw (U.fromList (length l : l)) diff --git a/app/mios.hs b/app/mios.hs --- a/app/mios.hs +++ b/app/mios.hs @@ -1,3 +1,6 @@ +{-# LANGUAGE + MultiWayIf + #-} -- | Executable of 'Minisat Implementation and Optimization Study' module Main ( @@ -7,14 +10,15 @@ import SAT.Mios +usage :: String +usage = miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf" + -- | main main :: IO () -main = do - opts <- miosParseOptionsFromArgs versionId - case () of - _ | _displayVersion opts -> putStrLn versionId - _ | _displayHelp opts -> putStrLn $ miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf" - _ | _targetFile opts == Just "" -> putStrLn $ miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf" - _ | _validateAssignment opts -> executeValidator opts - _ | otherwise -> executeSolver opts +main = do opts <- miosParseOptionsFromArgs versionId + if | _displayVersion opts -> putStrLn versionId + | _displayHelp opts -> putStrLn usage + | _targetFile opts == Nothing -> putStrLn usage + | _validateAssignment opts -> executeValidator opts + | otherwise -> executeSolver opts diff --git a/mios.cabal b/mios.cabal --- a/mios.cabal +++ b/mios.cabal @@ -2,13 +2,12 @@ -- see http://haskell.org/cabal/users-guide/ name: mios -version: 1.4.0 -synopsis: A Minisat-based SAT solver in Haskell +version: 1.5.4 +synopsis: A Minisat-based CDCL 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 2.0 time slower than Minisat-2.2. + A modern and very fast SAT solver written in Haskell, using CDCL, watch literals, VSIDS, + blocking-literals, phase saving, LBD, Glucose-like restart and so on. 'Mios' is an abbreviation of 'Minisat-based Implementation and Optimization Study on SAT solver'. . @@ -20,7 +19,7 @@ category: Artificial Intelligence, Constraints build-type: Simple cabal-version: >=1.16 -extra-source-files: app/sample.hs +extra-source-files: app/sample.hs source-repository head type: git @@ -30,38 +29,41 @@ Description: Compile with llvm Default: False -Flag lib - Description: Build the solver library - Default: True +Flag MultiConflict + Description: Build tools in MultiConflict + Default: False +Flag utils + Description: Build misc utilities for developer + Default: False + library - if flag(lib) - buildable: True - else - buildable: False + hs-source-dirs: src default-language: Haskell2010 default-extensions: Strict - other-extensions: BangPatterns - FlexibleContexts - FlexibleInstances - FunctionalDependencies - MagicHash - MultiParamTypeClasses - RecordWildCards - ScopedTypeVariables - TypeFamilies - Trustworthy - TupleSections - Safe - UndecidableInstances - ViewPatterns + other-extensions: BangPatterns + FlexibleContexts + FlexibleInstances + FunctionalDependencies + MagicHash + MultiParamTypeClasses + RecordWildCards + ScopedTypeVariables + TypeFamilies + Trustworthy + TupleSections + Safe + UndecidableInstances + ViewPatterns exposed-modules: SAT.Mios.Clause SAT.Mios.ClauseManager - SAT.Mios.Vec + SAT.Mios.ClausePool + SAT.Mios.Criteria SAT.Mios.Main SAT.Mios.OptionParser SAT.Mios.Solver + SAT.Mios.Vec SAT.Mios.Types SAT.Mios.Validator SAT.Mios.Util.DIMACS.MinisatReader @@ -70,29 +72,119 @@ SAT.Mios.Util.DIMACS SAT.Mios.Util.BoolExp SAT.Mios - build-depends: base ==4.9.*, vector >=0.11, ghc-prim >=0.5, bytestring >=0.10 + build-depends: base >=4.10 && < 5, vector >=0.12, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6 if flag(llvm) - ghc-options: -O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3 + ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures else - ghc-options: -O2 -ignore-asserts -funbox-strict-fields + ghc-options: -O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures -executable mios - main-is: app/mios.hs +executable mios-1.5.4 + hs-source-dirs: app + main-is: mios.hs buildable: True default-language: Haskell2010 - default-extensions: Strict - build-depends: base ==4.9.*, vector >=0.11, ghc-prim >=0.5, bytestring >=0.10 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios if flag(llvm) - ghc-options: -O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3 + ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -rtsopts -fwarn-missing-signatures else + ghc-options: -O2 -funbox-strict-fields -msse2 -rtsopts -fwarn-missing-signatures + +executable cnf-stat + hs-source-dirs: utils + main-is: cnf-stat.hs + if flag(utils) + buildable: True + else + buildable: False + default-language: Haskell2010 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios, bytestring >=0.10 + ghc-options: -O1 -ignore-asserts -funbox-strict-fields + +executable mios-mc + hs-source-dirs: MultiConflict app + main-is: mios.hs + if flag(MultiConflict) + buildable: True + else + buildable: False + default-language: Haskell2010 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios, bytestring >=0.10 + if flag(llvm) + ghc-options: -O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O2 -optlc-O2 + else ghc-options: -O2 -ignore-asserts -funbox-strict-fields - other-modules: - SAT.Mios.Clause - SAT.Mios.ClauseManager - SAT.Mios.Vec - SAT.Mios.Main - SAT.Mios.OptionParser - SAT.Mios.Solver - SAT.Mios.Types - SAT.Mios.Validator - SAT.Mios + +executable mc-dump2csv + hs-source-dirs: MultiConflict + main-is: utils/dump2csv.hs + if flag(MultiConflict) && flag(utils) + buildable: True + else + buildable: False + default-language: Haskell2010 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios, bytestring >=0.10 + ghc-options: -O1 -ignore-asserts -funbox-strict-fields + +executable mc-averagecsv + hs-source-dirs: MultiConflict + main-is: utils/averagecsv.hs + if flag(MultiConflict) && flag(utils) + buildable: True + else + buildable: False + default-language: Haskell2010 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios, bytestring >=0.10 + ghc-options: -O1 -ignore-asserts -funbox-strict-fields + +executable mc-summary + hs-source-dirs: MultiConflict + main-is: utils/summary.hs + if flag(MultiConflict) && flag(utils) + buildable: True + else + buildable: False + default-language: Haskell2010 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios, bytestring >=0.10 + ghc-options: -O1 -ignore-asserts -funbox-strict-fields + +executable mc-stat2csv + hs-source-dirs: MultiConflict + main-is: utils/stat2csv.hs + if flag(MultiConflict) && flag(utils) + buildable: True + else + buildable: False + default-language: Haskell2010 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios, bytestring >=0.10 + ghc-options: -O1 -ignore-asserts -funbox-strict-fields + +executable mc-pickup + hs-source-dirs: MultiConflict + main-is: utils/pickup.hs + if flag(MultiConflict) && flag(utils) + buildable: True + else + buildable: False + default-language: Haskell2010 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios, bytestring >=0.10 + ghc-options: -O1 -ignore-asserts -funbox-strict-fields + +executable mc-numbers + hs-source-dirs: MultiConflict + main-is: utils/numbers.hs + if flag(MultiConflict) && flag(utils) + buildable: True + else + buildable: False + default-language: Haskell2010 + default-extensions: Strict + build-depends: base >=4.10 && < 5, mios, bytestring >=0.10 + ghc-options: -O1 -ignore-asserts -funbox-strict-fields diff --git a/src/SAT/Mios.hs b/src/SAT/Mios.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios.hs @@ -0,0 +1,335 @@ +-- | (This file is a part of MIOS.) +-- Minisat-based Implementation and Optimization Study on SAT solver +{-# LANGUAGE + BangPatterns + , LambdaCase + , ViewPatterns +#-} +{-# LANGUAGE Safe #-} + +module SAT.Mios + ( + -- * Interface to the core of solver + versionId + , CNFDescription (..) + , module SAT.Mios.OptionParser + , runSolver + , solveSAT + , solveSATWithConfiguration + , solve + , SolverResult + , Certificate (..) + -- * Assignment Validator + , validateAssignment + , validate + -- * For standalone programs + , executeSolverOn + , executeSolver + , executeValidatorOn + , executeValidator + -- * File IO + , parseCNF + , injectClausesFromCNF + , dumpAssigmentAsCNF + ) + where + +import Control.Concurrent (forkIO, killThread, myThreadId, threadDelay + , newEmptyMVar, putMVar, readMVar) +import Control.Exception +import Control.Monad ((<=<), unless, void, when) +import Data.Char +import qualified Data.ByteString.Char8 as B +import Numeric (showFFloat) +import System.CPUTime +import System.Exit +import System.IO + +import SAT.Mios.Types +import SAT.Mios.Main +import SAT.Mios.OptionParser +import SAT.Mios.Validator + +-- | version name +versionId :: String +versionId = "mios-1.5.4 -- https://github.com/shnarazk/mios" + +reportElapsedTime :: Bool -> String -> Integer -> IO Integer +reportElapsedTime False _ 0 = return 0 +reportElapsedTime False _ _ = getCPUTime +reportElapsedTime True 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 -> (Just cnfFile)) = do + t0 <- reportElapsedTime False "" $ if _confVerbose opts || 0 <= _confBenchmark opts then -1 else 0 + (desc, cls) <- parseCNF (_targetFile opts) + -- when (_numberOfVariables desc == 0) $ error $ "couldn't load " ++ show cnfFile + token <- newEmptyMVar -- :: IO (MVar (Maybe Solver)) + solverId <- myThreadId + handle (\case + UserInterrupt -> putStrLn "User interrupt recieved." + ThreadKilled -> reportResult opts t0 =<< readMVar token + e -> print e) $ do + when (0 < _confBenchmark opts) $ + void $ forkIO $ do let fromMicro = 1000000 :: Int + threadDelay $ fromMicro * fromIntegral (_confBenchmark opts) + putMVar token (Left TimeOut) + killThread solverId + when (_confMaxSize opts < _numberOfVariables desc) $ + if -1 == _confBenchmark opts + then errorWithoutStackTrace $ "ABORT: too many variables to solve, " ++ show desc + else putMVar token (Left OutOfMemory) >> killThread solverId + s <- newSolver (toMiosConf opts) desc + injectClausesFromCNF s desc cls + void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Parse: ") t0 + when (0 < _confDumpStat opts) $ dumpSolver DumpCSVHeader s + result <- solve s [] + putMVar token result + killThread solverId + +executeSolver _ = return () + +-- | print messages on solver's result +-- Note: the last field of benchmark CSV is: +-- * 0 if UNSAT +-- * 1 if satisfiable (by finding an assignment) +-- * other bigger values are used for aborted cases. +reportResult :: MiosProgramOption -> Integer -> SolverResult -> IO () +-- abnormal cases, catching 'too large CNF', 'timeout' for now. +reportResult opts@(_targetFile -> Just cnfFile) _ (Left flag) = + putStrLn ("\"" ++ takeWhile (' ' /=) versionId ++ "\"," + ++ show (_confBenchSeq opts) ++ "," + ++ "\"" ++ cnfFile ++ "\"," + ++ show (_confBenchmark opts) ++ "," ++ show (fromEnum flag)) + +-- solver terminated normally +reportResult opts@(_targetFile -> Just cnfFile) t0 (Right result) = do + t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0 + case result of + _ | 0 <= _confBenchmark opts -> return () + SAT _ | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "SATISFIABLE" + UNSAT _ | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "UNSATISFIABLE" + SAT asg -> print asg + UNSAT t -> do when (_confVerbose opts) $ hPutStrLn stderr "UNSAT" -- contradiction + print t + dumpAssigmentAsCNF (_outputFile opts) result + valid <- if _confCheckAnswer opts || 0 <= _confBenchmark opts + then case result of + SAT asg -> do (desc, cls) <- parseCNF (_targetFile opts) + s' <- newSolver (toMiosConf opts) desc + injectClausesFromCNF s' desc cls + validate s' asg + UNSAT _ -> return True + else return True + when (_confCheckAnswer opts) $ do + if _confVerbose opts + then hPutStrLn stderr $ if valid then "A vaild answer" else "Internal error: mios returns a wrong answer" + else unless valid $ hPutStrLn stderr "Internal error: mios returns a wrong answer" + void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Validate: ") t2 + when (0 <= _confBenchmark opts) $ do + let fromPico = 1000000000000 :: Double + phase = case result of { SAT _ -> 1; UNSAT _ -> 0::Int } + putStrLn $ "\"" ++ takeWhile (' ' /=) versionId ++ "\"," + ++ show (_confBenchSeq opts) ++ "," + ++ "\"" ++ cnfFile ++ "\"," + ++ if valid + then showFFloat (Just 3) (fromIntegral (t2 - t0) / fromPico) "," ++ show phase + else show (_confBenchmark opts) ++ "," ++ show (fromEnum InternalInconsistent) + +reportResult _ _ _ = 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`) <=< (newStackFromList . map int2lit)) c + noConf <- simplifyDB s + if noConf + then do + x <- solve s [] + case x of + Right (SAT a) -> return $ Right a + Right (UNSAT a) -> return $ Left a + _ -> return $ Left [] + 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`) <=< (newStackFromList . map int2lit)) cls + noConf <- simplifyDB s + if noConf + then do result <- solve s [] + case result of + Right (SAT a) -> return a + _ -> 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) <- parseCNF target + when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ show cnfFile + s <- newSolver (toMiosConf opts) desc + injectClausesFromCNF s desc cls + when (_confVerbose opts) $ + hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (_numberOfVariables desc) ++ " #c = " ++ show (_numberOfClauses desc) + 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`) <=< (newStackFromList . 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 (Just "result.cnf") y <$> model s +-- +dumpAssigmentAsCNF :: Maybe FilePath -> Certificate -> IO () +dumpAssigmentAsCNF Nothing _ = return () +-- | FIXME: swtich to DRAT +dumpAssigmentAsCNF (Just fname) (UNSAT _) = + writeFile fname "s UNSAT\n0\n" +dumpAssigmentAsCNF (Just fname) (SAT l) = + withFile fname WriteMode $ \h -> do hPutStrLn h "s SAT"; hPutStrLn h . (++ " 0") . unwords $ map show l + +-------------------------------------------------------------------------------- +-- DIMACS CNF Reader +-------------------------------------------------------------------------------- + +-- | parses the header of a CNF file +parseCNF :: Maybe FilePath -> IO (CNFDescription, B.ByteString) +parseCNF target@(Just cnfFile) = do + let -- format: p cnf n m, length "p cnf" == 5 + parseP line = case parseInt (skipWhitespace (B.drop 5 line)) of + (x, second) -> case B.readInt (skipWhitespace second) of + Just (y, _) -> CNFDescription x y target + seek :: B.ByteString -> IO (CNFDescription, B.ByteString) + seek bs + | B.head bs == 'p' = return (parseP l, B.tail bs') + | otherwise = seek (B.tail bs') + where (l, bs') = B.span ('\n' /=) bs + seek =<< B.readFile cnfFile + +-- | parses ByteString then injects the clauses in it into a solver +injectClausesFromCNF :: Solver -> CNFDescription -> B.ByteString -> IO () +injectClausesFromCNF s (CNFDescription nv nc _) bs = do + let maxLit = int2lit $ negate nv + buffer <- newVec (maxLit + 1) 0 + polvec <- newVec (maxLit + 1) 0 + 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 checkPolarity :: Int -> IO () + checkPolarity ((< nv) -> False) = return () + checkPolarity v = do + p <- getNth polvec $ var2lit v True + if p == LiftedF + then setAssign s v p + else do n <- getNth polvec $ var2lit v False + when (n == LiftedF) $ setAssign s v p + checkPolarity $ v + 1 + checkPolarity 1 + +{-# INLINE skipWhitespace #-} +skipWhitespace :: B.ByteString -> B.ByteString +skipWhitespace !s = B.dropWhile (`elem` " \t\n") s + +-- | skip comment lines +-- __Pre-condition:__ we are on the benngining of a line +{-# INLINE skipComments #-} +skipComments :: B.ByteString -> B.ByteString +skipComments !s + | c == 'c' = skipComments . B.tail . B.dropWhile (/= '\n') $ s + | otherwise = s + where + c = B.head s + +{-# INLINABLE parseInt #-} +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) + '0' -> (0, B.tail st) +-- '+' -> loop st (0 :: Int) + _ -> loop st 0 +-- c | '0' <= c && c <= '9' -> loop st 0 +-- _ -> error "PARSE ERROR! Unexpected char" + +{-# INLINABLE readClause #-} +readClause :: Solver -> Stack -> Vec Int -> B.ByteString -> IO B.ByteString +readClause s buffer bvec stream = do + let + loop :: Int -> B.ByteString -> IO B.ByteString + loop !i !b = case parseInt $ skipWhitespace b of + (0, b') -> do setNth buffer 0 $ i - 1 + sortStack buffer + void $ addClause s buffer + return b' + (k, b') -> case int2lit k of + l -> do setNth buffer i l + setNth bvec l LiftedT + loop (i + 1) b' + loop 1 . skipComments . skipWhitespace $ stream + +showPath :: FilePath -> String +showPath str = replicate (len - length basename) ' ' ++ if elem '/' str then basename else basename' + where + len = 50 + basename = reverse . takeWhile (/= '/') . reverse $ str + basename' = take len str diff --git a/src/SAT/Mios/Clause.hs b/src/SAT/Mios/Clause.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Clause.hs @@ -0,0 +1,129 @@ +-- | (This is a part of MIOS.) +-- Clause, supporting pointer-based equality +{-# LANGUAGE + FlexibleInstances + , MagicHash + , MultiParamTypeClasses + , RecordWildCards + , ViewPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Mios.Clause + ( + Clause (..) + , newClauseFromStack + -- * Vector of Clause + , ClauseVector + , newClauseVector + ) + where + +import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#) +import qualified Data.Vector as V +import qualified Data.Vector.Mutable as MV +-- import Data.List (intercalate) +import SAT.Mios.Types + +-- | __Fig. 7.(p.11)__ +-- normal, null (and binary) clause. +-- This matches both of @Clause@ and @GClause@ in MiniSat. +data Clause = Clause + { + rank :: !Int' -- ^ goodness like LBD; computed in 'Ranking' + , activity :: !Double' -- ^ activity of this clause +-- , protected :: !Bool' -- ^ protected from reduce + , lits :: !Stack -- ^ 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" + +-- | 'Clause' is a 'VecFamily' of 'Lit'. +instance VecFamily Clause Lit where + {-# SPECIALIZE INLINE getNth :: Clause -> Int -> IO Int #-} + getNth Clause{..} n = error "no getNth for Clause" + {-# SPECIALIZE INLINE setNth :: Clause -> Int -> Int -> IO () #-} + setNth Clause{..} n x = error "no setNth for Clause" + -- | returns a vector of literals in it. + asList NullClause = return [] + asList Clause{..} = take <$> get' lits <*> (tail <$> asList lits) + -- dump mes NullClause = return $ mes ++ "Null" + -- dump mes Clause{..} = return $ mes ++ "a clause" +{- + dump mes Clause{..} = do + a <- show <$> get' activity + n <- get' lits + l <- asList lits + return $ mes ++ "C" ++ show n ++ "{" ++ intercalate "," [show learnt, a, show (map lit2int l)] ++ "}" +-} + +-- | 'Clause' is a 'SingleStorage' on the number of literals in it. +instance SingleStorage Clause Int where + -- | returns the number of literals in a clause, even if the given clause is a binary clause + {-# SPECIALIZE INLINE get' :: Clause -> IO Int #-} + get' = get' . lits + -- getSize (BinaryClause _) = return 1 + -- | sets the number of literals in a clause, even if the given clause is a binary clause + {-# SPECIALIZE INLINE set' :: Clause -> Int -> IO () #-} + set' c n = set' (lits c) n + -- getSize (BinaryClause _) = return 1 + +-- | 'Clause' is a 'Stackfamily'on literals since literals in it will be discared if satisifed at level = 0. +instance StackFamily Clause Lit where + -- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals + {-# SPECIALIZE INLINE shrinkBy :: Clause -> Int -> IO () #-} + shrinkBy c n = modifyNth (lits c) (subtract n) 0 + +-- 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. +{-# INLINABLE newClauseFromStack #-} +newClauseFromStack :: Bool -> Stack -> IO Clause +newClauseFromStack l vec = do + n <- get' vec + v <- newStack n + let + loop ((<= n) -> False) = return () + loop i = (setNth v i =<< getNth vec i) >> loop (i + 1) + loop 0 + Clause <$> new' (if l then 1 else 0) <*> new' 0.0 {- <*> new' False -} <*> return v + +-------------------------------------------------------------------------------- Clause Vector + +-- | Mutable 'Clause' Vector +type ClauseVector = MV.IOVector Clause + +-- | 'ClauseVector' is a vector of 'Clause'. +instance VecFamily ClauseVector Clause where + {-# SPECIALIZE INLINE getNth :: ClauseVector -> Int -> IO Clause #-} + getNth = MV.unsafeRead + {-# SPECIALIZE INLINE setNth :: ClauseVector -> Int -> Clause -> IO () #-} + setNth = MV.unsafeWrite + {-# SPECIALIZE INLINE swapBetween :: ClauseVector -> Int -> Int -> IO () #-} + swapBetween = MV.unsafeSwap + asList cv = V.toList <$> V.freeze cv -- mapM (asList <=< getNth vec) [0 .. ???] +{- + 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 diff --git a/src/SAT/Mios/ClauseManager.hs b/src/SAT/Mios/ClauseManager.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/ClauseManager.hs @@ -0,0 +1,293 @@ +-- | (This is a part of MIOS.) +-- A shrinkable vector of 'C.Clause' +{-# LANGUAGE + BangPatterns + , FlexibleInstances + , MultiParamTypeClasses + , RecordWildCards + , ViewPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Mios.ClauseManager + ( + -- * higher level interface for ClauseVector + ClauseManager (..) + -- * Simple Clause Manager + , ClauseSimpleManager + -- * Manager with an extra Int (used as sort key or blocking literal) + , ClauseExtManager + , pushClauseWithKey + , getKeyVector + , markClause + -- * WatcherList + , WatcherList + , newWatcherList + , getNthWatcher + ) + where + +import Control.Monad (unless, when) +import qualified Data.IORef as IORef +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 vector of 'C.Clause'. +class ClauseManager a where + newManager :: Int -> IO a + getClauseVector :: a -> IO C.ClauseVector +-- removeClause :: a -> C.Clause -> IO () +-- removeNthClause :: a -> Int -> IO () + +-------------------------------------------------------------------------------- + +-- | Clause + Blocking Literal +data ClauseSimpleManager = ClauseSimpleManager + { + _numActives :: !Int' -- number of active clause + , _clsVector :: IORef.IORef C.ClauseVector -- clause list + } + +-- | 'ClauseSimpleManager' is a 'SingleStorage` on the number of clauses in it. +instance SingleStorage ClauseSimpleManager Int where + {-# SPECIALIZE INLINE get' :: ClauseSimpleManager -> IO Int #-} + get' m = get' (_numActives m) + {-# SPECIALIZE INLINE set' :: ClauseSimpleManager -> Int -> IO () #-} + set' m = set' (_numActives m) + +-- | 'ClauseSimpleManager' is a 'StackFamily` on clauses. +instance StackFamily ClauseSimpleManager C.Clause where + {-# SPECIALIZE INLINE shrinkBy :: ClauseSimpleManager -> Int -> IO () #-} + shrinkBy m k = modify' (_numActives m) (subtract k) + pushTo ClauseSimpleManager{..} c = do + -- checkConsistency m c + !n <- get' _numActives + !v <- IORef.readIORef _clsVector + if MV.length v - 1 <= n + then do + let len = max 8 $ MV.length v + v' <- MV.unsafeGrow v len + MV.unsafeWrite v' n c + IORef.writeIORef _clsVector v' + else MV.unsafeWrite v n c + modify' _numActives (1 +) + popFrom m = modify' (_numActives m) (subtract 1) + lastOf ClauseSimpleManager{..} = do + n <- get' _numActives + v <- IORef.readIORef _clsVector + MV.unsafeRead v (n - 1) + +-- | 'ClauseSimpleManager' is a 'ClauseManager' +instance ClauseManager ClauseSimpleManager where + -- | returns a new instance. + {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseSimpleManager #-} + newManager initialSize = do + i <- new' 0 + v <- C.newClauseVector initialSize + ClauseSimpleManager i <$> IORef.newIORef v + -- | returns the internal 'C.ClauseVector'. + {-# SPECIALIZE INLINE getClauseVector :: ClauseSimpleManager -> IO C.ClauseVector #-} + getClauseVector !m = IORef.readIORef (_clsVector m) + +-------------------------------------------------------------------------------- + +-- | Clause + Blocking Literal +data ClauseExtManager = ClauseExtManager + { + _nActives :: !Int' -- number of active clause + , _purged :: !Bool' -- whether it needs gc + , _clauseVector :: IORef.IORef C.ClauseVector -- clause list + , _keyVector :: IORef.IORef (Vec [Int]) -- Int list + } + +-- | 'ClauseExtManager' is a 'SingleStorage` on the number of clauses in it. +instance SingleStorage ClauseExtManager Int where + {-# SPECIALIZE INLINE get' :: ClauseExtManager -> IO Int #-} + get' m = get' (_nActives m) + {-# SPECIALIZE INLINE set' :: ClauseExtManager -> Int -> IO () #-} + set' m = set' (_nActives m) + +-- | 'ClauseExtManager' is a 'StackFamily` on clauses. +instance StackFamily ClauseExtManager C.Clause where + {-# SPECIALIZE INLINE shrinkBy :: ClauseExtManager -> Int -> IO () #-} + shrinkBy m k = modify' (_nActives m) (subtract k) + pushTo ClauseExtManager{..} c = do + -- checkConsistency m c + !n <- get' _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' <- growBy 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 + modify' _nActives (1 +) + popFrom m = modify' (_nActives m) (subtract 1) + lastOf ClauseExtManager{..} = do + n <- get' _nActives + v <- IORef.readIORef _clauseVector + MV.unsafeRead v (n - 1) + +-- | 'ClauseExtManager' is a 'ClauseManager' +instance ClauseManager ClauseExtManager where + -- | returns a new instance. + {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-} + newManager initialSize = do + i <- new' 0 + v <- C.newClauseVector initialSize + b <- newVec (MV.length v) 0 + ClauseExtManager i <$> new' False <*> IORef.newIORef v <*> IORef.newIORef b + -- | returns the internal 'C.ClauseVector'. + {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-} + getClauseVector !m = IORef.readIORef (_clauseVector m) +{- + -- | O(1) insertion function + pushClause !ClauseExtManager{..} !c = do + -- checkConsistency m c + !n <- get' _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' <- growBy 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 + modify' _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 <$> get' _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 + set' _nActives n + removeNthClause = error "removeNthClause is not implemented on ClauseExtManager" +-} + +-- | sets the expire flag to a clause. +{-# INLINABLE markClause #-} +markClause :: ClauseExtManager -> C.Clause -> IO () +markClause ClauseExtManager{..} c = do + !n <- get' _nActives + !v <- IORef.readIORef _clauseVector + let + seekIndex :: Int -> IO () + seekIndex k = do + -- assert (k < n) + 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 + set' _purged True + +{-# INLINABLE purifyManager #-} +purifyManager :: ClauseExtManager -> IO () +purifyManager ClauseExtManager{..} = do + diry <- get' _purged + when diry $ do + n <- get' _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 <- getNth vec i + if c /= C.NullClause + then do + unless (i == j) $ do + setNth vec j c + setNth keys j =<< getNth keys i + loop (i + 1) (j + 1) + else loop (i + 1) j + set' _nActives =<< loop 0 0 + set' _purged False + +-- | returns the associated Int vector, which holds /blocking literals/. +{-# INLINE getKeyVector #-} +getKeyVector :: ClauseExtManager -> IO (Vec [Int]) +getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector + +-- | O(1) inserter +{-# INLINABLE pushClauseWithKey #-} +pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO () +pushClauseWithKey ClauseExtManager{..} !c k = do + -- checkConsistency m c + !n <- get' _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' <- growBy 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 + modify' _nActives (1 +) + +-- | 'ClauseExtManager' is a collection of 'C.Clause' +instance VecFamily ClauseExtManager C.Clause where + getNth = error "no getNth method for ClauseExtManager" + setNth = error "no setNth method for ClauseExtManager" + {-# SPECIALIZE INLINE reset :: ClauseExtManager -> IO () #-} + reset m = set' (_nActives m) 0 +{- + dump mes ClauseExtManager{..} = do + n <- get' _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 + +-- | Immutable 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 +-- FIXME: sometimes n > 1M +newWatcherList :: Int -> Int -> IO WatcherList +newWatcherList n m = V.replicateM (int2lit (negate n) + 2) (newManager m) + +-- | returns the watcher List for "Literal" /l/. +{-# INLINE getNthWatcher #-} +getNthWatcher :: WatcherList -> Lit -> ClauseExtManager +getNthWatcher = V.unsafeIndex + +-- | 'WatcherList' is an 'Lit'-indexed collection of 'C.Clause'. +instance VecFamily WatcherList C.Clause where + getNth = error "no getNth method for WatcherList" -- getNthWatcher is a pure function + setNth = error "no setNth method for WatcherList" + {-# SPECIALIZE INLINE reset :: WatcherList -> IO () #-} + reset = V.mapM_ purifyManager +-- dump _ _ = (mes ++) . concat <$> mapM (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i)) [1 .. V.length wl - 1] diff --git a/src/SAT/Mios/ClausePool.hs b/src/SAT/Mios/ClausePool.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/ClausePool.hs @@ -0,0 +1,75 @@ +-- | (This is a part of MIOS.) +-- Recycling clauses +{-# LANGUAGE + ViewPatterns + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Mios.ClausePool + ( + ClausePool + , newClausePool + , makeClauseFromStack + , putBackToPool + ) + where + +import Control.Monad (when) +import qualified Data.Vector as V +import SAT.Mios.Vec +import SAT.Mios.Clause +import qualified SAT.Mios.ClauseManager as CM + +-- | an immutable Vector of 'ClauseSimpleManager' +type ClausePool = V.Vector CM.ClauseSimpleManager + +-- | biclause should be stored into index:0, so the real limit is 64. +storeLimit :: Int +storeLimit = 62 + +-- | returns a new 'ClausePool' +newClausePool ::Int -> IO ClausePool +newClausePool n = V.fromList <$> mapM (\_ -> CM.newManager n) [0 .. storeLimit] + +-- | returns 'CM.ClauseManager' for caluses which have suitable sizes. +{-# INLINE getManager #-} +getManager :: ClausePool -> Int -> CM.ClauseSimpleManager +getManager p n = V.unsafeIndex p n + +-- | If a nice candidate as a learnt is stored, return it. +-- Otherwise allocate a new clause in heap then return it. +{-# INLINABLE makeClauseFromStack #-} +makeClauseFromStack :: ClausePool -> Stack -> IO Clause +makeClauseFromStack pool v = do + let pickup :: Int -> IO Clause + pickup ((<= storeLimit) -> False) = return NullClause + pickup i = do + let mgr = getManager pool i + nn <- get' mgr + if 0 < nn + then do c <- lastOf mgr + popFrom mgr + return c + else pickup $ i + 1 + n <- get' v + c <- pickup (n - 2) + if c == NullClause + then newClauseFromStack True v + else do let lstack = lits c + loop :: Int -> IO () + loop ((<= n) -> False) = return () + loop i = (setNth lstack i =<< getNth v i) >> loop (i + 1) + loop 0 + -- the caller (newLearntClause) should set these slots + -- - rank + -- - protected + set' (activity c) 0.0 + return c + +-- | Note: only not-too-large and learnt clauses are recycled. +{-# INLINE putBackToPool #-} +putBackToPool :: ClausePool -> Clause -> IO () +putBackToPool pool c = do + l <- get' (rank c) + when (0 /= l) $ do let n = realLengthOfStack (lits c) - 3 + when (n <= storeLimit) $ pushTo (getManager pool n) c diff --git a/src/SAT/Mios/Criteria.hs b/src/SAT/Mios/Criteria.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Criteria.hs @@ -0,0 +1,327 @@ +-- | (This is a part of MIOS.) +-- Advanced heuristics library for 'SAT.Mios.Main' +{-# LANGUAGE + MultiWayIf + , RecordWildCards + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +module SAT.Mios.Criteria + ( + -- * Activities + claBumpActivity + , claDecayActivity + , varBumpActivity + , varDecayActivity + -- * Clause + , addClause + -- * Literal Block Distance + , lbdOf + -- * Restart + , checkRestartCondition + ) + where + +import Control.Monad (when) +import SAT.Mios.Types +import SAT.Mios.Clause +import SAT.Mios.ClauseManager +import SAT.Mios.Solver + +-------------------------------------------------------------------------------- Activities + +varActivityThreshold :: Double +varActivityThreshold = 1e100 + +-- | __Fig. 14 (p.19)__ Bumping of clause activity +{-# INLINE varBumpActivity #-} +varBumpActivity :: Solver -> Var -> IO () +varBumpActivity s@Solver{..} x = do + a <- (+) <$> getNth activities x <*> get' varInc + setNth activities x a + when (varActivityThreshold < a) $ varRescaleActivity s + update s x -- update the position in heap + +-- | __Fig. 14 (p.19)__ +{-# INLINABLE varDecayActivity #-} +varDecayActivity :: Solver -> IO () +varDecayActivity Solver{..} = modify' varInc (/ variableDecayRate config) + +-- | __Fig. 14 (p.19)__ +{-# INLINABLE varRescaleActivity #-} +varRescaleActivity :: Solver -> IO () +varRescaleActivity Solver{..} = do + let + loop ((<= nVars) -> False) = return () + loop i = modifyNth activities (/ varActivityThreshold) i >> loop (i + 1) + loop 1 + modify' varInc (/ varActivityThreshold) + +-- | value for rescaling clause activity. +claActivityThreshold :: Double +claActivityThreshold = 1e20 + +-- | __Fig. 14 (p.19)__ +{-# INLINE claBumpActivity #-} +claBumpActivity :: Solver -> Clause -> IO () +claBumpActivity s@Solver{..} Clause{..} = do + a <- (+) <$> get' activity <*> get' claInc + set' activity a + when (claActivityThreshold <= a) $ claRescaleActivity s + +-- | __Fig. 14 (p.19)__ +{-# INLINE claDecayActivity #-} +claDecayActivity :: Solver -> IO () +claDecayActivity Solver{..} = modify' claInc (/ clauseDecayRate config) + +-- | __Fig. 14 (p.19)__ +{-# INLINABLE claRescaleActivity #-} +claRescaleActivity :: Solver -> IO () +claRescaleActivity Solver{..} = do + vec <- getClauseVector learnts + n <- get' learnts + let + loopOnVector :: Int -> IO () + loopOnVector ((< n) -> False) = return () + loopOnVector i = do + c <- getNth vec i + modify' (activity c) (/ claActivityThreshold) + loopOnVector $ i + 1 + loopOnVector 0 + modify' claInc (/ claActivityThreshold) + +{- +-- | __Fig. 14 (p.19)__ +{-# INLINABLE claRescaleActivityAfterRestart #-} +claRescaleActivityAfterRestart :: Solver -> IO () +claRescaleActivityAfterRestart Solver{..} = do + vec <- getClauseVector learnts + n <- get' learnts + let + loopOnVector :: Int -> IO () + loopOnVector ((< n) -> False) = return () + loopOnVector i = do + c <- getNth vec i + d <- get' c + if d < 9 + then modify' (activity c) sqrt + else set' (activity c) 0 + -- set' (protected c) False + loopOnVector $ i + 1 + loopOnVector 0 +-} + +-------------------------------------------------------------------------------- ClauseNew + +-- | __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.) +-- +-- * @Left False@ if the clause is in a confilct +-- * @Left True@ if the clause is satisfied +-- * @Right clause@ if the clause is enqueued successfully +{-# INLINABLE clauseNew #-} +clauseNew :: Solver -> Stack -> Bool -> IO (Either 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 + if | y == l -> do -- finds a duplicate + swapBetween ps j n + modifyNth ps (subtract 1) 0 + handle j l (n - 1) + | - y == l -> reset ps >> return True -- p and negateLit p occurs in ps + | otherwise -> handle (j + 1) l n + loopForLearnt :: Int -> IO Bool + loopForLearnt i = do + n <- get' ps + 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 <- get' ps + 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 -> reset ps >> 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 <- get' ps + case k of + 0 -> return (Left exit) + 1 -> do + l <- getNth ps 1 + Left <$> enqueue s l NullClause + _ -> do + -- allocate clause: + c <- newClauseFromStack isLearnt ps + let lstack = lits 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 lstack i + varBumpActivity s v' -- this is a just good chance to bump activities of literals in this clause + 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 1 1 0 + swapBetween lstack 2 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 + -- Add clause to watcher lists: + l1 <- getNth lstack 1 + l2 <- getNth lstack 2 + pushClauseWithKey (getNthWatcher watches (negateLit l1)) c 0 + pushClauseWithKey (getNthWatcher watches (negateLit l2)) c 0 + return (Right c) + +-- | 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 -> Stack -> IO Bool +addClause s@Solver{..} vecLits = do + result <- clauseNew s vecLits False + case result of + Left b -> return b -- No new clause was returned becaues a confilct occured or the clause is a literal + Right c -> pushTo clauses c >> return True + +-------------------------------------------------------------------------------- LBD + +-- | returns a POSIVITE value +{-# INLINABLE lbdOf #-} +lbdOf :: Solver -> Stack -> IO Int +lbdOf Solver{..} vec = do + k <- (\k -> if 1000000 < k then 1 else k + 1) <$> get' lbd'key + set' lbd'key k -- store the last used value + nv <- getNth vec 0 + let loop :: Int -> Int -> IO Int + loop ((<= nv) -> False) n = return $ max 1 n + loop i n = do l <- getNth level . lit2var =<< getNth vec i + x <- getNth lbd'seen l + if x /= k && l /= 0 + then setNth lbd'seen l k >> loop (i + 1) (n + 1) + else loop (i + 1) n + loop 1 0 + +{- +{-# INLINE setLBD #-} +setLBD :: Solver -> Clause -> IO () +setLBD _ NullClause = error "LBD44" +setLBD s c = set' (rank c) =<< lbdOf s (lits c) + +-- | update the lbd field of /c/ +{-# INLINE updateLBD #-} +updateLBD :: Solver -> Clause -> IO () +updateLBD s NullClause = error "LBD71" +updateLBD s c@Clause{..} = do + k <- get' c +-- o <- getInt lbd + n <- lbdOf s lits + case () of + _ | n == 1 -> set' rank (k - 1) + -- _ | n < o -> setInt lbd n + _ -> return () +-} + +-------------------------------------------------------------------------------- restart + +ema1, ema2, ema3, ema4 :: Double +ema1 = 2 ** (-5) -- coefficient for fast average of LBD +ema2 = 2 ** (-14) -- coefficient for slow average of LBD +ema3 = 2 ** (-5) -- coefficient for fast average of | assignment | +ema4 = 2 ** (-12) -- coefficient for slow average of | assignment | + +ema0 :: Int +ema0 = 2 ^ (14 :: Int) -- = floor $ 1 / ema2 + +-- | #62 +checkRestartCondition :: Solver -> Int -> IO Bool +checkRestartCondition s@Solver{..} (fromIntegral -> lbd) = do + k <- getStat s NumOfRestart + let step = 100 + next <- get' nextRestart + count <- getStat s NumOfBackjump + nas <- fromIntegral <$> nAssigns s + let revise a f x = do f' <- ((a * x) +) . ((1 - a) *) <$> get' f + set' f f' + return f' + gef = 1.1 :: Double -- geometric expansion factor + df <- revise ema1 emaDFast lbd + ds <- revise ema2 emaDSlow lbd + af <- revise ema3 emaAFast nas + as <- revise ema4 emaASlow nas + mode <- get' restartMode + if | count < next -> return False + | mode == 1 -> do + when (ema0 < count && df < 2.0 * ds) $ set' restartMode 2 -- enter the second mode + incrementStat s NumOfRestart 1 + incrementStat s NumOfGeometricRestart 1 + k' <- getStat s NumOfGeometricRestart + set' nextRestart (count + floor (fromIntegral step * gef ** fromIntegral k')) + when (3 == dumpStat config) $ dumpSolver DumpCSV s + return True + | 1.25 * as < af -> do + incrementStat s NumOfBlockRestart 1 + set' nextRestart (count + floor (fromIntegral step + gef ** fromIntegral k)) + when (3 == dumpStat config) $ dumpSolver DumpCSV s + return False + | 1.25 * ds < df -> do + incrementStat s NumOfRestart 1 + set' nextRestart (count + step) + when (3 == dumpStat config) $ dumpSolver DumpCSV s + return True + | otherwise -> return False + +{- +{-# INLINABLE luby #-} +luby :: Double -> Int -> Double +luby y x_ = loop 1 0 + where + loop :: Int -> Int -> Double + loop sz sq + | sz < x_ + 1 = loop (2 * sz + 1) (sq + 1) + | otherwise = loop2 x_ sz sq + loop2 :: Int -> Int -> Int -> Double + loop2 x sz sq + | sz - 1 == x = y ** fromIntegral sq + | otherwise = let s = div (sz - 1) 2 in loop2 (mod x s) s (sq - 1) +-} diff --git a/src/SAT/Mios/Main.hs b/src/SAT/Mios/Main.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Main.hs @@ -0,0 +1,759 @@ +-- | (This is a part of MIOS.) +-- Main part of solving satisfiability problem. +{-# LANGUAGE + BangPatterns + , MultiWayIf + , RecordWildCards + , ScopedTypeVariables + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +module SAT.Mios.Main + ( + -- * Interface to 'Solver', imported from 'SAT.Mios.Criteria' + Solver + , newSolver + , setAssign + , addClause + , dumpSolver + -- * Main function + , simplifyDB + , solve + ) + where + +import Control.Monad (unless, void, when) +import Data.Bits +import Data.Foldable (foldrM) +import Data.Int +import SAT.Mios.Types +import SAT.Mios.Clause +import SAT.Mios.ClauseManager +import SAT.Mios.Solver +import SAT.Mios.ClausePool +import SAT.Mios.Criteria + +-- | #114: __RemoveWatch__ +{-# INLINABLE removeWatch #-} +removeWatch :: Solver -> Clause -> IO () +removeWatch Solver{..} c = do + let lstack = lits c + l1 <- negateLit <$> getNth lstack 1 + markClause (getNthWatcher watches l1) c + l2 <- negateLit <$> getNth lstack 2 + markClause (getNthWatcher watches l2) c + putBackToPool clsPool c + +-------------------------------------------------------------------------------- +-- Operations on 'Clause' +-------------------------------------------------------------------------------- + +-- | __Fig. 8. (p.12)__ creates a new LEARNT clause and adds it to watcher lists. +-- This is a strippped-down version of 'newClause' in Solver. +newLearntClause :: Solver -> Stack -> IO Int +newLearntClause s@Solver{..} ps = 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 <- get' ps + case k of + 1 -> do l <- getNth ps 1 + unsafeEnqueue s l NullClause + return 1 + _ -> do c <- makeClauseFromStack clsPool ps -- newClauseFromStack True ps + let lstack = lits c + findMax :: Int -> Int -> Int -> IO Int -- Pick a second literal to watch: + findMax ((<= k) -> False) j _ = return j + findMax i j val = do + v <- lit2var <$> getNth lstack 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 lstack 2 =<< findMax 1 1 0 -- Let @max_i@ be the index of the literal with highest decision level + -- Bump, enqueue, store clause: + claBumpActivity s c + -- Add clause to all managers + pushTo learnts c + l1 <- getNth lstack 1 + l2 <- getNth lstack 2 + pushClauseWithKey (getNthWatcher watches (negateLit l1)) c l2 + pushClauseWithKey (getNthWatcher watches (negateLit l2)) c l1 + -- update the solver state by @l@ + unsafeEnqueue s l1 c + -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue + lbd <- lbdOf s (lits c) + set' (rank c) lbd + -- assert (0 < rank c) + -- set' (protected c) True + return lbd + +-- | __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 <- get' c + let lstack = lits c + loop ::Int -> IO Bool + loop ((<= n) -> False) = return False + loop i = do v <- valueLit s =<< getNth lstack i + if v == 1 then return True else loop (i + 1) + loop 1 + +-------------------------------------------------------------------------------- +-- 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@ +analyze :: Solver -> Clause -> IO Int +analyze s@Solver{..} confl = do + -- litvec + reset litsLearnt + pushTo litsLearnt 0 -- reserve the first place for the unassigned literal + dl <- decisionLevel s + let loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int + loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level + d <- get' (rank c) + when (0 /= d) $ claBumpActivity s c + -- update LBD like #Glucose4.0 + when (2 < d) $ do + nblevels <- lbdOf s (lits c) + when (nblevels + 1 < d) $ -- improve the LBD + -- when (d <= 30) $ set' (protected c) True -- 30 is `lbLBDFrozenClause` + -- seems to be interesting: keep it fro the next round + set' (rank c) nblevels -- Update it + sc <- get' c + let lstack = lits 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 lstack 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 + -- UPDATEVARACTIVITY: glucose heuristics + r <- getNth reason v + when (r /= NullClause) $ do + ra <- get' (rank r) + when (0 /= ra) $ pushTo an'lastDL q + -- end of glucose heuristics + loopOnLiterals (j + 1) b (pc + 1) + else pushTo litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc + else loopOnLiterals (j + 1) b pc + (b', pathC') <- loopOnLiterals (if p == bottomLit then 1 else 2) bl pathC + let nextPickedUpLit :: Int -> IO Int -- select next clause to look at + nextPickedUpLit i = do x <- getNth an'seen . lit2var =<< getNth trail i + if x == 0 then nextPickedUpLit (i - 1) else return (i - 1) + ti' <- nextPickedUpLit (ti + 1) + nextP <- getNth trail (ti' + 1) + let nextV = lit2var nextP + confl' <- getNth reason nextV + setNth an'seen nextV 0 + if 1 < pathC' + then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1) + else setNth litsLearnt 1 (negateLit nextP) >> return b' + ti <- subtract 1 <$> get' trail + levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0 + -- Simplify phase (implemented only @expensive_ccmin@ path) + n <- get' litsLearnt + reset an'stack -- analyze_stack.clear(); + reset an'toClear -- out_learnt.copyTo(analyze_toclear); + pushTo an'toClear =<< getNth litsLearnt 1 + let merger :: Int -> Int64 -> IO Int64 + merger ((<= n) -> False) b = return b + merger i b = do l <- getNth litsLearnt i + pushTo an'toClear l + -- restrict the search depth (range) to 63 + merger (i + 1) . setBit b . (63 .&.) =<< getNth level (lit2var l) + levels <- merger 2 0 + let loopOnLits :: Int -> Int -> IO () + loopOnLits ((<= n) -> False) n' = shrinkBy litsLearnt $ n - n' + 1 + loopOnLits i j = do + l <- getNth litsLearnt i + c1 <- (NullClause ==) <$> getNth reason (lit2var l) + if c1 + then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1) + else do + c2 <- not <$> analyzeRemovable s l levels + if c2 + then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1) + else loopOnLits (i + 1) j + loopOnLits 2 2 -- the first literal is specail + -- UPDATEVARACTIVITY: glucose heuristics + nld <- get' an'lastDL + r <- get' litsLearnt -- this is an estimated LBD value based on the clause size + let loopOnLastDL :: Int -> IO () + loopOnLastDL ((<= nld) -> False) = return () + loopOnLastDL i = do v <- lit2var <$> getNth an'lastDL i + r' <- get' =<< getNth reason v + when (r < r') $ varBumpActivity s v + loopOnLastDL $ i + 1 + loopOnLastDL 1 + reset an'lastDL + -- Clear seen + k <- get' an'toClear + let cleaner :: Int -> IO () + cleaner ((<= k) -> False) = return () + cleaner i = do v <- lit2var <$> getNth an'toClear i + setNth an'seen v 0 + cleaner $ i + 1 + cleaner 1 + 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@. +-- +analyzeRemovable :: Solver -> Lit -> Int64 -> IO Bool +analyzeRemovable Solver{..} p minLevel = do + -- assert (reason[var(p)] != NullClause); + reset an'stack -- analyze_stack.clear() + pushTo an'stack p -- analyze_stack.push(p); + top <- get' an'toClear + let + loopOnStack :: IO Bool + loopOnStack = do + k <- get' an'stack -- int top = analyze_toclear.size(); + if 0 == k + then return True + else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL); + sl <- lastOf an'stack + popFrom an'stack -- analyze_stack.pop(); + c <- getNth reason (lit2var sl) -- getRoot sl + nl <- get' c + let + lstack = lits c + loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){ + loopOnLit ((<= nl) -> False) = loopOnStack + loopOnLit i = do + p' <- getNth lstack i -- valid range is [1 .. nl] + 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 /=) <$> getNth reason v' + if c3 && testBit minLevel (l' .&. 63) -- 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; + pushTo an'stack p' -- analyze_stack.push(p); + pushTo an'toClear p' -- analyze_toclear.push(p); + loopOnLit $ i + 1 + else do + -- for (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0; + top' <- get' an'toClear + let clearAll :: Int -> IO () + clearAll ((<= top') -> False) = return () + clearAll j = do x <- getNth an'toClear j; setNth an'seen (lit2var x) 0; clearAll (j + 1) + clearAll $ top + 1 + -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop + shrinkBy an'toClear $ top' - top + return False + else loopOnLit $ i + 1 + loopOnLit 2 + 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 + reset conflicts + rl <- get' rootLevel + unless (rl == 0) $ do + n <- get' confl + let lstack = lits confl + loopOnConfl :: Int -> IO () + loopOnConfl ((<= n) -> False) = return () + loopOnConfl i = do + (x :: Var) <- lit2var <$> getNth lstack i + lvl <- getNth level x + when (0 < lvl) $ setNth an'seen x 1 + loopOnConfl $ i + 1 + loopOnConfl $ if skipFirst then 2 else 1 + tls <- get' trailLim + trs <- get' trail + tlz <- getNth trailLim 1 + let loopOnTrail :: Int -> IO () + loopOnTrail ((tlz <=) -> False) = return () + loopOnTrail i = do + (l :: Lit) <- getNth trail (i + 1) + let (x :: Var) = lit2var l + saw <- getNth an'seen x + when (saw == 1) $ do + (r :: Clause) <- getNth reason x + if r == NullClause + then pushTo conflicts (negateLit l) + else do + k <- get' r + let lstack' = lits r + loopOnLits :: Int -> IO () + loopOnLits ((<= k) -> False) = return () + loopOnLits j = do + (v :: Var) <- lit2var <$> getNth lstack' j + lv <- getNth level v + when (0 < lv) $ setNth an'seen v 1 + loopOnLits $ i + 1 + loopOnLits 2 + setNth an'seen x 0 + loopOnTrail $ i - 1 + loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth trailLim (rl + 1) + +-- | 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` +propagate :: Solver -> IO Clause +propagate s@Solver{..} = do + let + while :: Clause -> Bool -> IO Clause + while confl False = return confl + while confl True = do + (p :: Lit) <- getNth trail . (1 +) =<< get' qHead + modify' qHead (+ 1) + incrementStat s NumOfPropagation 1 + let (ws :: ClauseExtManager) = getNthWatcher watches p + !falseLit = negateLit p + end <- get' ws + cvec <- getClauseVector ws + bvec <- getKeyVector ws + let copy :: Int -> Int -> IO () + copy ((< end) -> False) _ = return () + copy !i' !j' = do setNth cvec j' =<< getNth cvec i' + setNth bvec j' =<< getNth bvec i' + copy (i' + 1) (j' + 1) + let forClause :: Int -> Int -> IO Clause + forClause i@((< end) -> False) !j = shrinkBy ws (i - j) >> return confl + forClause !i !j = do + (blocker :: Lit) <- getNth bvec i -- Try to avoid inspecting the clause: + bv <- if blocker == 0 then return LiftedF else valueLit s blocker + if bv == LiftedT + then do unless (i == j) $ do (c :: Clause) <- getNth cvec i + setNth cvec j c + setNth bvec j blocker + forClause (i + 1) (j + 1) + else do -- Make sure the false literal is data[1]: + (c :: Clause) <- getNth cvec i + let !lstack = lits c + tmp <- getNth lstack 1 + first <- if falseLit == tmp + then do l2 <- getNth lstack 2 + setNth lstack 2 tmp + setNth lstack 1 l2 + return l2 + else return tmp + fv <- valueLit s first + if fv == LiftedT + then do unless (i == j) $ setNth cvec j c + setNth bvec j first + forClause (i + 1) (j + 1) + else do cs <- get' c -- Look for new watch: + let newWatch :: Int -> IO LiftedBool + newWatch ((<= cs) -> False) = do -- Did not find watch + setNth cvec j c + setNth bvec j first + if fv == LiftedF + then do ((== 0) <$> decisionLevel s) >>= (`when` set' ok LiftedF) + set' qHead =<< get' trail + copy (i + 1) (j + 1) + return LiftedF -- conflict + else do unsafeEnqueue s first c + return LBottom -- unit clause + newWatch !k = do (l' :: Lit) <- getNth lstack k + lv <- valueLit s l' + if lv /= LiftedF + then do setNth lstack 2 l' + setNth lstack k falseLit + pushClauseWithKey (getNthWatcher watches (negateLit l')) c first + return LiftedT -- found another watch + else newWatch $! k + 1 + ret <- newWatch 3 + case ret of + LiftedT -> forClause (i + 1) j -- found another watch + LBottom -> forClause (i + 1) (j + 1) -- unit clause + _ -> shrinkBy ws (i - j) >> return c -- conflict + c <- forClause 0 0 + while c =<< ((<) <$> get' qHead <*> get' trail) + while NullClause =<< ((<) <$> get' qHead <*> get' 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. +reduceDB :: Solver -> IO () +reduceDB s@Solver{..} = do + n <- nLearnts s + cvec <- getClauseVector learnts + let loop :: Int -> IO () + loop ((< n) -> False) = return () + loop i = do + removeWatch s =<< getNth cvec i + loop $ i + 1 + k <- sortClauses s learnts $ div n 2 -- k is the number of clauses not to be purged +{- + -- #GLUCOSE3.0 keep more + t3 <- get' . rank =<< getNth vec (thr -1) + t5 <- get' . rank =<< getNth vec (lim -1) + + let k = case (t3 <= 3, t5 <= 5) of + (True, True) -> min n (thr + 2000) + (False, False) -> thr + (_, _) -> min n (thr + 1000) + -- let k = div thr 2 +-} + loop k -- CAVEAT: `vec` is a zero-based vector + -- putStrLn $ "reduceDB: purge " ++ show (n - k) ++ " out of " ++ show n + reset watches + shrinkBy learnts (n - k) + incrementStat s NumOfReduction 1 + +-- constants for sort key layout +rankWidth :: Int +rankWidth = 10 +activityWidth :: Int +activityWidth = 50 -- note: the maximum clause activity is 1e20. +indexWidth :: Int +indexWidth = 32 -- 4G +rankMax :: Int +rankMax = 2 ^ rankWidth - 1 +activityMax :: Int +activityMax = 2 ^ activityWidth - 1 +indexMax :: Int +indexMax = 2 ^ indexWidth - 1 + +-- | applies a (good to bad) quick semi-sort to the vector in a 'ClauseExtManager' +-- and returns the number of privileged clauses. +-- This function uses the same criteria as reduceDB_lt in glucose 4.0: +-- 1. binary clause +-- 2. smaller LBD +-- 3. larger activity defined as MiniSat +-- +-- they are encoded into two "Int64"s as the following (10+52+32 layout): +-- +-- * 10 bits for rank (LBD): 'rankWidth' +-- * 50 bits for converted activity: 'activityWidth' +-- * 32 bits for clauseVector index: 'indexWidth' +-- +sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int +sortClauses s cm limit' = do + n <- get' cm + -- assert (n < indexMax) + vec <- getClauseVector cm + bvec <- getKeyVector cm + keys <- newVec (2 * n) 0 :: IO (Vec Int) + at <- (0.1 *) . (/ fromIntegral n) <$> get' (claInc s) -- activity threshold + -- 1: assign keys + let shiftLBD = activityWidth + shiftIndex = shiftL 1 indexWidth + am = fromIntegral activityMax :: Double + scaleAct :: Double -> Int + scaleAct x + | x < 1e-20 = activityMax + | otherwise = floor $ am * (1 - logBase 10 (x * 1e20) / 40) + assignKey :: Int -> Int -> IO Int + assignKey ((< n) -> False) t = return t + assignKey i t = do + setNth keys (2 * i + 1) $ shiftIndex + i + c <- getNth vec i + k <- get' c + if k == 2 -- Main criteria. Like in MiniSat we keep all binary clauses + then do setNth keys (2 * i) 0 + assignKey (i + 1) (t + 1) + else do a <- get' (activity c) -- Second one... based on LBD + r <- get' (rank c) + l <- locked s c + let d =if | l -> 0 + | a < at -> rankMax + | otherwise -> min rankMax r -- rank can be one + setNth keys (2 * i) $ shiftL d shiftLBD + scaleAct a + assignKey (i + 1) $ if l then t + 1 else t + limit <- max limit' <$> assignKey 0 0 + -- 2: sort keyVector + let limit2 = 2 * limit + sortOnRange :: Int -> Int -> IO () + sortOnRange left right + | limit2 < left = return () + | left >= right = return () + | left + 2 == right = do + a <- getNth keys left + b <- getNth keys right + unless (a < b) $ do swapBetween keys left right + swapBetween keys (left + 1) (right + 1) + | otherwise = do + let p = 2 * div (left + right) 4 + pivot <- getNth keys p + swapBetween keys p left -- set a sentinel for r' + swapBetween keys (p + 1) (left + 1) + let nextL :: Int -> IO Int + nextL i@((<= right) -> False) = return i + nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 2) else return i + nextR :: Int -> IO Int + nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 2) else return i + divide :: Int -> Int -> IO Int + divide l r = do + l' <- nextL l + r' <- nextR r + if l' < r' + then do swapBetween keys l' r' + swapBetween keys (l' + 1) (r' + 1) + divide (l' + 2) (r' - 2) + else return r' + m <- divide (left + 2) right + swapBetween keys left m + swapBetween keys (left + 1) (m + 1) + sortOnRange left (m - 2) + sortOnRange (m + 2) right + sortOnRange 0 $ 2 * (n - 1) + -- 3: place clauses in 'vec' based on the order stored in 'keys'. + -- To recycle existing clauses, we must reserve all clauses for now. + let seek :: Int -> IO () + seek ((< n) -> False) = return () + seek i = do + bits <- getNth keys (2 * i + 1) + when (indexMax < bits) $ do + c <- getNth vec i + d <- getNth bvec i + -- setNth keys i i + let sweep k = do k' <- (indexMax .&.) <$> getNth keys (2 * k + 1) + setNth keys (2 * k + 1) (indexMax .&. k) + if k' == i + then do setNth vec k c + setNth bvec k d + else do getNth vec k' >>= setNth vec k + getNth bvec k' >>= setNth bvec k + sweep k' + sweep i -- (indexMax .&. bits) + 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. +-- +simplifyDB :: Solver -> IO Bool +simplifyDB s@Solver{..} = do + good <- (LiftedT ==) <$> get' ok + if good + then do + p <- propagate s + if p /= NullClause + then set' ok LiftedF >> return False + else do + -- Remove satisfied clauses and their watcher lists: + let + for :: ClauseExtManager -> IO () + for mgr = do + vec' <- getClauseVector mgr + n' <- get' mgr + let + loopOnVector :: Int -> Int -> IO () + loopOnVector ((< n') -> False) j = shrinkBy mgr (n' - j) + loopOnVector i j = do + c <- getNth vec' i + l <- locked s c + r <- if l then return False else simplify s c + if r + then removeWatch s c >> loopOnVector (i + 1) j + else unless (i == j) (setNth vec' j c) >> loopOnVector (i + 1) (j + 1) + loopOnVector 0 0 + for clauses + for learnts + reset watches + return True + 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:__ +-- * '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. +-- * 'False' if the clause set is unsatisfiable or some error occured. +search :: Solver -> IO Bool +search s@Solver{..} = do + -- clear model + let loop :: Bool -> IO Bool + loop restart = do + confl <- propagate s + d <- decisionLevel s + if confl /= NullClause -- CONFLICT + then do incrementStat s NumOfBackjump 1 + r <- get' rootLevel + if d == r -- Contradiction found: + then analyzeFinal s confl False >> return False + else do backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself + (s `cancelUntil`) . max backtrackLevel =<< get' rootLevel + lbd' <- newLearntClause s litsLearnt + k <- get' litsLearnt + when (k == 1) $ do + (v :: Var) <- lit2var <$> getNth litsLearnt 1 + setNth level v 0 + varDecayActivity s + claDecayActivity s + -- learnt DB Size Adjustment + modify' learntSCnt (subtract 1) + cnt <- get' learntSCnt + when (cnt == 0) $ do + t' <- (* 1.5) <$> get' learntSAdj + set' learntSAdj t' + set' learntSCnt $ floor t' + -- modify' maxLearnts (* 1.1) + modify' maxLearnts (+ 300) + loop =<< checkRestartCondition s lbd' + else do when (d == 0) . void $ simplifyDB s -- Simplify the set of problem clauses + k1 <- get' learnts + k2 <- nAssigns s + nl <- floor <$> get' maxLearnts + when (nl < k1 - k2) $ do + reduceDB s -- Reduce the set of learnt clauses. + when (2 == dumpStat config) $ dumpSolver DumpCSV s + if | k2 == nVars -> return True -- Model found + | restart -> do -- Reached bound on number of conflicts + (s `cancelUntil`) =<< get' rootLevel -- force a restart + -- claRescaleActivityAfterRestart s +{- + let toggle :: Int -> Int + toggle LiftedT = LiftedF + toggle LiftedF = LiftedT + toggle x = x + nv = nVars + toggleAt :: Int -> IO () + toggleAt ((<= nv) -> False) = return () + toggleAt i = modifyNth phases toggle i >> toggleAt (i + 1) + rm <- get' restartMode + when (rm == 1) $ toggleAt 1 +-} + loop False + | otherwise -> do -- New variable decision + v <- select s + -- #phasesaving <<<< many have heuristic for polarity here + oldVal <- getNth phases v + unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@ + -- #phasesaving >>>> + loop False + loop False + +-- | __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 SolverResult +solve s@Solver{..} assumps = do + -- PUSH INCREMENTAL ASSUMPTIONS: + let inject :: Lit -> Bool -> IO Bool + inject _ False = return False + inject a True = do + b <- assume s a + if not b -- conflict analyze + then do (confl :: Clause) <- getNth reason (lit2var a) + analyzeFinal s confl True + pushTo conflicts (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 inject True assumps else return False + if x + then do set' rootLevel =<< decisionLevel s + status <- search s + -- post-proccesing should be done here + let toInt :: Var -> IO Lit + toInt v = (\p -> if LiftedT == p then v else negate v) <$> valueVar s v + asg1 <- mapM toInt [1 .. nVars] + asg2 <- map lit2int <$> asList conflicts + when (0 < dumpStat config) $ dumpSolver DumpCSV s + cancelUntil s 0 -- reset solver + flag <- get' ok + if | status && flag == LiftedT -> return $ Right (SAT asg1) + | not status && flag == LiftedF -> return $ Right (UNSAT asg2) + | otherwise -> return $ Left InternalInconsistent + else return $ Right (UNSAT []) + +-- | Though '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 $ lit2lbool p + setNth level v =<< decisionLevel s + setNth reason v from -- NOTE: @from@ might be NULL! + pushTo trail p + +-- | __Pre-condition:__ propagation queue is empty. +{-# INLINE unsafeAssume #-} +unsafeAssume :: Solver -> Lit -> IO () +unsafeAssume s@Solver{..} p = do + pushTo trailLim =<< get' trail + unsafeEnqueue s p NullClause diff --git a/src/SAT/Mios/OptionParser.hs b/src/SAT/Mios/OptionParser.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/OptionParser.hs @@ -0,0 +1,145 @@ +-- | (This is a part of MIOS.) +-- Command line option parser +{-# LANGUAGE Safe #-} + +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.Types (MiosConfiguration (..), defaultConfiguration) + +-- | configuration swithces +data MiosProgramOption = MiosProgramOption + { + _targetFile :: Maybe String + , _targets :: [String] + , _outputFile :: Maybe String + , _confVariableDecayRate :: !Double + , _confClauseDecayRate :: Double +-- , _confRandomDecisionRate :: Int + , _confMaxSize :: !Int + , _confCheckAnswer :: !Bool + , _confVerbose :: !Bool + , _confBenchmark :: Integer + , _confBenchSeq :: !Int + , _confNoAnswer :: !Bool + , _confDumpStat :: !Int + , _validateAssignment :: !Bool + , _displayHelp :: !Bool + , _displayVersion :: !Bool + } + +-- | default option settings +miosDefaultOption :: MiosProgramOption +miosDefaultOption = MiosProgramOption + { + _targetFile = Nothing + , _targets = [] + , _outputFile = Nothing + , _confVariableDecayRate = variableDecayRate defaultConfiguration + , _confClauseDecayRate = clauseDecayRate defaultConfiguration +-- , _confRandomDecisionRate = randomDecisionRate defaultConfiguration + , _confMaxSize = 4000000 -- 4,000,000 = 4M + , _confCheckAnswer = False + , _confVerbose = False + , _confBenchmark = -1 + , _confBenchSeq = 0 + , _confNoAnswer = False + , _confDumpStat = dumpStat defaultConfiguration + , _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 [] ["maxsize"] + (ReqArg (\v c -> c { _confMaxSize = read v }) (show (_confMaxSize miosDefaultOption))) + "[solver] limit of the number of variables" + , 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 (satisfiable) assignment" + , Option ['o'] ["output"] + (ReqArg (\v c -> c { _outputFile = Just v }) "file") + "[option] filename to store 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 solution" + , Option [] ["benchmark"] + (ReqArg (\v c -> c { _confBenchmark = read v }) "-1/0/N") + "[devel] No/Exhaustive/N-second timeout benchmark" + , Option [] ["sequence"] + (ReqArg (\v c -> c { _confBenchSeq = read v }) "NUM") + "[devel] set 2nd field of a CSV generated by benchmark" + , Option [] ["dump"] + (ReqArg (\v c -> c { _confDumpStat = read v }) (show (dumpStat defaultConfiguration))) + "[devel] dump level; 1:solved, 2:reduction, 3:restart" + , Option ['h'] ["help"] + (NoArg (\c -> c { _displayHelp = True })) + "[misc] display this 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, [], []) -> return $ foldl (flip id) miosDefaultOption o + (o, l, []) -> do + let conf = foldl (flip id) miosDefaultOption o + return $ conf { _targetFile = Just (head l), _targets = l } + (_, _, 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 + , dumpStat = _confDumpStat opts + } diff --git a/src/SAT/Mios/Solver.hs b/src/SAT/Mios/Solver.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Solver.hs @@ -0,0 +1,454 @@ +-- | (This is a part of MIOS.) +-- Solver, the main data structure +{-# LANGUAGE + MultiWayIf + , RecordWildCards + , ScopedTypeVariables + , TupleSections + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +module SAT.Mios.Solver + ( + -- * Solver + Solver (..) + , newSolver + -- * Misc Accessors + , nAssigns + , nClauses + , nLearnts + , decisionLevel + , valueVar + , valueLit + , locked + -- * State Modifiers + , setAssign + , enqueue + , assume + , cancelUntil + -- * Stats + , StatIndex (..) + , getStat + , setStat + , incrementStat + , getStats + , dumpSolver + ) + where + +import Control.Monad (unless, when) +import Data.List (intercalate) +import Numeric (showFFloat) +import SAT.Mios.Types +import SAT.Mios.Clause +import SAT.Mios.ClauseManager +import SAT.Mios.ClausePool + +-- | __Fig. 2.(p.9)__ Internal State of the solver +data Solver = Solver + { + -------- Database + clauses :: !ClauseExtManager -- ^ List of problem constraints. + , learnts :: !ClauseExtManager -- ^ List of learnt clauses. + , watches :: !WatcherList -- ^ list of constraint wathing 'p', literal-indexed + -------- Assignment Management + , assigns :: !(Vec Int) -- ^ The current assignments indexed on variables + , phases :: !(Vec Int) -- ^ The last assignments indexed on variables + , trail :: !Stack -- ^ List of assignments in chronological order + , trailLim :: !Stack -- ^ Separator indices for different decision levels in 'trail'. + , qHead :: !Int' -- ^ 'trail' is divided at qHead; assignment part and queue part + , reason :: !ClauseVector -- ^ For each variable, the constraint that implied its value + , level :: !(Vec Int) -- ^ For each variable, the decision level it was assigned + , conflicts :: !Stack -- ^ Set of literals in the case of conflicts + -------- Variable Order + , activities :: !(Vec Double) -- ^ Heuristic measurement of the activity of a variable + , order :: !VarHeap -- ^ Keeps track of the dynamic variable order. + -------- Configuration + , config :: !MiosConfiguration -- ^ search paramerters + , nVars :: !Int -- ^ number of variables + , claInc :: !Double' -- ^ Clause activity increment amount to bump with. + , varInc :: !Double' -- ^ Variable activity increment amount to bump with. + , rootLevel :: !Int' -- ^ Separates incremental and search assumptions. + -------- DB Size Adjustment + , learntSAdj :: Double' -- ^ used in 'SAT.Mios.Main.search' + , learntSCnt :: Int' -- ^ used in 'SAT.Mios.Main.search' + , maxLearnts :: Double' -- ^ used in 'SAT.Mios.Main.search' + -------- Working Memory + , ok :: !Int' -- ^ internal flag + , an'seen :: !(Vec Int) -- ^ used in 'SAT.Mios.Main.analyze' + , an'toClear :: !Stack -- ^ used in 'SAT.Mios.Main.analyze' + , an'stack :: !Stack -- ^ used in 'SAT.Mios.Main.analyze' + , an'lastDL :: !Stack -- ^ last decision level used in 'SAT.Mios.Main.analyze' + , clsPool :: ClausePool -- ^ clause recycler + , litsLearnt :: !Stack -- ^ used in 'SAT.Mios.Main.analyze' and 'SAT.Mios.Main.search' to create a learnt clause + , stats :: !(Vec [Int]) -- ^ statistics information holder + , lbd'seen :: !(Vec Int) -- ^ used in lbd computation + , lbd'key :: !Int' -- ^ used in lbd computation + -------- restart heuristics #62 + , emaDFast :: !Double' -- ^ fast ema value of LBD + , emaDSlow :: !Double' -- ^ slow ema value of LBD + , emaAFast :: !Double' -- ^ fast ema value of assignment + , emaASlow :: !Double' -- ^ slow ema value of assignment + , nextRestart :: !Int' -- ^ next restart in number of conflict + , restartMode :: Int' -- ^ mode of restart + } + +-- | returns an everything-is-initialized solver from the arguments. +newSolver :: MiosConfiguration -> CNFDescription -> IO Solver +newSolver conf (CNFDescription nv dummy_nc _) = + Solver + -- Clause Database + <$> newManager dummy_nc -- clauses + <*> newManager 2000 -- learnts + <*> newWatcherList nv 2 -- watches + -- Assignment Management + <*> newVec nv LBottom -- assigns + <*> newVec nv LBottom -- phases + <*> newStack nv -- trail + <*> newStack nv -- trailLim + <*> new' 0 -- qHead + <*> newClauseVector (nv + 1) -- reason + <*> newVec nv (-1) -- level + <*> newStack nv -- conflicts + -- Variable Order + <*> newVec nv 0 -- activities + <*> newVarHeap nv -- order + -- Configuration + <*> return conf -- config + <*> return nv -- nVars + <*> new' 1.0 -- claInc + <*> new' 1.0 -- varInc + <*> new' 0 -- rootLevel + -- Learnt DB Size Adjustment + <*> new' 100 -- learntSAdj + <*> new' 100 -- learntSCnt + <*> new' 2000 -- maxLearnts + -- Working Memory + <*> new' LiftedT -- ok + <*> newVec nv 0 -- an'seen + <*> newStack nv -- an'toClear + <*> newStack nv -- an'stack + <*> newStack nv -- an'lastDL + <*> newClausePool 10 -- clsPool + <*> newStack nv -- litsLearnt + <*> newVec (fromEnum EndOfStatIndex) 0 -- stats + <*> newVec nv 0 -- lbd'seen + <*> new' 0 -- lbd'key + -- restart heuristics #62 + <*> new' 0.0 -- emaDFast + <*> new' 0.0 -- emaDSlow + <*> new' 0.0 -- emaAFast + <*> new' 0.0 -- emaASlow + <*> new' 100 -- nextRestart + <*> new' 1 -- restartMode + +-------------------------------------------------------------------------------- +-- Accessors + +-- | returns the number of current assigments. +{-# INLINE nAssigns #-} +nAssigns :: Solver -> IO Int +nAssigns = get' . trail + +-- | returns the number of constraints (clauses). +{-# INLINE nClauses #-} +nClauses :: Solver -> IO Int +nClauses = get' . clauses + +-- | returns the number of learnt clauses. +{-# INLINE nLearnts #-} +nLearnts :: Solver -> IO Int +nLearnts = get' . learnts + +-- | returns the current decision level. +{-# INLINE decisionLevel #-} +decisionLevel :: Solver -> IO Int +decisionLevel = get' . 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 +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 ==) <$> (getNth (reason s) . lit2var =<< getNth (lits c) 1) + +-------------------------------------------------------------------------------- Statistics + +-- | 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 a list. +{-# INLINABLE getStats #-} +getStats :: Solver -> IO [(StatIndex, Int)] +getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex] + +-------------------------------------------------------------------------------- State Modifiers + +-- | assigns a value to the /n/-th variable +setAssign :: Solver -> Int -> LiftedBool -> IO () +setAssign Solver{..} v x = setNth assigns v x + +-- | __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 <- get' (lbd from) + k <- (12 +) <$> decisionLevel s + when (k < l) $ set' (lbd from) k +-} + let signumP = lit2lbool p + let v = lit2var p + val <- valueVar s v + if val /= LBottom + then return $ val == signumP -- Existing consistent assignment -- don't enqueue + else do setNth assigns v signumP -- New fact, store it + setNth level v =<< decisionLevel s + setNth reason v from -- NOTE: @from@ might be NULL! + pushTo 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 + pushTo (trailLim s) =<< get' (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 + lim <- getNth trailLim (lvl + 1) + ts <- get' trail + ls <- get' trailLim + let + loopOnTrail :: Int -> IO () + loopOnTrail ((lim <) -> False) = return () + loopOnTrail c = do + x <- lit2var <$> getNth trail 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. + setNth 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 + shrinkBy trail (ts - lim) + shrinkBy trailLim (ls - lvl) + set' qHead =<< get' 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 + +-------------------------------------------------------------------------------- VarHeap + +-- | 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 :: !Stack -- order to var + , idxs :: !Stack -- var to order (index) + } + +newVarHeap :: Int -> IO VarHeap +newVarHeap n = do + v1 <- newVec n 0 + v2 <- newVec n 0 + let + loop :: Int -> IO () + loop ((<= n) -> False) = set' v1 n >> set' v2 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 = get' . heap . order + +{-# INLINE inHeap #-} +inHeap :: Solver -> Var -> IO Bool +inHeap Solver{..} n = case idxs order of at -> (/= 0) <$> getNth at n + +{-# INLINE increaseHeap #-} +increaseHeap :: Solver -> Int -> IO () +increaseHeap s@Solver{..} n = case idxs order of + at -> 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 <- getNth activities v + 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 <- getNth activities v' + 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 <- getNth activities v + 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 <- getNth activities l + acR <- getNth activities r + 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 + +{-# INLINABLE 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 + set' to n + percolateUp s n + +-- | returns the value on the root (renamed from @getmin@). +{-# INLINABLE 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 + +-------------------------------------------------------------------------------- dump + +{-# INLINABLE dumpSolver #-} +-- | print statatistic data to stdio. This should be called after each restart. +dumpSolver :: DumpMode -> Solver -> IO () + +dumpSolver NoDump _ = return () + +dumpSolver DumpCSVHeader s@Solver{..} = do + sts <- init <$> getStats s + let labels = map (show . fst) sts ++ ["emaDFast", "emaDSlow", "emaAFast", "emaASlow"] + putStrLn $ intercalate "," labels + +dumpSolver DumpCSV s@Solver{..} = do + -- First update the stat data + df <- get' emaDFast + ds <- get' emaDSlow + af <- get' emaAFast + as <- get' emaASlow + sts <- init <$> getStats s + va <- get' trailLim + setStat s NumOfVariable . (nVars -) =<< if va == 0 then get' trail else getNth trailLim 1 + setStat s NumOfAssigned =<< nAssigns s + setStat s NumOfClause =<< get' clauses + setStat s NumOfLearnt =<< get' learnts + -- Additional data which type is Double + let emas = [("emaDFast", df), ("emaDSlow", ds), ("emaAFast", af), ("emaASlow", as)] + fs x = showFFloat (Just 3) x "" + vals = map (show . snd) sts ++ map (fs . snd) emas + putStrLn $ intercalate "," vals + +-- | FIXME: use Util/Stat +dumpSolver DumpJSON _ = return () -- mode 2: JSON diff --git a/src/SAT/Mios/Types.hs b/src/SAT/Mios/Types.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Types.hs @@ -0,0 +1,337 @@ +-- | (This is a part of MIOS.) +-- Basic data types used throughout mios. +{-# LANGUAGE + BangPatterns + , PatternSynonyms + #-} +{-# LANGUAGE Safe #-} + +module SAT.Mios.Types + ( + -- * Interface to caller + SolverResult + , Certificate (..) + , SolverException (..) + , CNFDescription (..) + -- * Solver Configuration + , MiosConfiguration (..) + , defaultConfiguration + -- * internal structure + , module SAT.Mios.Vec + -- * Variable + , Var + , bottomVar + , int2var + -- * Internal encoded Literal + , Lit + , lit2int + , int2lit + , bottomLit + , positiveLit + , lit2var + , var2lit + , negateLit + -- * Assignment on the lifted Bool domain + , LiftedBool + , lit2lbool + , Int (LiftedF, LiftedT, LBottom, Conflict) + -- a heap + , VarOrder (..) + -- * statistics + , StatIndex (..) + , DumpMode (..) +{- + -- * dump statistics + , DumpTag (..) + , DumpedValue + , MiosStats (..) + , QuadLearntC (..) + , MiosDump (..) +-} + ) + where + +import Data.Bits +import SAT.Mios.Vec + +-- | terminate and find an SAT/UNSAT answer +data Certificate + = SAT [Int] + | UNSAT [Int] -- FIXME: replace with DRAT + deriving (Eq, Ord, Read, Show) + +-- | abnormal termination flags +data SolverException + = StateUNSAT -- 0 + | StateSAT -- 1 + | OutOfMemory -- 2 + | TimeOut -- 3 + | InternalInconsistent -- 4 + | UndescribedError -- 5 + deriving (Bounded, Enum, Eq, Ord, Show) + +-- | the type that Mios returns +-- This captures the following three cases: +-- * solved with a satisfiable assigment, +-- * proved that it's an unsatisfiable problem, and +-- * aborted due to Mios specification or an internal error +type SolverResult = Either SolverException Certificate + +-- | 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 :: Int -> Int +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. +type LiftedBool = Int + +-- | /FALSE/ on the Lifted Bool domain +pattern LiftedF :: Int +pattern LiftedF = -1 + +-- | /TRUE/ on the Lifted Bool domain +pattern LiftedT :: Int +pattern LiftedT = 1 + +-- | /UNDEFINED/ on the Lifted Bool domain +pattern LBottom :: Int +pattern LBottom = 0 + +-- | /CONFLICT/ on the Lifted Bool domain +pattern Conflict :: Int +pattern Conflict = 2 + +-- | returns the value of a literal as a 'LiftedBool' +{-# INLINE lit2lbool #-} +lit2lbool :: Lit -> LiftedBool +lit2lbool l = if positiveLit l then LiftedT else LiftedF + +{- +-- | converts 'Bool' into 'LBool' +{-# INLINE lbool #-} +lbool :: Bool -> LiftedBool +lbool True = LTrue +lbool False = LFalse +-} + +-- | 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 :: (VecFamily v1 Bool, VecFamily 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" +-} + -- | should be called when a variable has increased in activity. + update :: o -> Var -> IO () + update _ = error "update undefined" +{- + -- | should be called when all variables have been assigned. + updateAll :: o -> IO () + updateAll = error "updateAll undefined" +-} + -- | should be called when a variable becomes unbound (may be selected again). + undo :: o -> Var -> IO () + undo _ _ = error "undo undefined" + + -- | returns a new, unassigned var as the next decision. + select :: o -> IO Var + select = error "select undefined" + +-- | Misc information on a CNF +data CNFDescription = CNFDescription + { + _numberOfVariables :: !Int -- ^ the number of variables + , _numberOfClauses :: !Int -- ^ the number of clauses + , _pathname :: Maybe FilePath -- ^ given filename + } + deriving (Eq, Ord, Read, Show) + +-- | 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 + , dumpStat :: !Int -- ^ dump stats data during solving + } + deriving (Eq, Ord, Read, Show) + +-- | 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 + +-------------------------------------------------------------------------------- Statistics + +-- | stat index +data StatIndex = + NumOfBackjump -- ^ the number of backjump + | NumOfRestart -- ^ the number of restart + | NumOfBlockRestart -- ^ the number of blacking start + | NumOfGeometricRestart -- ^ the number of classic restart + | NumOfPropagation -- ^ the number of propagation + | NumOfReduction -- ^ the number of reduction + | NumOfClause -- ^ the number of 'alive' given clauses + | NumOfLearnt -- ^ the number of 'alive' learnt clauses + | NumOfVariable -- ^ the number of 'alive' variables + | NumOfAssigned -- ^ the number of assigned variables + | EndOfStatIndex -- ^ Don't use this dummy. + deriving (Bounded, Enum, Eq, Ord, Read, Show) + +-- | formats of state dump +data DumpMode = NoDump | DumpCSVHeader | DumpCSV | DumpJSON + deriving (Bounded, Enum, Eq, Ord, Read, Show) + +data DumpTag = TerminateS + | PropagationS + | ConflictS + | LearntS + | BackjumpS + | RestartS + | LearningRateS + | ExtraS + deriving (Bounded, Enum, Eq, Ord, Read, Show) + +type DumpedValue = (DumpTag, Either Double Int) + +newtype MiosStats = MiosStats [DumpedValue] + deriving (Eq, Ord, Read, Show) + +data MiosDump = + MiosDump { _dumpedConf :: (String, MiosConfiguration) + , _dupmedCNFDesc :: CNFDescription + , _dumpedStat :: MiosStats + } + deriving (Eq, Ord, Read, Show) diff --git a/src/SAT/Mios/Util/BoolExp.hs b/src/SAT/Mios/Util/BoolExp.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Util/BoolExp.hs @@ -0,0 +1,249 @@ +{-# 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 :: BoolForm +boolFormTrue = Cnf (-1, 1) [] + +boolFormFalse :: BoolForm +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' +(-|||-) :: [BoolForm] -> BoolForm +(-|||-) = disjunctionOf + +-- | merge [BoolForm] by '(-&-)' +conjunctionOf :: [BoolForm] -> BoolForm +conjunctionOf [] = boolFormTrue +conjunctionOf (x:l) = foldl' (-&-) x l + +-- | an alias of 'conjunctionOf' +(-&&&-) :: [BoolForm] -> BoolForm +(-&&&-) = 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/src/SAT/Mios/Util/DIMACS.hs b/src/SAT/Mios/Util/DIMACS.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Util/DIMACS.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE Safe #-} + +-- | Read/Write a CNF file only with ghc standard libraries +module SAT.Mios.Util.DIMACS + ( + -- * Input + fromFile + , clauseListFromFile + , fromMinisatOutput + , clauseListFromMinisatOutput + -- * Output + , toFile + , toDIMACSString + , asDIMACSString + , asDIMACSString_ + -- * Bool Operation + , module SAT.Mios.Util.BoolExp + ) + where +import SAT.Mios.Util.DIMACS.Reader +import SAT.Mios.Util.DIMACS.Writer +import SAT.Mios.Util.DIMACS.MinisatReader +import SAT.Mios.Util.BoolExp + +-- | String from BoolFrom +asDIMACSString :: BoolForm -> String +asDIMACSString = toDIMACSString . asList + +-- | String from BoolFrom +asDIMACSString_ :: BoolForm -> String +asDIMACSString_ = toDIMACSString . asList_ diff --git a/src/SAT/Mios/Util/DIMACS/MinisatReader.hs b/src/SAT/Mios/Util/DIMACS/MinisatReader.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Util/DIMACS/MinisatReader.hs @@ -0,0 +1,77 @@ +{-# LANGUAGE Safe #-} + +-- | Read an output file of minisat +module SAT.Mios.Util.DIMACS.MinisatReader + ( + -- * Interface + fromMinisatOutput + , clauseListFromMinisatOutput + ) + where +-- import Control.Applicative ((<$>), (<*>), (<*), (*>)) +import Data.Char +import Text.ParserCombinators.ReadP + +-- parser +-- |parse a non-signed integer +{-# INLINE pint #-} +pint :: ReadP Int +pint = do + n <- munch isDigit + return (read n :: Int) + +{-# INLINE mint #-} +mint :: ReadP Int +mint = do + char '-' + n <- munch isDigit + return (- (read n::Int)) + +-- |parse a (signed) integer +{-# INLINE int #-} +int :: ReadP Int +int = mint <++ pint + +-- |return integer list that terminates at zero +{-# INLINE seqNums #-} +seqNums :: ReadP [Int] +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/src/SAT/Mios/Util/DIMACS/Reader.hs b/src/SAT/Mios/Util/DIMACS/Reader.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Util/DIMACS/Reader.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE Safe #-} + +-- | Read a CNF file without haskell-platform +module SAT.Mios.Util.DIMACS.Reader + ( + -- * Interface + fromFile + , clauseListFromFile + ) + where +import Control.Applicative ((<$>), (<*>), (<*), (*>)) +import Data.Char +import Text.ParserCombinators.ReadP + +-- parser +{-# INLINE newline #-} +newline :: ReadP Char +newline = char '\n' + +{-# INLINE digit #-} +digit :: ReadP Char +digit = satisfy isDigit + +{-# INLINE spaces #-} +spaces :: ReadP String +spaces = munch (`elem` " \t") + +{-# INLINE noneOf #-} +noneOf :: Foldable t => t Char -> ReadP Char +noneOf s = satisfy (`notElem` s) + +-- |parse a non-signed integer +{-# INLINE pint #-} +pint :: ReadP Int +pint = do + n <- munch isDigit + return (read n :: Int) + +{-# INLINE mint #-} +mint :: ReadP Int +mint = do + char '-' + n <- munch isDigit + return (- (read n::Int)) + +-- |parse a (signed) integer +{-# INLINE int #-} +int :: ReadP Int +int = mint <++ pint + +-- |Parse something like: p FORMAT VARIABLES CLAUSES +{-# INLINE problemLine #-} +problemLine :: ReadP (Int, Int) +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 :: ReadP () +commentLines = do + l <- look + if (head l) == 'c' + then do + munch ('\n' /=) + newline + commentLines + else return () + +_commentLines :: ReadP () +_commentLines = do + char 'c' + munch ('\n' /=) + newline + l <- look + if (head l) == 'c' then commentLines else return () + +-- |Parse the preamble part +{-# INLINE preambleCNF #-} +preambleCNF :: ReadP (Int, Int) +preambleCNF = do + commentLines + problemLine + +-- |return integer list that terminates at zero +{-# INLINE seqNums #-} +seqNums :: ReadP [Int] +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 :: String -> [([[Int]], String)] +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/src/SAT/Mios/Util/DIMACS/Writer.hs b/src/SAT/Mios/Util/DIMACS/Writer.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Util/DIMACS/Writer.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE Safe #-} + +-- | Write SAT data to DIMACS file +module SAT.Mios.Util.DIMACS.Writer + ( + -- * Interface + toFile + , toDIMACSString + , toString + , toLatexString + ) + where +import Data.List (intercalate, nub, sort) +import System.IO + +-- | Write the DIMACS to file 'f', using 'toDIMACSString' +toFile :: FilePath -> [[Int]] -> IO () +toFile f l = writeFile f $ toDIMACSString l + +-- | Convert [Clause] to String, where Clause is [Int] +-- +-- >>> toDIMACSString [] +-- "p cnf 0 0\n" +-- +-- >>> toDIMACSString [[-1, 2], [-3, -4]] +-- "p cnf 4 2\n-1 2 0\n-3 -4 0\n" +-- +-- >>> toDIMACSString [[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" +-- +toDIMACSString :: [[Int]] -> String +toDIMACSString 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/src/SAT/Mios/Validator.hs b/src/SAT/Mios/Validator.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Validator.hs @@ -0,0 +1,69 @@ +-- | (This is a part of MIOS.) +-- Validate an assignment +{-# LANGUAGE + RecordWildCards + , ViewPatterns + #-} +{-# LANGUAGE Safe #-} + +module SAT.Mios.Validator + ( + validate +-- , checkUniqueness + ) + where + +import Control.Monad (when) +import Data.Foldable (toList) +import Data.List (sort) +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 t = do + assignment <- newVec (1 + nVars s) (0 :: Int) :: IO (Vec Int) + vec <- getClauseVector (clauses s) + nc <- get' (clauses s) + let + lst = map int2lit $ toList t + inject :: Lit -> IO () + inject l = setNth assignment (lit2var l) $ lit2lbool l + -- returns True if the literal is satisfied under the assignment + satisfied :: Lit -> IO Bool + satisfied l + | positiveLit l = (LiftedT ==) <$> getNth assignment (lit2var l) + | otherwise = (LiftedF ==) <$> 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 + sat' <- satAny =<< asList =<< getNth vec i + 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 + +-- | checks uniqueness of learnts +checkUniqueness :: Solver -> Clause -> IO () +checkUniqueness Solver{..} c = do + n <- get' learnts + cvec <- getClauseVector learnts + cls <- sort <$> asList c + let + loop :: Int -> IO () + loop ((< n) -> False) = return () + loop i = do + c' <- getNth cvec i + cls' <- sort <$> asList c' + when (cls' == cls) $ errorWithoutStackTrace "reinsert a same clause" + loop (i + 1) + loop 0 diff --git a/src/SAT/Mios/Vec.hs b/src/SAT/Mios/Vec.hs new file mode 100644 --- /dev/null +++ b/src/SAT/Mios/Vec.hs @@ -0,0 +1,359 @@ +-- | (This is a part of MIOS.) +-- Abstraction Layer for Mutable Vectors +{-# LANGUAGE + BangPatterns + , FlexibleContexts + , FlexibleInstances + , FunctionalDependencies + , MultiParamTypeClasses + , TypeFamilies + #-} +{-# LANGUAGE Trustworthy #-} + +module SAT.Mios.Vec + ( + -- * Vector class and type + VecFamily (..) + , Vec (..) + -- * SingleStorage + , SingleStorage (..) + , Bool' + , Double' + , Int' + -- * Stack + , StackFamily (..) + , Stack + , newStackFromList + , realLengthOfStack + , sortStack + ) + where + +import qualified Data.Vector.Unboxed.Mutable as UV +import qualified Data.Primitive.ByteArray as BA +import Control.Monad.Primitive + +-------------------------------------------------------------------------------- VecFamily +-- | The interface on vectors. +class VecFamily v a | v -> a where + -- | returns the /n/-th value. + getNth ::v -> Int -> IO a + -- | sets the /n/-th value. + setNth :: v -> Int -> a -> IO () + -- | erases all elements in it. + reset:: v -> IO () + -- | returns the /n/-th value (index starts from zero in any case). + -- | swaps two elements. + swapBetween :: v -> Int -> Int -> IO () + -- | calls the update function. + modifyNth :: v -> (a -> a) -> Int -> IO () + -- | returns a new vector. + newVec :: Int -> a -> IO v + -- | sets all elements. + setAll :: v -> a -> IO () + -- | extends the size of stack by /n/; note: values in new elements aren't initialized maybe. + growBy :: v -> Int -> IO v + -- | converts to a list. + asList :: v -> IO [a] + {-# MINIMAL getNth, setNth #-} + reset = errorWithoutStackTrace "no default method: reset" + swapBetween = errorWithoutStackTrace "no default method: swapBetween" + modifyNth = errorWithoutStackTrace "no default method: modifyNth" + newVec = errorWithoutStackTrace "no default method: newVec" + setAll = errorWithoutStackTrace "no default method: setAll" + asList = errorWithoutStackTrace "no default method: asList" + growBy = errorWithoutStackTrace "no default method: growBy" + -- | (FOR DEBUG) dump the contents. + -- dump :: Show a => String -> v -> IO String + -- dump msg v = (msg ++) . show <$> asList v + +-------------------------------------------------------------------------------- Vec +-- | Another abstraction layer on 'Vector' which reserves zero element for internal use. +-- __Note__: If you want to use the 0-th element, use @UVector Int@. + +data family Vec a; + +-------------------------------------------------------------------------------- UVector + +-- | A thin abstract layer for mutable unboxed Vector +type UVector a = UV.IOVector a + +instance VecFamily (UVector Int) Int where + {-# SPECIALIZE INLINE getNth :: UVector Int -> Int -> IO Int #-} + getNth = UV.unsafeRead + {-# SPECIALIZE INLINE setNth :: UVector Int -> Int -> Int -> IO () #-} + setNth = UV.unsafeWrite + {-# SPECIALIZE INLINE modifyNth :: UVector Int -> (Int -> Int) -> Int -> IO () #-} + modifyNth = UV.unsafeModify + {-# SPECIALIZE INLINE swapBetween:: UVector Int -> Int -> Int -> IO () #-} + swapBetween = UV.unsafeSwap + {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO (UVector Int) #-} + newVec n 0 = UV.new n + newVec n x = do v <- UV.new n + UV.set v x + return v + {-# SPECIALIZE INLINE setAll :: UVector Int -> Int -> IO () #-} + setAll = UV.set + {-# SPECIALIZE INLINE growBy :: UVector Int -> Int -> IO (UVector Int) #-} + growBy = UV.unsafeGrow + asList v = mapM (UV.unsafeRead v) [0 .. UV.length v - 1] + +-- Note: type @[Int]@ is selected for 'UVector' not to export it. +data instance Vec [Int] = Vec (UVector Int) + +instance VecFamily (Vec [Int]) Int where + {-# SPECIALIZE INLINE getNth :: Vec [Int] -> Int -> IO Int #-} + getNth (Vec v) = UV.unsafeRead v + {-# SPECIALIZE INLINE setNth :: Vec [Int] -> Int -> Int -> IO () #-} + setNth (Vec v) = UV.unsafeWrite v + {-# SPECIALIZE INLINE reset :: Vec [Int] -> IO () #-} + reset (Vec v) = setNth v 0 0 + {-# SPECIALIZE INLINE modifyNth :: Vec [Int] -> (Int -> Int) -> Int -> IO () #-} + modifyNth (Vec v) = UV.unsafeModify v + {-# SPECIALIZE INLINE swapBetween :: Vec [Int] -> Int -> Int -> IO () #-} + swapBetween (Vec v) = UV.unsafeSwap v + {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO (Vec [Int]) #-} + newVec n x = Vec <$> newVec (n + 1) x + {-# SPECIALIZE INLINE setAll :: Vec [Int] -> Int -> IO () #-} + setAll (Vec v) = UV.set v + {-# SPECIALIZE INLINE growBy :: Vec [Int] -> Int -> IO (Vec [Int]) #-} + growBy (Vec v) n = Vec <$> UV.unsafeGrow v n + asList (Vec v) = mapM (getNth v) [0 .. UV.length v - 1] + +{- NOT IN USE +data instance Vec [Double] = Vec (UVector Double) + +instance VecFamily (UVector Double) Double where + {-# SPECIALIZE INLINE getNth :: UVector Double -> Int -> IO Double #-} + getNth = UV.unsafeRead + {-# SPECIALIZE INLINE setNth :: UVector Double -> Int -> Double -> IO () #-} + setNth = UV.unsafeWrite + {-# SPECIALIZE INLINE modifyNth :: UVector Double -> (Double -> Double) -> Int -> IO () #-} + modifyNth = UV.unsafeModify + {-# SPECIALIZE INLINE swapBetween:: UVector Double -> Int -> Int -> IO () #-} + swapBetween = UV.unsafeSwap + {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO (UVector Double) #-} + newVec n x = do v <- UV.new n + UV.set v x + return v + {-# SPECIALIZE INLINE setAll :: UVector Double -> Double -> IO () #-} + setAll = UV.set + {-# SPECIALIZE INLINE growBy :: UVector Double -> Int -> IO (UVector Double) #-} + growBy = UV.unsafeGrow + asList v = mapM (UV.unsafeRead v) [0 .. UV.length v - 1] + +instance VecFamily (Vec Double) Double where + {-# SPECIALIZE INLINE getNth :: Vec Double -> Int -> IO Double #-} + getNth (Vec v) = UV.unsafeRead v + {-# SPECIALIZE INLINE setNth :: Vec Double -> Int -> Double -> IO () #-} + setNth (Vec v) = UV.unsafeWrite v + {-# SPECIALIZE INLINE modifyNth :: Vec Double -> (Double -> Double) -> Int -> IO () #-} + modifyNth (Vec v) = UV.unsafeModify v + {-# SPECIALIZE INLINE swapBetween :: Vec Double -> Int -> Int -> IO () #-} + swapBetween (Vec v) = UV.unsafeSwap v + {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO (Vec Double) #-} + newVec n x = Vec <$> newVec (n + 1) x + {-# SPECIALIZE INLINE setAll :: Vec Double -> Double -> IO () #-} + setAll (Vec v) = UV.set v + {-# SPECIALIZE INLINE growBy :: Vec Double -> Int -> IO (Vec Double) #-} + growBy (Vec v) n = Vec <$> UV.unsafeGrow v n +-} + +-------------------------------------------------------------------------------- ByteArray + +data instance Vec Int = ByteArrayInt (BA.MutableByteArray RealWorld) +data instance Vec Double = ByteArrayDouble (BA.MutableByteArray RealWorld) + +type ByteArrayInt = Vec Int +type ByteArrayDouble = Vec Double + +instance VecFamily ByteArrayInt Int where + {-# SPECIALIZE INLINE getNth :: ByteArrayInt -> Int -> IO Int #-} + getNth (ByteArrayInt v) i = BA.readByteArray v i + {-# SPECIALIZE INLINE setNth :: ByteArrayInt -> Int -> Int -> IO () #-} + setNth (ByteArrayInt v) i x = BA.writeByteArray v i x + {-# SPECIALIZE INLINE modifyNth :: ByteArrayInt -> (Int -> Int) -> Int -> IO () #-} + modifyNth (ByteArrayInt v) f i = BA.writeByteArray v i . f =<< BA.readByteArray v i + {-# SPECIALIZE INLINE swapBetween:: ByteArrayInt -> Int -> Int -> IO () #-} + swapBetween (ByteArrayInt v) i j = do x <- BA.readByteArray v i + y <- BA.readByteArray v j + BA.writeByteArray v i (y :: Int) + BA.writeByteArray v j (x :: Int) + {-# SPECIALIZE INLINE reset :: ByteArrayInt -> IO () #-} + reset (ByteArrayInt v) = BA.writeByteArray v 0 (0 :: Int) + newVec n k = do v <- BA.newByteArray (8 * (n + 1)) + BA.writeByteArray v 0 (0 :: Int) + BA.setByteArray v 1 n k + return $ ByteArrayInt v + asList (ByteArrayInt v) = mapM (BA.readByteArray v) [0 .. div (BA.sizeofMutableByteArray v) 8 - 1] + +instance VecFamily ByteArrayDouble Double where + {-# SPECIALIZE INLINE getNth :: ByteArrayDouble -> Int -> IO Double #-} + getNth (ByteArrayDouble v) i = BA.readByteArray v i + {-# SPECIALIZE INLINE setNth :: ByteArrayDouble -> Int -> Double -> IO () #-} + setNth (ByteArrayDouble v) i x = BA.writeByteArray v i x + {-# SPECIALIZE INLINE modifyNth :: ByteArrayDouble -> (Double -> Double) -> Int -> IO () #-} + modifyNth (ByteArrayDouble v) f i = BA.writeByteArray v i . f =<< BA.readByteArray v i + {-# SPECIALIZE INLINE swapBetween:: ByteArrayDouble -> Int -> Int -> IO () #-} + swapBetween (ByteArrayDouble v) i j = do x <- BA.readByteArray v i + y <- BA.readByteArray v j + BA.writeByteArray v i (y :: Int) + BA.writeByteArray v j (x :: Int) + {-# SPECIALIZE INLINE reset :: ByteArrayDouble -> IO () #-} + reset (ByteArrayDouble v) = BA.writeByteArray v 0 (0 :: Double) + newVec n k = do v <- BA.newByteArray (8 * (n + 1)) + BA.writeByteArray v 0 (0 :: Double) + BA.setByteArray v 1 n k + return $ ByteArrayDouble v + asList (ByteArrayDouble v) = mapM (BA.readByteArray v) [0 .. div (BA.sizeofMutableByteArray v) 8 - 1] + +-------------------------------------------------------------------------------- SingleStorage + +-- | Interface for single (one-length vector) mutable data +class SingleStorage s t | s -> t where + -- | allocates and returns an new data. + new' :: t -> IO s + -- | gets the value. + get' :: s -> IO t + -- | sets the value. + set' :: s -> t -> IO () + -- | calls an update function on it. + modify' :: s -> (t -> t) -> IO () + {-# MINIMAL get', set' #-} + new' = undefined + modify' = undefined + +-- | Mutable Bool +type Bool' = UV.IOVector Bool + +instance SingleStorage Bool' Bool where + {-# SPECIALIZE INLINE new' :: Bool -> IO Bool' #-} + new' k = do s <- UV.new 1 + UV.unsafeWrite s 0 k + return s + {-# SPECIALIZE INLINE get' :: Bool' -> IO Bool #-} + get' val = UV.unsafeRead val 0 + {-# SPECIALIZE INLINE set' :: Bool' -> Bool -> IO () #-} + set' val !x = UV.unsafeWrite val 0 x + {-# SPECIALIZE INLINE modify' :: Bool' -> (Bool -> Bool) -> IO () #-} + modify' val f = UV.unsafeModify val f 0 + +-- | Mutable Int +-- __Note:__ Int' is identical to 'Stack' +type Int' = ByteArrayInt + +instance SingleStorage ByteArrayInt Int where + {-# SPECIALIZE INLINE new' :: Int -> IO ByteArrayInt #-} + new' k = do s <- BA.newByteArray 8 + BA.writeByteArray s 0 k + return $ ByteArrayInt s + {-# SPECIALIZE INLINE get' :: ByteArrayInt -> IO Int #-} + get' (ByteArrayInt v) = BA.readByteArray v 0 + {-# SPECIALIZE INLINE set' :: ByteArrayInt -> Int -> IO () #-} + set' (ByteArrayInt v) !x = BA.writeByteArray v 0 x + {-# SPECIALIZE INLINE modify' :: ByteArrayInt -> (Int -> Int) -> IO () #-} + modify' (ByteArrayInt v) f = BA.writeByteArray v 0 . f =<< BA.readByteArray v 0 + +-- | Mutable Double +type Double' = ByteArrayDouble + +instance SingleStorage ByteArrayDouble Double where + {-# SPECIALIZE INLINE new' :: Double -> IO ByteArrayDouble #-} + new' k = do s <- BA.newByteArray 8 + BA.writeByteArray s 0 k + return $ ByteArrayDouble s + {-# SPECIALIZE INLINE get' :: ByteArrayDouble -> IO Double #-} + get' (ByteArrayDouble v) = BA.readByteArray v 0 + {-# SPECIALIZE INLINE set' :: ByteArrayDouble -> Double -> IO () #-} + set' (ByteArrayDouble v) !x = BA.writeByteArray v 0 x + {-# SPECIALIZE INLINE modify' :: ByteArrayDouble -> (Double -> Double) -> IO () #-} + modify' (ByteArrayDouble v) f = BA.writeByteArray v 0 . f =<< BA.readByteArray v 0 + +-------------------------------------------------------------------------------- Stack + +-- | Interface on stacks +class SingleStorage s Int => StackFamily s t | s -> t where + -- | returns a new stack. + newStack :: Int -> IO s + -- | pushs an value to the tail of the stack. + pushTo :: s -> t-> IO () + -- | pops the last element. + popFrom :: s -> IO () + -- | peeks the last element. + lastOf :: s -> IO t + -- | shrinks the stack. + shrinkBy :: s -> Int -> IO () + newStack = undefined + pushTo = undefined + popFrom = undefined + lastOf = undefined + shrinkBy = undefined + +-- | Stack of Int, an alias of @Vec Int@ +type Stack = Vec Int + +instance StackFamily ByteArrayInt Int where + {-# SPECIALIZE INLINE newStack :: Int -> IO ByteArrayInt #-} + newStack n = do s <- newVec (2 * n) 0 + setNth s 0 (0::Int) + return s + {-# SPECIALIZE INLINE pushTo :: ByteArrayInt -> Int -> IO () #-} + pushTo (ByteArrayInt v) x = do i <- (+ 1) <$> (BA.readByteArray v 0 :: IO Int) + BA.writeByteArray v i x + BA.writeByteArray v 0 i + {-# SPECIALIZE INLINE popFrom :: ByteArrayInt -> IO () #-} + popFrom (ByteArrayInt v) = BA.writeByteArray v 0 . subtract 1 =<< (BA.readByteArray v 0 :: IO Int) + {-# SPECIALIZE INLINE lastOf :: ByteArrayInt -> IO Int #-} + lastOf (ByteArrayInt v) = BA.readByteArray v =<< BA.readByteArray v 0 + {-# SPECIALIZE INLINE shrinkBy :: ByteArrayInt -> Int -> IO () #-} + shrinkBy (ByteArrayInt v) k = BA.writeByteArray v 0 . subtract k =<< (BA.readByteArray v 0 :: IO Int) + +-- | returns a new 'Stack' from @[Int]@. +{-# INLINABLE newStackFromList #-} +newStackFromList :: [Int] -> IO Stack +newStackFromList l = do + v <- BA.newByteArray (8 * (length l + 1)) + let loop :: [Int] -> Int -> IO Stack + loop [] _ = return $ ByteArrayInt v + loop (x:l') i = BA.writeByteArray v i x >> loop l' (i + 1) + loop (length l : l) 0 + +-- | returns the number of allocated slots +{-# INLINE realLengthOfStack #-} +realLengthOfStack :: Stack -> Int +realLengthOfStack (ByteArrayInt v) = div (BA.sizeofMutableByteArray v) 8 + +-- | sort the content of a stack, in small-to-large order. +{-# INLINABLE sortStack #-} +sortStack :: Stack -> IO () +sortStack vec = do + n <- get' vec + let sortOnRange :: Int -> Int -> IO () + sortOnRange left right + | n < left = return () + | right < 1 = return () + | left >= right = return () + | left + 1 == right = do + a <- getNth vec left + b <- getNth vec right + if a < b then return () else swapBetween vec left right + | otherwise = do + let p = div (left + right) 2 + pivot <- getNth vec p + swapBetween vec p left -- set a sentinel for r' + let nextL :: Int -> IO Int + nextL i + | i <= right = do v <- getNth vec i; if v < pivot then nextL (i + 1) else return i + | otherwise = return i + nextR :: Int -> IO Int + nextR i = do v <- getNth vec 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 vec l' r' >> divide (l' + 1) (r' - 1) else return r' + m <- divide (left + 1) right + swapBetween vec left m + sortOnRange left (m - 1) + sortOnRange (m + 1) right + sortOnRange 1 n diff --git a/utils/cnf-stat.hs b/utils/cnf-stat.hs new file mode 100644 --- /dev/null +++ b/utils/cnf-stat.hs @@ -0,0 +1,54 @@ +-- | Prints +-- - the CNF filename, +-- - the number of literals /n/, +-- - the number of clauses /m/, +-- - the number of literal occurences in the file /o/, +-- - the average number of literals in a clause /k/ +{-# LANGUAGE + MultiWayIf + #-} +module Main + ( + main + ) + where + +import Control.Monad (when) +import qualified Data.ByteString.Char8 as B +import Data.List +import Numeric (showFFloat) +import SAT.Mios +import System.IO + +-- version id +vid :: String +vid = "cnf-stats version 0.2" + +usage :: String +usage = miosUsage $ vid ++ "\n" ++ "Usage: cnf-stats cnf+" + +-- | main +main :: IO () +main = do opts <- miosParseOptionsFromArgs vid + if | _displayVersion opts -> putStrLn vid + | _displayHelp opts -> putStrLn usage + | null (_targets opts) -> putStrLn usage + | otherwise -> mapM_ (countLiterals opts) (_targets opts) + +countLiterals :: MiosProgramOption -> FilePath -> IO () +countLiterals opts cnfFile = do + (desc, cls) <- parseCNF (Just cnfFile) + let n = _numberOfVariables desc + let m = _numberOfClauses desc + when (n /= 0) $ do + let o = length . filter ("0" /=) . words $ B.unpack cls + putStrLn $ intercalate "," + [ cnfFile + , show n + , show m + , show o + , showf $ fromIntegral o / fromIntegral m + ] + +showf :: Double -> String +showf x = showFFloat (Just 2) x ""