diff --git a/app/DiscordSecret.hs b/app/DiscordSecret.hs new file mode 100644 --- /dev/null +++ b/app/DiscordSecret.hs @@ -0,0 +1,6 @@ +-- join to a server: +-- https://discordapp.com/oauth2/authorize?&client_id=431666856785346560&scope=bot&permissions=0 +module DiscordSecret (token) where + +token :: String +token = "NDQ4ODM2NDM0MjkyNjM3NzA2.Deb7VA.v1mtGLLwG0GK9kbqNko7D_R14Bc" diff --git a/app/mios.hs b/app/mios.hs --- a/app/mios.hs +++ b/app/mios.hs @@ -1,5 +1,6 @@ {-# LANGUAGE - MultiWayIf + MultiWayIf + , TemplateHaskell #-} -- | Executable of 'Minisat Implementation and Optimization Study' module Main @@ -9,16 +10,20 @@ where import SAT.Mios +import Development.GitRev +gitId :: String +gitId = "mios " ++ versionId ++ "/commit/" ++ $(gitHash) + usage :: String -usage = miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf" +usage = miosUsage $ gitId ++ "\nUsage: mios [OPTIONS] target.cnf" -- | main main :: IO () main = do opts <- miosParseOptionsFromArgs versionId - if | _displayVersion opts -> putStrLn versionId + if | _displayVersion opts -> putStrLn gitId | _displayHelp opts -> putStrLn usage - | _targetFile opts == Nothing -> putStrLn usage - | _validateAssignment opts -> executeValidator opts - | otherwise -> executeSolver opts + | _targetFile opts == Left "" -> putStrLn usage + | _validateAssignment opts -> executeValidator opts =<< buildSolver opts + | otherwise -> executeSolver opts =<< buildSolver opts diff --git a/mios.cabal b/mios.cabal --- a/mios.cabal +++ b/mios.cabal @@ -1,11 +1,11 @@ --- This file has been generated from package.yaml by hpack version 0.20.0. +-- This file has been generated from package.yaml by hpack version 0.28.2. -- -- see: https://github.com/sol/hpack -- --- hash: 1a93fd2f2b1b1d0ba5e203ac6b48c5ca8abd31384c1955776cfb00969c311cbb +-- hash: 5cd432e14ff114a77b46f65cd54a00907c68da1bb380706bdbeb682bf43ff46d name: mios -version: 1.6.0 +version: 1.6.2 synopsis: A Minisat-based CDCL SAT solver in Haskell description: 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'. category: Artificial Intelligence, Constraints @@ -18,7 +18,6 @@ license-file: LICENSE build-type: Simple cabal-version: >= 1.10 - extra-source-files: app/sample.hs @@ -37,21 +36,6 @@ default: False library - hs-source-dirs: - src - default-extensions: Strict - build-depends: - base >=4.7 && <5 - , bytestring >=0.10 - , ghc-prim >=0.5 - , primitive >=0.6 - , vector >=0.12 - if flag(llvm) - ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures - ghc-prof-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -fprof-auto - else - ghc-options: -O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures - ghc-prof-options: -O2 -funbox-strict-fields -fprof-auto exposed-modules: SAT.Mios SAT.Mios.Clause @@ -71,10 +55,27 @@ SAT.Mios.Vec other-modules: Paths_mios + hs-source-dirs: + src + default-extensions: Strict + build-depends: + base >=4.7 && <5 + , bytestring >=0.10 + , ghc-prim >=0.5 + , primitive >=0.6 + , vector >=0.12 + if flag(llvm) + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3 + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto + else + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2 + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto default-language: Haskell2010 executable cnf-stat main-is: cnf-stat.hs + other-modules: + Paths_mios hs-source-dirs: utils default-extensions: Strict @@ -86,21 +87,22 @@ , primitive >=0.6 , vector >=0.12 if flag(llvm) - ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures - ghc-prof-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -fprof-auto + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3 + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto else - ghc-options: -O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures - ghc-prof-options: -O2 -funbox-strict-fields -fprof-auto + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2 + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto if flag(utils) buildable: True else buildable: False - other-modules: - Paths_mios default-language: Haskell2010 -executable mios-1.6.0 +executable mios162 main-is: mios.hs + other-modules: + DiscordSecret + Paths_mios hs-source-dirs: app default-extensions: Strict @@ -108,19 +110,46 @@ base >=4.7 && <5 , bytestring >=0.10 , ghc-prim >=0.5 + , gitrev , mios , primitive >=0.6 , vector >=0.12 if flag(llvm) - ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures - ghc-prof-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -fprof-auto + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3 + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto else - ghc-options: -O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures - ghc-prof-options: -O2 -funbox-strict-fields -fprof-auto + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2 + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto if flag(llvm) - ghc-prof-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -fprof-auto -rtsopts + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3 -rtsopts -with-rtsopts=-M7g + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto -rtsopts else - ghc-prof-options: -O2 -funbox-strict-fields -fprof-auto -rtsopts + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2 -rtsopts -with-rtsopts=-M7g + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto -rtsopts + default-language: Haskell2010 + +test-suite mios-test + type: exitcode-stdio-1.0 + main-is: Spec.hs other-modules: + MiosSpec Paths_mios + hs-source-dirs: + test + default-extensions: Strict + ghc-options: -threaded -rtsopts -with-rtsopts=-N + build-depends: + base >=4.7 && <5 + , bytestring >=0.10 + , ghc-prim >=0.5 + , hspec + , mios + , primitive >=0.6 + , vector >=0.12 + if flag(llvm) + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3 + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto + else + ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2 + ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto default-language: Haskell2010 diff --git a/src/SAT/Mios.hs b/src/SAT/Mios.hs --- a/src/SAT/Mios.hs +++ b/src/SAT/Mios.hs @@ -13,29 +13,29 @@ versionId , CNFDescription (..) , module SAT.Mios.OptionParser + -- * Main Interace + , SolverResult + , Certificate (..) + , buildOption + , buildSolver + , buildDescription + , executeSolver + , executeValidator + -- * Simple Interface , runSolver , solveSAT , solveSATWithConfiguration - , solve - , SolverResult - , Certificate (..) + , showAnswerFromString -- * Assignment Validator - , validateAssignment , validate - -- * For standalone programs - , executeSolverOn - , executeSolver - , executeValidatorOn - , executeValidator + , validateAssignment -- * File IO - , parseCNF - , injectClausesFromCNF , dumpAssigmentAsCNF ) where -import Control.Concurrent (forkIO, killThread, myThreadId, threadDelay - , newEmptyMVar, putMVar, readMVar) +import Control.Concurrent ( newEmptyMVar, putMVar, readMVar, takeMVar + , ThreadId, forkIO, killThread, myThreadId, threadDelay) import Control.Exception import Control.Monad ((<=<), unless, void, when) import Data.Char @@ -46,13 +46,14 @@ 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.6.0 -- https://github.com/shnarazk/mios" +versionId = "1.6.2 https://gitlab.com/satisfiability01/mios" reportElapsedTime :: Bool -> String -> Integer -> IO Integer reportElapsedTime False _ 0 = return 0 @@ -64,93 +65,139 @@ 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 }) +-- | returns a MiosProgramOption for the target +buildOption :: Either FilePath String -> MiosProgramOption +buildOption target = (miosDefaultOption { _targetFile = target }) +-- | returns a new solver injected a problem +buildSolver :: MiosProgramOption -> IO Solver +buildSolver opts = do + token <- newEmptyMVar -- :: IO (MVar (Maybe Solver)) + (desc, cls) <- parseCNF (_targetFile opts) + t0 <- reportElapsedTime False "" $ if _confVerbose opts || 0 <= _confBenchmark opts then -1 else 0 + readerId <- forkIO $ do + s <- newSolver (toMiosConf opts) desc + when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ (take 100 . show . _targetFile) opts + injectClausesFromCNF s desc cls + putMVar token s + when (0 < _confBenchmark opts) $ + void $ forkIO $ do let -- getCPUTime returns a pico sec. :: Integer, 1000 * 1000 * 1000 * 1000 + -- threadDelay requires a micro sec. :: Int, 1000 * 1000 + req = 1000000000000 * fromIntegral (_confBenchmark opts) :: Integer + waiting = do + elp <- getCPUTime + when (elp < req) $ do + threadDelay . max 1000000 $ fromIntegral (req - elp) `div` 1000000 + waiting + waiting + killThread readerId + s' <- newSolver defaultConfiguration (CNFDescription 0 0 "") + set' (ok s') LiftedF + putMVar token s' + void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] Parse: ") t0 + takeMVar token + +-- | returns the data on a given CNF file. Only solver knows it. +buildDescription :: FilePath -> Solver -> IO CNFDescription +buildDescription target s = CNFDescription (nVars s) <$> nClauses s <*> return target + -- | 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)) +executeSolver :: MiosProgramOption -> Solver -> IO () +executeSolver opts s = do solverId <- myThreadId + token <- newEmptyMVar -- :: IO (MVar (Maybe Solver)) + t0 <- reportElapsedTime False "" $ if _confVerbose opts || 0 <= _confBenchmark opts then -1 else 0 handle (\case - UserInterrupt -> putStrLn "User interrupt recieved." + UserInterrupt -> if -1 == _confBenchmark opts + then putStrLn "User interrupt (SIGINT) recieved." + else reportResult opts t0 (Left TimeOut) ThreadKilled -> reportResult opts t0 =<< readMVar token - e -> print e) $ do + HeapOverflow -> if -1 == _confBenchmark opts + then putStrLn "Abort: a too large problem or heap exhausted (use '+RTS -M16g' if you need)" + else reportResult opts t0 (Left OutOfMemory) + e -> if -1 == _confBenchmark opts then print e else reportResult opts t0 (Left TimeOut) + ) $ do when (0 < _confBenchmark opts) $ - void $ forkIO $ do let fromMicro = 1000000 :: Int - threadDelay $ fromMicro * fromIntegral (_confBenchmark opts) + void $ forkIO $ do let -- getCPUTime returns a pico sec. :: Integer, 1000 * 1000 * 1000 * 1000 + -- threadDelay requires a micro sec. :: Int, 1000 * 1000 + req = 1000000000000 * fromIntegral (_confBenchmark opts) :: Integer + waiting = do elp <- getCPUTime + when (elp < req) $ do + threadDelay . max 1000000 $ fromIntegral (req - elp) `div` 1000000 + waiting + waiting 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 + when (0 < _confDumpStat opts) $ dumpStats 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. +-- TODO: this function shuld return @IO String@ in someday. 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)) +reportResult opts t0 (Left OutOfMemory) = do + t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] Total: ") t0 + when (0 <= _confBenchmark opts) $ do + let fromPico = 1000000000000 :: Double + putStrLn ("\"" ++ takeWhile (' ' /=) versionId ++ "\"," + ++ show (_confBenchSeq opts) ++ "," + ++ "\"" ++ showPath opts ++ "\"," + ++ show (_confBenchmark opts) ++ "," ++ show (fromEnum OutOfMemory) + ) +reportResult opts t0 (Left TimeOut) = do + t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] Total: ") t0 + when (0 <= _confBenchmark opts) $ do + let fromPico = 1000000000000 :: Double + putStrLn ("\"" ++ takeWhile (' ' /=) versionId ++ "\"," + ++ show (_confBenchSeq opts) ++ "," + ++ "\"" ++ showPath opts ++ "\"," + ++ showFFloat (Just 3) (fromIntegral t2 / fromPico) "," + ++ show (fromEnum TimeOut) + ) + -- solver terminated normally -reportResult opts@(_targetFile -> Just cnfFile) t0 (Right result) = do - t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0 - case result of +reportResult opts t0 (Right result) = do + t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] Total: ") t0 + dumpName <- if _confNoAnswer opts then return Nothing else (Just <$> dumpAssigmentAsCNF opts result) + case (result, dumpName) 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 + (_, Just "") -> return () + (SAT _, Just o) -> hPutStrLn stderr $ "SATISFIABLE, saved to " ++ o ++ " for " ++ showPathBaseName opts + (SAT _, Nothing) -> hPutStrLn stderr $ "SATISFIABLE, " ++ showPathBaseName opts + (UNSAT _, Just o) -> hPutStrLn stderr $ "UNSATISFIABLE, saved to " ++ o ++ " for " ++ showPathBaseName opts + (UNSAT _, Nothing) -> hPutStrLn stderr $ "UNSATISFIABLE, " ++ showPathBaseName opts + valid <- if _confCheckAnswer opts -- or 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 + SAT asg -> flip validate asg =<< buildSolver opts 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 + void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] 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) + putStrLn ("\"" ++ takeWhile (' ' /=) versionId ++ "\"," + ++ show (_confBenchSeq opts) ++ "," + ++ "\"" ++ showPath opts ++ "\"," + ++ if valid + then showFFloat (Just 3) (fromIntegral t2 / fromPico) "," ++ show phase + else show (_confBenchmark opts) ++ "," ++ show (fromEnum InternalInconsistent)) reportResult _ _ _ = return () --- | new top-level interface that returns: +-- | NOT MAINTAINED NOW +-- new top-level interface that returns: -- -- * conflicting literal set :: Left [Int] -- * satisfiable assignment :: Right [Int] @@ -181,7 +228,6 @@ 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 @@ -191,21 +237,10 @@ _ -> 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) +executeValidator :: MiosProgramOption -> Solver -> IO () +executeValidator opts@(_targetFile -> target@(Left cnfFile)) s = do asg <- read <$> getContents unless (_confNoAnswer opts) $ print asg result <- s `validate` (asg :: [Int]) @@ -213,7 +248,7 @@ then putStrLn ("It's a valid assignment for " ++ cnfFile ++ ".") >> exitSuccess else putStrLn ("It's an invalid assignment for " ++ cnfFile ++ ".") >> exitFailure -executeValidator _ = return () +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@, @@ -233,103 +268,153 @@ -- -- >>> do y <- solve s ... ; dumpAssigmentAsCNF (Just "result.cnf") y <$> model s -- -dumpAssigmentAsCNF :: Maybe FilePath -> Certificate -> IO () -dumpAssigmentAsCNF Nothing _ = return () +dumpAssigmentAsCNF :: MiosProgramOption -> Certificate -> IO String -- | 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 +dumpAssigmentAsCNF opt (UNSAT _) = do + if _outputFile opt == Just "--" + then print "[]" >> return "" + else do let fname = case _outputFile opt of + Just x -> x + Nothing -> case _targetFile opt of + Left f -> ".ans_" ++ (reverse . takeWhile (/= '/') . reverse) f + Right _ -> ".ans_mios" + writeFile fname "s UNSAT\n0\n" + return fname +dumpAssigmentAsCNF opt (SAT l) = do + if _outputFile opt == Just "--" + then print l >> return "" + else do let fname = case _outputFile opt of + Just x -> x + Nothing -> case _targetFile opt of + Left f -> ".ans_" ++ (reverse . takeWhile (/= '/') . reverse) f + Right _ -> ".ans_mios" + withFile fname WriteMode $ \h -> do + hPutStrLn h "s SAT" + hPutStrLn h . (++ " 0") . unwords $ map show l + return fname +showPath :: MiosProgramOption -> String +showPath (_targetFile -> Left str) = str +showPath _ = "{a cnf embedded}" + +showPathBaseName :: MiosProgramOption -> String +showPathBaseName (_targetFile -> Left str) = (reverse . takeWhile (/= '/') . reverse) str +showPathBaseName _ = "aCNF" + +showPathFixed :: MiosProgramOption -> String +showPathFixed (_targetFile -> Left str) = replicate (len - length basename) ' ' ++ if elem '/' str then basename else basename' + where + len = 50 + basename = reverse . takeWhile (/= '/') . reverse $ str + basename' = take len str + +showPathFixed (_targetFile -> Right _) = replicate (len - length basename) ' ' ++ basename + where + len = 50 + basename = "embedded data" + -------------------------------------------------------------------------------- -- DIMACS CNF Reader -------------------------------------------------------------------------------- -- | parses the header of a CNF file -parseCNF :: Maybe FilePath -> IO (CNFDescription, B.ByteString) -parseCNF target@(Just cnfFile) = do +parseCNF :: Either FilePath String -> IO (CNFDescription, B.ByteString) +parseCNF pathOrData = do let -- format: p cnf n m, length "p cnf" == 5 + target = case pathOrData of + Left str -> str + Right _ -> "" 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 + 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 + case pathOrData of + Left cnfFile -> seek =<< B.readFile cnfFile + Right bdata -> seek $ B.pack bdata -- | parses ByteString then injects the clauses in it into a solver +{-# INLINABLE injectClausesFromCNF #-} 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 + buffer <- newVec (maxLit + 1) 0 :: IO (Vec Int) + let skipComments :: B.ByteString -> B.ByteString + skipComments !s = case B.uncons s of -- __Pre-condition:__ we are on the benngining of a line + Just ('c', b') -> skipComments . B.tail . B.dropWhile (/= '\n') $ b' + _ -> s + readClause :: Int -> B.ByteString -> IO () + readClause ((< nc) -> False) _ = return () + readClause !i !stream = do + let loop :: Int -> B.ByteString -> IO () + loop !j !b = case parseInt $ skipWhitespace b of + (k, b') -> if k == 0 + then do setNth buffer 0 $ j - 1 + res <- addClause s buffer + unless res $ set' (ok s) LiftedF + readClause (i + 1) b' + else do setNth buffer j (int2lit k) + loop (j + 1) b' + loop 1 . skipComments . B.dropWhile (`elem` " \t\n") $ stream + readClause 0 bs {-# 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 +skipWhitespace !s = B.dropWhile (== ' ') {- (`elem` " \t") -} s -{-# INLINABLE parseInt #-} +{-# INLINE 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" + loop :: (Int, B.ByteString) -> (Int, B.ByteString) + loop (val, s) = case B.uncons s of + Just (c, s') -> if '0' <= c && c <= '9' then loop (val * 10 + ord c - zero, s') else (val, s') + -- _ -> error (">>>>" ++ take 80 (B.unpack s)) + case B.uncons st of + Just ('-', st') -> let (k, x) = loop (0, st') in (negate k, x) + Just ('0', st') -> (0, st') + _ -> loop (0, st) -{-# 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 +-- | executes a solver on the given 'arg :: MiosConfiguration'. +-- This is another entry point for standalone programs. +showAnswerFromString :: String -> IO String +showAnswerFromString str = do + let opts = miosDefaultOption { _targetFile = Right str } + solverId <- myThreadId + desc <- fst <$> parseCNF (_targetFile opts) + token <- newEmptyMVar -- :: IO (MVar (Maybe Solver)) + t0 <- reportElapsedTime False "" 0 + s <- buildSolver opts + handle (\case + UserInterrupt -> return "User interrupt recieved." + ThreadKilled -> makeReport opts t0 =<< readMVar token + HeapOverflow -> if -1 == _confBenchmark opts + then return "Abort: a too large problem or heap exhausted" + else makeReport opts t0 (Left OutOfMemory) + e -> if -1 == _confBenchmark opts then return "unhandled iterrupt" else makeReport opts t0 (Left TimeOut) + ) $ do + when (0 < _confBenchmark opts) $ + void $ forkIO $ do let req = 1000000000000 * fromIntegral (_confBenchmark opts) :: Integer + waiting = do elp <- getCPUTime + when (elp < req) $ do + threadDelay $ fromIntegral (req - elp) `div` 1000000 + waiting + waiting + putMVar token (Left TimeOut) + killThread solverId + result <- solve s [] + putMVar token result + killThread solverId + return $ show desc + +makeReport :: MiosProgramOption -> Integer -> SolverResult -> IO String +makeReport opts t0 (Left OutOfMemory) = return "out of memory" +makeReport opts t0 (Left TimeOut) = return "time out" +makeReport opts t0 (Right (SAT asg)) = return $ show asg +makeReport opts t0 (Right (UNSAT _)) = return "UNSAT" +makeReport _ _ _ = return "" diff --git a/src/SAT/Mios/Clause.hs b/src/SAT/Mios/Clause.hs --- a/src/SAT/Mios/Clause.hs +++ b/src/SAT/Mios/Clause.hs @@ -13,6 +13,10 @@ ( Clause (..) , newClauseFromStack + , getRank + , setRank + -- , getActivity + -- , setActivity -- * Vector of Clause , ClauseVector , newClauseVector @@ -30,10 +34,10 @@ -- This matches both of @Clause@ and @GClause@ in MiniSat. data Clause = Clause { - rank :: !Int' -- ^ goodness like LBD; computed in 'Ranking' + lits :: !Stack -- ^ literals and rank + , rank :: !Int' -- ^ another metrics of this clause , activity :: !Double' -- ^ activity of this clause --- , protected :: !Bool' -- ^ protected from reduce - , lits :: !Stack -- ^ which this clause consists of +-- , protected :: !Bool' -- ^ protected from reduce } | NullClause -- as null pointer -- | BinaryClause Lit -- binary clause consists of only a propagating literal @@ -93,12 +97,31 @@ 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) + v <- newStack (n + 1) + 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 v <$> new' (if l then 1 else 0) <*> new' 0.0 + +-- | returns the rank, a goodness, of a given clause +{-# INLINE getRank #-} +getRank :: Clause -> IO Int +getRank Clause{..} = get' rank + +-- | sets the rank of a given clause +{-# INLINE setRank #-} +setRank :: Clause -> Int -> IO () +setRank Clause{..} k = set' rank k + +{- +{-# INLINE getActivity #-} +getActivity :: Clause -> IO Int +getActivity Clause{..} = do n <- get' lits; getNth lits (n + 2) + +{-# INLINE setActivity #-} +setActivity :: Clause -> Int -> IO () +setActivity Clause{..} k = do n <- get' lits; setNth lits (n + 2) k +-} -------------------------------------------------------------------------------- Clause Vector diff --git a/src/SAT/Mios/ClauseManager.hs b/src/SAT/Mios/ClauseManager.hs --- a/src/SAT/Mios/ClauseManager.hs +++ b/src/SAT/Mios/ClauseManager.hs @@ -20,6 +20,7 @@ , pushClauseWithKey , getKeyVector , markClause +-- , allocateKeyVectorSize -- * WatcherList , WatcherList , newWatcherList @@ -29,6 +30,7 @@ import Control.Monad (unless, when) import qualified Data.IORef as IORef +import qualified Data.Primitive.ByteArray as BA import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV import SAT.Mios.Types @@ -99,7 +101,7 @@ _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 + , _keyVector :: IORef.IORef (Vec Int) -- Int list } -- | 'ClauseExtManager' is a 'SingleStorage` on the number of clauses in it. @@ -120,7 +122,7 @@ !b <- IORef.readIORef _keyVector if MV.length v - 1 <= n then do - let len = max 8 $ MV.length v + let len = max 8 $ div (MV.length v) 2 v' <- MV.unsafeGrow v len b' <- growBy b len MV.unsafeWrite v' n c @@ -228,7 +230,7 @@ -- | returns the associated Int vector, which holds /blocking literals/. {-# INLINE getKeyVector #-} -getKeyVector :: ClauseExtManager -> IO (Vec [Int]) +getKeyVector :: ClauseExtManager -> IO (Vec Int) getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector -- | O(1) inserter @@ -241,7 +243,7 @@ !b <- IORef.readIORef _keyVector if MV.length v - 1 <= n then do - let len = max 8 $ MV.length v + let len = max 8 $ div (MV.length v) 2 v' <- MV.unsafeGrow v len b' <- growBy b len MV.unsafeWrite v' n c @@ -277,7 +279,10 @@ -- | 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) +newWatcherList n m = do let n' = int2lit (negate n) + 2 + v <- MV.unsafeNew n' + mapM_ (\i -> MV.unsafeWrite v i =<< newManager m) [0 .. n' - 1] + V.unsafeFreeze v -- | returns the watcher List for "Literal" /l/. {-# INLINE getNthWatcher #-} @@ -291,3 +296,20 @@ {-# 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] + +-------------------------------------------------------------------------------- + +-- | returns the associated Int vector, which holds /blocking literals/. +{-# INLINE setKeyVector #-} +setKeyVector :: ClauseExtManager -> Vec Int -> IO () +setKeyVector ClauseExtManager{..} v = IORef.writeIORef _keyVector v + +{-# INLINABLE allocateKeyVectorSize #-} +allocateKeyVectorSize :: ClauseExtManager -> Int -> IO (Vec Int) +allocateKeyVectorSize ClauseExtManager{..} n' = do + v <- IORef.readIORef _keyVector + if realLength v < n' -- never shrink it + then do v' <- newVec n' 0 + IORef.writeIORef _keyVector v' + return v' + else return v diff --git a/src/SAT/Mios/ClausePool.hs b/src/SAT/Mios/ClausePool.hs --- a/src/SAT/Mios/ClausePool.hs +++ b/src/SAT/Mios/ClausePool.hs @@ -47,29 +47,23 @@ let mgr = getManager pool i nn <- get' mgr if 0 < nn - then do c <- lastOf mgr - popFrom mgr - return c + then do c <- lastOf mgr; popFrom mgr; return c else pickup $ i + 1 n <- get' v - c <- pickup (n - 2) + c <- pickup (n - 2) -- mapping the number of literals for the smallest clauses to zero if c == NullClause then newClauseFromStack True v else do let lstack = lits c loop :: Int -> IO () - loop ((<= n) -> False) = return () + loop ((<= n) -> False) = set' (activity c) 0.0 -- setActivity c 1 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 + return c -- the caller (newLearntClause) should set rank and protected by himself -- | 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 + n <- subtract 2 <$> get' c -- the number of literals in a clause >= 2 + l <- getRank c + when (0 /= l && n <= storeLimit) $ pushTo (getManager pool n) c diff --git a/src/SAT/Mios/Criteria.hs b/src/SAT/Mios/Criteria.hs --- a/src/SAT/Mios/Criteria.hs +++ b/src/SAT/Mios/Criteria.hs @@ -1,7 +1,8 @@ -- | (This is a part of MIOS.) -- Advanced heuristics library for 'SAT.Mios.Main' {-# LANGUAGE - MultiWayIf + BangPatterns + , MultiWayIf , RecordWildCards , ViewPatterns #-} @@ -16,14 +17,21 @@ , varDecayActivity -- * Clause , addClause - -- * Literal Block Distance + -- * Clause Metrics , lbdOf + , updateNDD + , nddOf -- * Restart , checkRestartCondition + -- * Reporting + , dumpStats ) where -import Control.Monad (when) +import Control.Monad (void, when) +import Data.Bits +import Data.List (intercalate) +import Numeric (showFFloat) import SAT.Mios.Types import SAT.Mios.Clause import SAT.Mios.ClauseManager @@ -37,16 +45,18 @@ -- | __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 +varBumpActivity s@Solver{..} v = do + x <- getNth activities v + y <- fromIntegral <$> getStat s NumOfBackjump + let a = (x + y) / 2 + setNth activities v a when (varActivityThreshold < a) $ varRescaleActivity s - update s x -- update the position in heap + updateVO s v -- update the position in heap -- | __Fig. 14 (p.19)__ {-# INLINABLE varDecayActivity #-} varDecayActivity :: Solver -> IO () -varDecayActivity Solver{..} = modify' varInc (/ variableDecayRate config) +varDecayActivity Solver{..} = return () -- modify' varInc (/ variableDecayRate config) -- | __Fig. 14 (p.19)__ {-# INLINABLE varRescaleActivity #-} @@ -129,104 +139,44 @@ -- * @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 +clauseNew :: Solver -> Stack -> IO (Either Bool Clause) +clauseNew s@Solver{..} ps = do + n <- get' ps + sortStack ps + let loop :: Int -> Int -> Lit -> IO Bool + loop ((<= n) -> False) j _ = setNth ps 0 (j - 1) >> return False + loop !i !j !l' = do l <- getNth ps i -- check the i-th literal's satisfiability + sat <- valueLit s l + if | sat == LiftedT || negateLit l == l' -> reset ps >> return True + | sat /= LiftedF && l /= l' -> setNth ps j l >> loop (i + 1) (j + 1) l + | otherwise -> loop (i + 1) j l' + exit <- loop 1 1 LBottom 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) + 1 -> do l <- getNth ps 1 + Left <$> enqueue s l NullClause + _ -> do c <- newClauseFromStack False ps + let lstack = lits c + 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. +-- This function is called only before the solving phase to register the given clauses (not learnt). {-# INLINABLE addClause #-} addClause :: Solver -> Stack -> IO Bool addClause s@Solver{..} vecLits = do - result <- clauseNew s vecLits False + result <- clauseNew s vecLits case result of - Left b -> return b -- No new clause was returned becaues a confilct occured or the clause is a literal + Left b -> return b -- No clause is returned becaues a confilct occured or the clause is a literal Right c -> pushTo clauses c >> return True --------------------------------------------------------------------------------- LBD +-------------------------------------------------------------------------------- Clause Metrics --- | returns a POSIVITE value +-- | returns a POSIVITE value of Literal Block Distance {-# INLINABLE lbdOf #-} lbdOf :: Solver -> Stack -> IO Int lbdOf Solver{..} vec = do @@ -262,66 +212,138 @@ _ -> return () -} --------------------------------------------------------------------------------- restart +-- | returns a vector index of NDD for the nth bit of a var +{-# INLINE varBit2vIndex #-} +varBit2vIndex :: Int -> Int -> Int +varBit2vIndex v ((`mod` 124) -> b) + | 62 <= b = 2 * v + 1 + | otherwise = 2 * v -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 | +-- | returns a bit index of NDD for the nth bit of a var +{-# INLINE varBit2bIndex #-} +varBit2bIndex :: Int -> Int -> Int +varBit2bIndex v b = mod b 62 -ema0 :: Int -ema0 = 2 ^ (14 :: Int) -- = floor $ 1 / ema2 +-- | updates a /var/'s ndl, which is assigned by a 'reason' /clause/ +{-# INLINE updateNddOf #-} +updateNddOf :: Solver -> Var -> Clause -> IO () +updateNddOf Solver{..} v NullClause = do + l <- getNth level v + setNth ndd (varBit2vIndex v l) $ if l == 0 then 0 else setBit 0 (varBit2bIndex v l) --- | #62 -checkRestartCondition :: Solver -> Int -> IO Bool -checkRestartCondition s@Solver{..} (fromIntegral -> lbd) = do - k <- getStat s NumOfRestart - let step = 100 +updateNddOf Solver{..} v Clause{..} = do + n <- get' lits + let iv = varBit2vIndex v 0 + setNth ndd iv 0 + setNth ndd (iv + 1) 0 + let loop :: Int -> Int -> Int -> IO () + loop ((<= n) -> False) low high = do setNth ndd iv low + setNth ndd (iv + 1) high + loop i low high = do v' <- lit2var <$> getNth lits i + let jv = varBit2vIndex v' 0 + low' <- (low .|.) <$> getNth ndd jv + high' <- (high .|.) <$> getNth ndd (jv + 1) + loop (i + 1) low' high' + loop 1 0 0 + +-- | updates all assigned vars' ndl +{-# INLINABLE updateNDD #-} +updateNDD :: Solver -> IO () +updateNDD s@Solver{..} = do + n <- get' trail + let -- thr = if ns == 0 then 0 else floor . logBase 2 $ lv / ns :: Int + update :: Int -> IO () + update ((<= n) -> False) = return () + update i = do v <- lit2var <$> getNth trail i + updateNddOf s v =<< getNth reason v + update (i + 1) + update 1 + +-- | returns the NDL +{-# INLINABLE nddOf #-} +nddOf :: Solver -> Stack -> IO Int +nddOf Solver{..} stack = do + n <- get' stack + let loop :: Int -> Int -> Int -> IO Int -- var -> #lowbits -> #highbits + loop ((<= n) -> False) low high = return $ popCount low + popCount high + loop i low high = do v <- lit2var <$> getNth stack i + let iv = varBit2vIndex v 0 + l <- getNth ndd iv + h <- getNth ndd (iv + 1) + loop (i + 1) (low .|. l) (high .|. h) + max 1 <$> loop 1 0 0 + +-------------------------------------------------------------------------------- restart + +-- | #62, #74, #91 +checkRestartCondition :: Solver -> Int -> Int -> IO Bool +checkRestartCondition s@Solver{..} (fromIntegral -> lbd) (fromIntegral -> cLv) = do next <- get' nextRestart - count <- getStat s NumOfBackjump + count <- getStat s NumOfBackjump -- it should be > 0 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 + bLv <- fromIntegral <$> decisionLevel s + df <- updateEMA emaDFast lbd + ds <- updateEMA emaDSlow lbd + af <- updateEMA emaAFast nas + as <- updateEMA emaASlow nas + void $ updateEMA emaCDLvl cLv + nb <- getStat s NumOfBlockRestart + nf <- getStat s NumOfRestart + let bias = if | nb <= 10 -> 0 + | nb <= nf -> 0.1 * (fromIntegral nf / fromIntegral nb) ** 2 + | otherwise -> 0.1 * negate ((fromIntegral nb / fromIntegral nf) ** 2) + block = 1.25 * as < af + force = (1.25 + bias) * ds < df + updateParams ki = do + gef <- (max 0) . (+ ki) <$> get' restartExp + set' nextRestart $ count + 100 + ceiling (50 * gef) + set' restartExp gef + updateBDL = updateEMA emaBDLvl bLv >> return False + restartBDL = do + updateEMA emaBDLvl 0 + -- do z <- get' restartExp; when (0.4 < z) $ print (nb, nf, bias, z) + when (3 == dumpSolverStatMode config) $ dumpStats DumpCSV s + return True + if | count < next -> updateBDL + | block -> 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 + updateParams 1.0 >> updateBDL + | force -> do incrementStat s NumOfRestart 1 - set' nextRestart (count + step) - when (3 == dumpStat config) $ dumpSolver DumpCSV s - return True - | otherwise -> return False + updateParams (-0.1) >> restartBDL + | otherwise -> do + updateParams (-0.9) >> updateBDL -{- -{-# 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) --} +-------------------------------------------------------------------------------- dump + +emaLabels :: [(String, Solver -> EMA)] +emaLabels = [ ("emaAFast", emaAFast) + , ("emaASlow", emaASlow) + , ("emaBDLvl", emaBDLvl) + , ("emaCDLvl", emaCDLvl) + , ("emaDFast", emaDFast) + , ("emaDSlow", emaDSlow) + ] + +{-# INLINABLE dumpStats #-} +-- | print statatistic data to stdio. This should be called after each restart. +dumpStats :: DumpMode -> Solver -> IO () +dumpStats NoDump _ = return () +dumpStats DumpCSVHeader s@Solver{..} = do + sts <- init <$> getStats s + putStrLn . intercalate "," $ map (show . fst) sts ++ map fst emaLabels +dumpStats DumpCSV s@Solver{..} = do + -- update the stat data before dump + 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 + sts <- init <$> getStats s + let fs :: (Solver -> EMA) -> IO String + fs e = do x <- getEMA (e s) + return $ showFFloat (Just 3) x "" + vals <- mapM (fs . snd) emaLabels + putStrLn . intercalate "," $ map (show . snd) sts ++ vals +-- | FIXME: use Util/Stat +dumpStats DumpJSON _ = return () -- mode 2: JSON diff --git a/src/SAT/Mios/Main.hs b/src/SAT/Mios/Main.hs --- a/src/SAT/Mios/Main.hs +++ b/src/SAT/Mios/Main.hs @@ -16,7 +16,7 @@ , newSolver , setAssign , addClause - , dumpSolver + , dumpStats -- * Main function , simplifyDB , solve @@ -64,14 +64,13 @@ 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 + 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 -- get the index of the literal with highest level -- Bump, enqueue, store clause: claBumpActivity s c -- Add clause to all managers @@ -84,7 +83,7 @@ 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 + setRank c lbd -- assert (0 < rank c) -- set' (protected c) True return lbd @@ -142,7 +141,7 @@ 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) + d <- getRank c when (0 /= d) $ claBumpActivity s c -- update LBD like #Glucose4.0 when (2 < d) $ do @@ -150,7 +149,7 @@ 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 + setRank c nblevels -- Update it sc <- get' c let lstack = lits c loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int) @@ -169,7 +168,7 @@ -- UPDATEVARACTIVITY: glucose heuristics r <- getNth reason v when (r /= NullClause) $ do - ra <- get' (rank r) + ra <- getRank r when (0 /= ra) $ pushTo an'lastDL q -- end of glucose heuristics loopOnLiterals (j + 1) b (pc + 1) @@ -198,7 +197,7 @@ 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 + -- restrict the search depth (range) to [0 .. 63] merger (i + 1) . setBit b . (63 .&.) =<< getNth level (lit2var l) levels <- merger 2 0 let loopOnLits :: Int -> Int -> IO () @@ -439,6 +438,7 @@ reduceDB s@Solver{..} = do n <- nLearnts s cvec <- getClauseVector learnts + n' <- get' trail let loop :: Int -> IO () loop ((< n) -> False) = return () loop i = do @@ -464,17 +464,13 @@ -- constants for sort key layout rankWidth :: Int -rankWidth = 10 +rankWidth = 11 activityWidth :: Int -activityWidth = 50 -- note: the maximum clause activity is 1e20. -indexWidth :: Int -indexWidth = 32 -- 4G +activityWidth = 51 -- note: the maximum clause activity is 1e20. 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. @@ -483,23 +479,23 @@ -- 2. smaller LBD -- 3. larger activity defined as MiniSat -- --- they are encoded into two "Int64"s as the following (10+52+32 layout): +-- They are encoded into an "Int64" as the following (11+51 layout): -- --- * 10 bits for rank (LBD): 'rankWidth' --- * 50 bits for converted activity: 'activityWidth' --- * 32 bits for clauseVector index: 'indexWidth' +-- * 11 bits for rank (LBD): 'rankWidth' +-- * 51 bits for converted activity: 'activityWidth' -- 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) + kvec <- getKeyVector cm at <- (0.1 *) . (/ fromIntegral n) <$> get' (claInc s) -- activity threshold -- 1: assign keys + updateNDD s + cl <- getEMA (emaCDLvl s) + surface <- if cl == 0 then return 0 else (/ cl) <$> getEMA (emaBDLvl s) -- 0 <=backjumped level / coflict level < 1.0 let shiftLBD = activityWidth - shiftIndex = shiftL 1 indexWidth am = fromIntegral activityMax :: Double scaleAct :: Double -> Int scaleAct x @@ -508,78 +504,60 @@ 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 + then do setNth kvec i 0 assignKey (i + 1) (t + 1) - else do a <- get' (activity c) -- Second one... based on LBD - r <- get' (rank c) + else do a <- get' (activity c) -- Second one... based on LBD + rLBD <- fromIntegral <$> getRank c -- above the level + rNDD <- fromIntegral <$> nddOf s (lits c) -- under the level + let r = if rNDD == 1 -- this implies rLBD == 1. + then 1 + else ceiling $ rLBD ** surface * rNDD ** (1 - surface) 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 + setNth kvec 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 () + let sortOnRange :: Int -> Int -> IO () sortOnRange left right - | limit2 < left = return () + | limit < 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) + | left + 1 == right = do + a <- getNth kvec left + b <- getNth kvec right + unless (a < b) $ do setNth kvec left b + setNth kvec right a + swapBetween vec left right | 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 p = div (left + right) 2 + pivot <- getNth kvec p + swapBetween kvec p left -- set a sentinel for r' + swapBetween vec p left 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 + nextL i = do v <- getNth kvec 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 - 2) else return i + nextR i = do v <- getNth kvec 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 do swapBetween keys l' r' - swapBetween keys (l' + 1) (r' + 1) - divide (l' + 2) (r' - 2) + then do swapBetween kvec l' r' + swapBetween vec l' r' + divide (l' + 1) (r' - 1) 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 + m <- divide (left + 1) right + swapBetween kvec left m + swapBetween vec left m + sortOnRange left (m - 1) + sortOnRange (m + 1) right + sortOnRange 0 (n - 1) return limit -- | #M22 @@ -637,6 +615,7 @@ search :: Solver -> IO Bool search s@Solver{..} = do -- clear model + let delta = (sqrt . fromIntegral) nVars let loop :: Bool -> IO Bool loop restart = do confl <- propagate s @@ -662,16 +641,15 @@ t' <- (* 1.5) <$> get' learntSAdj set' learntSAdj t' set' learntSCnt $ floor t' - -- modify' maxLearnts (* 1.1) - modify' maxLearnts (+ 300) - loop =<< checkRestartCondition s lbd' + modify' maxLearnts (+ delta) + loop =<< checkRestartCondition s lbd' d 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 + when (2 == dumpSolverStatMode config) $ dumpStats DumpCSV s if | k2 == nVars -> return True -- Model found | restart -> do -- Reached bound on number of conflicts (s `cancelUntil`) =<< get' rootLevel -- force a restart @@ -690,7 +668,7 @@ -} loop False | otherwise -> do -- New variable decision - v <- select s + v <- selectVO s -- #phasesaving <<<< many have heuristic for polarity here oldVal <- getNth phases v unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@ @@ -723,8 +701,9 @@ cancelUntil s 0 return False else return True + check_given <- get' ok good <- simplifyDB s - x <- if good then foldrM inject True assumps else return False + x <- if check_given /= LiftedF && good then foldrM inject True assumps else return False if x then do set' rootLevel =<< decisionLevel s status <- search s @@ -733,7 +712,7 @@ 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 + when (0 < dumpSolverStatMode config) $ dumpStats DumpCSV s cancelUntil s 0 -- reset solver flag <- get' ok if | status && flag == LiftedT -> return $ Right (SAT asg1) diff --git a/src/SAT/Mios/OptionParser.hs b/src/SAT/Mios/OptionParser.hs --- a/src/SAT/Mios/OptionParser.hs +++ b/src/SAT/Mios/OptionParser.hs @@ -23,41 +23,43 @@ -- | configuration swithces data MiosProgramOption = MiosProgramOption { - _targetFile :: Maybe String - , _targets :: [String] - , _outputFile :: Maybe String - , _confVariableDecayRate :: !Double - , _confClauseDecayRate :: Double + _targetFile :: Either String String -- path or data + , _targets :: [String] + , _outputFile :: Maybe String + , _confVariableDecayRate :: Double + , _confClauseDecayRate :: Double + , _confRestartE :: Double + , _confRestartS :: Double -- , _confRandomDecisionRate :: Int - , _confMaxSize :: !Int - , _confCheckAnswer :: !Bool - , _confVerbose :: !Bool - , _confBenchmark :: Integer - , _confBenchSeq :: !Int - , _confNoAnswer :: !Bool - , _confDumpStat :: !Int - , _validateAssignment :: !Bool - , _displayHelp :: !Bool - , _displayVersion :: !Bool + , _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 + _targetFile = Left "" , _targets = [] , _outputFile = Nothing , _confVariableDecayRate = variableDecayRate defaultConfiguration , _confClauseDecayRate = clauseDecayRate defaultConfiguration --- , _confRandomDecisionRate = randomDecisionRate defaultConfiguration - , _confMaxSize = 4000000 -- 4,000,000 = 4M + , _confRestartE = restartExpansion defaultConfiguration + , _confRestartS = restartStep defaultConfiguration + --, _confRandomDecisionRate = randomDecisionRate defaultConfiguration , _confCheckAnswer = False , _confVerbose = False , _confBenchmark = -1 , _confBenchSeq = 0 , _confNoAnswer = False - , _confDumpStat = dumpStat defaultConfiguration + , _confDumpStat = dumpSolverStatMode defaultConfiguration , _validateAssignment = False , _displayHelp = False , _displayVersion = False @@ -73,12 +75,15 @@ , 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 [] ["Re"] + (ReqArg (\v c -> c { _confRestartE = read v }) (show (_confRestartE miosDefaultOption))) + "[solver] expansion rate for blocking/forcing restart (>= 1.0)" + , Option [] ["Rs"] + (ReqArg (\v c -> c { _confRestartS = read v }) (show (_confRestartS miosDefaultOption))) + "[solver] a fixed number of conflicts between restarts" -- , 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" @@ -87,7 +92,7 @@ "[solver] self-check (satisfiable) assignment" , Option ['o'] ["output"] (ReqArg (\v c -> c { _outputFile = Just v }) "file") - "[option] filename to store result" + "[option] filename to store result, '--' for stdout" {- , Option [] ["stdin"] (NoArg (\c -> c { _targetFile = Nothing })) @@ -106,7 +111,7 @@ (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))) + (ReqArg (\v c -> c { _confDumpStat = read v }) (show (dumpSolverStatMode defaultConfiguration))) "[devel] dump level; 1:solved, 2:reduction, 3:restart" , Option ['h'] ["help"] (NoArg (\c -> c { _displayHelp = True })) @@ -127,7 +132,7 @@ (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 } + return $ conf { _targetFile = Left (head l), _targets = l } (_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes)) -- | builds "MiosProgramOption" from a String @@ -141,5 +146,8 @@ variableDecayRate = _confVariableDecayRate opts , clauseDecayRate = _confClauseDecayRate opts -- , randomDecisionRate = _confRandomDecisionRate opts - , dumpStat = _confDumpStat opts + , dumpSolverStatMode = _confDumpStat opts + , emaCoeffs = emaCoeffs defaultConfiguration + , restartExpansion = _confRestartE opts + , restartStep = _confRestartS opts } diff --git a/src/SAT/Mios/Solver.hs b/src/SAT/Mios/Solver.hs --- a/src/SAT/Mios/Solver.hs +++ b/src/SAT/Mios/Solver.hs @@ -33,7 +33,6 @@ , setStat , incrementStat , getStats - , dumpSolver ) where @@ -60,6 +59,7 @@ , 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 + , ndd :: !(Vec Int) -- ^ For each variable, the number of depending decisions , conflicts :: !Stack -- ^ Set of literals in the case of conflicts -------- Variable Order , activities :: !(Vec Double) -- ^ Heuristic measurement of the activity of a variable @@ -82,16 +82,19 @@ , 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 + , 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 + -------- restart heuristics #62, clause evaluation criteria #74 + , emaAFast :: !EMA -- ^ Number of Assignments Fast + , emaASlow :: !EMA -- ^ Number of Assignments Slow + , emaBDLvl :: !EMA -- ^ Backjumped and Restart Dicision Level + , emaCDLvl :: !EMA -- ^ Conflicting Level + , emaDFast :: !EMA -- ^ (Literal Block) Distance Fast + , emaDSlow :: !EMA -- ^ (Literal Block) Distance Slow , nextRestart :: !Int' -- ^ next restart in number of conflict - , restartMode :: Int' -- ^ mode of restart + , restartExp :: !Double' -- ^ incremented by blocking + , emaRstBias :: !EMA -- ^ average phase of restart } -- | returns an everything-is-initialized solver from the arguments. @@ -101,7 +104,7 @@ -- Clause Database <$> newManager dummy_nc -- clauses <*> newManager 2000 -- learnts - <*> newWatcherList nv 2 -- watches + <*> newWatcherList nv 1 -- watches -- Assignment Management <*> newVec nv LBottom -- assigns <*> newVec nv LBottom -- phases @@ -110,6 +113,7 @@ <*> new' 0 -- qHead <*> newClauseVector (nv + 1) -- reason <*> newVec nv (-1) -- level + <*> newVec (2 * (nv + 1)) 0 -- ndd <*> newStack nv -- conflicts -- Variable Order <*> newVec nv 0 -- activities @@ -136,12 +140,17 @@ <*> 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 + <*> newEMA False ef -- emaAFast + <*> newEMA True es -- emaASlow + <*> newEMA True 2 -- emaBDLvl + <*> newEMA True 2 -- emaCDLvl + <*> newEMA False ef -- emaDFast + <*> newEMA True es -- emaDSlow <*> new' 100 -- nextRestart - <*> new' 1 -- restartMode + <*> new' 0.0 -- restartExp + <*> newEMA False 100 -- emaRstBias + where + (ef, es) = emaCoeffs conf -------------------------------------------------------------------------------- -- Accessors @@ -267,7 +276,7 @@ -- 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 + undoVO s x -- insertHeap s x -- insertVerOrder loopOnTrail $ c - 1 loopOnTrail ts @@ -295,12 +304,12 @@ -- 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 + {-# SPECIALIZE INLINE updateVO :: Solver -> Var -> IO () #-} + updateVO = increaseHeap + {-# SPECIALIZE INLINE undoVO :: Solver -> Var -> IO () #-} + undoVO s v = inHeap s v >>= (`unless` insertHeap s v) + {-# SPECIALIZE INLINE selectVO :: Solver -> IO Var #-} + selectVO s = do let asg = assigns s -- | returns the most active var (heap-based implementation) @@ -418,37 +427,3 @@ 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 --- a/src/SAT/Mios/Types.hs +++ b/src/SAT/Mios/Types.hs @@ -37,6 +37,11 @@ , Int (LiftedF, LiftedT, LBottom, Conflict) -- a heap , VarOrder (..) + -- Exponential Moving Average, EMA + , EMA + , newEMA + , getEMA + , updateEMA -- * statistics , StatIndex (..) , DumpMode (..) @@ -250,36 +255,72 @@ newVar = error "newVar undefined" -} -- | should be called when a variable has increased in activity. - update :: o -> Var -> IO () - update _ = error "update undefined" + updateVO :: o -> Var -> IO () + updateVO _ = 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" + undoVO :: o -> Var -> IO () + undoVO _ _ = error "undo undefined" -- | returns a new, unassigned var as the next decision. - select :: o -> IO Var - select = error "select undefined" + selectVO :: o -> IO Var + selectVO = error "select undefined" +-------------------------------------------------------------------------------- EMA + +-- | Exponential Moving Average, EMA +type EMA = (Double', Maybe Double', Double) + +-- | returns a new EMA from a flag (slow or fast) and a window size +{-# INLINE newEMA #-} +newEMA :: Bool -> Int -> IO EMA +newEMA True s = do v <- new' 0.0 + c <- new' 0.0 + return (v, Just c, 1 / fromIntegral s) +newEMA False s = do v <- new' 0.0; return (v, Nothing, 1 / fromIntegral s) + +-- | returns an EMA value +{-# INLINE getEMA #-} +getEMA :: EMA -> IO Double +getEMA (ema, Just cal, _) = do x <- get' ema + c <- get' cal + return $ if c == 0 then 0 else x / c +getEMA (ema, Nothing, _) = get' ema + +-- | updates an EMA +{-# INLINE updateEMA #-} +updateEMA :: EMA -> Double -> IO Double +updateEMA (ema, Just cal, cof) x = do e <- ((cof * x) +) . ((1 - cof) *) <$> get' ema + set' ema e + c <- ((cof * 1) +) . ((1 - cof) *) <$> get' cal + set' cal c + return $ e / c +updateEMA (ema, Nothing, cof) x = do e <- ((cof * x) +) . ((1 - cof) *) <$> get' ema; set' ema e; return e + +-------------------------------------------------------------------------------- CNF + -- | 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 + , _pathname :: !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 + variableDecayRate :: !Double -- ^ decay rate for variable activity + , clauseDecayRate :: !Double -- ^ decay rate for clause activity + , dumpSolverStatMode :: !Int -- ^ dump stats data during solving + , emaCoeffs :: !(Int, Int) -- ^ the coefficients for restarts + , restartExpansion :: !Double -- ^ restart expansion factor + , restartStep :: !Double -- ^ static Steps between restarts } deriving (Eq, Ord, Read, Show) @@ -291,7 +332,9 @@ -- * Mios-1.2 uses @(0.95, 0.999, 0)@. -- defaultConfiguration :: MiosConfiguration -defaultConfiguration = MiosConfiguration 0.95 0.999 0 +defaultConfiguration = MiosConfiguration 0.95 0.999 0 (ef, es) 1.15 100 + where ef = (2 :: Int) ^ ( 5 :: Int) + es = (2 :: Int) ^ (14 :: Int) -------------------------------------------------------------------------------- Statistics diff --git a/src/SAT/Mios/Vec.hs b/src/SAT/Mios/Vec.hs --- a/src/SAT/Mios/Vec.hs +++ b/src/SAT/Mios/Vec.hs @@ -24,7 +24,7 @@ , StackFamily (..) , Stack , newStackFromList - , realLengthOfStack + , realLength , sortStack ) where @@ -98,67 +98,6 @@ 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) @@ -181,10 +120,14 @@ BA.writeByteArray v j (x :: Int) {-# SPECIALIZE INLINE reset :: ByteArrayInt -> IO () #-} reset (ByteArrayInt v) = BA.writeByteArray v 0 (0 :: Int) + {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO ByteArrayInt #-} 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 + growBy (ByteArrayInt v) n = do v' <- BA.newByteArray (BA.sizeofMutableByteArray v + 8 * n) + BA.copyMutableByteArray v' 0 v 0 (BA.sizeofMutableByteArray v) + return (ByteArrayInt v') asList (ByteArrayInt v) = mapM (BA.readByteArray v) [0 .. div (BA.sizeofMutableByteArray v) 8 - 1] instance VecFamily ByteArrayDouble Double where @@ -201,12 +144,18 @@ BA.writeByteArray v j (x :: Int) {-# SPECIALIZE INLINE reset :: ByteArrayDouble -> IO () #-} reset (ByteArrayDouble v) = BA.writeByteArray v 0 (0 :: Double) + {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO ByteArrayDouble #-} 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] +-- | returns the number of allocated slots +{-# INLINE realLength #-} +realLength :: Vec Int -> Int +realLength (ByteArrayInt v) = div (BA.sizeofMutableByteArray v) 8 + -------------------------------------------------------------------------------- SingleStorage -- | Interface for single (one-length vector) mutable data @@ -318,37 +267,32 @@ 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 + 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 + if a < b then return () else setNth vec left b >> setNth vec right a | 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 + 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 + 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 + 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' diff --git a/test/MiosSpec.hs b/test/MiosSpec.hs new file mode 100644 --- /dev/null +++ b/test/MiosSpec.hs @@ -0,0 +1,14 @@ +module MiosSpec (spec) where + +import System.IO.Unsafe +import Test.Hspec +import SAT.Mios + +testRun :: Spec +testRun = do + describe "SAT problems" $ do + let res = unsafePerformIO $ solveSAT (CNFDescription 4 5 Nothing) [[1,2,-3], [-1, -4], [2,4], [1,-3,4], [-3,4]] + it "a simple SAT" $ res `shouldBe` [-1,2,-3,-4] + +spec :: Spec +spec = testRun diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,8 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-} +-- main :: IO () +-- main = putStrLn "Test suite not yet implemented" + +--import SAT.Mios +--main :: IO () +--main = do +-- print =<< solveSAT (CNFDescription 4 5 "") [[1,2,-3], [-1, -4], [2,4], [1,-3,4], [-3,4]]