module SAT.Mios.Criteria
(
claBumpActivity
, claDecayActivity
, varBumpActivity
, varDecayActivity
, addClause
, lbdOf
, checkRestartCondition
)
where
import Control.Monad (when)
import SAT.Mios.Types
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
import SAT.Mios.Solver
varActivityThreshold :: Double
varActivityThreshold = 1e100
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
varDecayActivity :: Solver -> IO ()
varDecayActivity Solver{..} = modify' varInc (/ variableDecayRate config)
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)
claActivityThreshold :: Double
claActivityThreshold = 1e20
claBumpActivity :: Solver -> Clause -> IO ()
claBumpActivity s@Solver{..} Clause{..} = do
a <- (+) <$> get' activity <*> get' claInc
set' activity a
when (claActivityThreshold <= a) $ claRescaleActivity s
claDecayActivity :: Solver -> IO ()
claDecayActivity Solver{..} = modify' claInc (/ clauseDecayRate config)
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)
clauseNew :: Solver -> Stack -> Bool -> IO (Either Bool Clause)
clauseNew s@Solver{..} ps isLearnt = do
exit <- do
let
handle :: Int -> Int -> Int -> IO Bool
handle j l n
| j > n = return False
| otherwise = do
y <- getNth ps j
if | y == l -> do
swapBetween ps j n
modifyNth ps (subtract 1) 0
handle j l (n 1)
| y == l -> reset ps >> return True
| 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
sat <- valueLit s l
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
c <- newClauseFromStack isLearnt ps
let lstack = lits c
when isLearnt $ do
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'
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
max_i <- findMax 1 1 0
swapBetween lstack 2 max_i
claBumpActivity s 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)
addClause :: Solver -> Stack -> IO Bool
addClause s@Solver{..} vecLits = do
result <- clauseNew s vecLits False
case result of
Left b -> return b
Right c -> pushTo clauses c >> return True
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
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
ema1, ema2, ema3, ema4 :: Double
ema1 = 2 ** (5)
ema2 = 2 ** (14)
ema3 = 2 ** (5)
ema4 = 2 ** (12)
ema0 :: Int
ema0 = 2 ^ (14 :: Int)
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
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
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