module SAT.Solver.Mios.Solver
(
Solver (..)
, newSolver
, nAssigns
, nClauses
, nLearnts
, decisionLevel
, valueVar
, valueLit
, locked
, VarHeap
, addClause
, enqueue
, assume
, cancelUntil
, getModel
, claBumpActivity
, claDecayActivity
, varBumpActivity
, varDecayActivity
, StatIndex (..)
, incrementStat
, getStats
)
where
import Control.Monad ((<=<), forM_, unless, when)
import SAT.Solver.Mios.Types
import SAT.Solver.Mios.Internal
import SAT.Solver.Mios.Clause
import SAT.Solver.Mios.ClauseManager
data Solver = Solver
{
model :: !VecBool
, conflict :: !Stack
, clauses :: !ClauseExtManager
, learnts :: !ClauseExtManager
, watches :: !WatcherList
, assigns :: !Vec
, phases :: !Vec
, trail :: !Stack
, trailLim :: !Stack
, qHead :: !IntSingleton
, reason :: !ClauseVector
, level :: !Vec
, activities :: !VecDouble
, order :: !VarHeap
, config :: !MiosConfiguration
, nVars :: !Int
, claInc :: !DoubleSingleton
, varInc :: !DoubleSingleton
, rootLevel :: !IntSingleton
, ok :: !BoolSingleton
, an'seen :: !Vec
, an'toClear :: !Stack
, an'stack :: !Stack
, pr'seen :: !Vec
, lbd'seen :: !Vec
, lbd'key :: !IntSingleton
, litsLearnt :: !Stack
, lastDL :: !Stack
, stats :: !Vec
}
newSolver :: MiosConfiguration -> CNFDescription -> IO Solver
newSolver conf (CNFDescription nv nc _) = do
Solver
<$> newVecBool nv False
<*> newStack nv
<*> newManager nc
<*> newManager nc
<*> newWatcherList nv 2
<*> newVecWith (nv + 1) lBottom
<*> newVecWith (nv + 1) lBottom
<*> newStack nv
<*> newStack nv
<*> newInt 0
<*> newClauseVector (nv + 1)
<*> newVecWith (nv + 1) (1)
<*> newVecDouble (nv + 1) 0
<*> newVarHeap nv
<*> return conf
<*> return nv
<*> newDouble 1.0
<*> newDouble 1.0
<*> newInt 0
<*> newBool True
<*> newVec (nv + 1)
<*> newStack nv
<*> newStack nv
<*> newVecWith (nv + 1) (1)
<*> newVec nv
<*> newInt 0
<*> newStack nv
<*> newStack nv
<*> newVec (1 + fromEnum (maxBound :: StatIndex))
nAssigns :: Solver -> IO Int
nAssigns = sizeOfStack . trail
nClauses :: Solver -> IO Int
nClauses = numberOfClauses . clauses
nLearnts :: Solver -> IO Int
nLearnts = numberOfClauses . learnts
getModel :: Solver -> IO [Int]
getModel s = zipWith (\n b -> if b then n else negate n) [1 .. ] <$> asList (model s)
decisionLevel :: Solver -> IO Int
decisionLevel Solver{..} = sizeOfStack trailLim
valueVar :: Solver -> Var -> IO Int
valueVar s !x = getNth (assigns s) x
valueLit :: Solver -> Lit -> IO Int
valueLit Solver{..} !p = if positiveLit p then getNth assigns (lit2var p) else negate <$> getNth assigns (lit2var p)
locked :: Solver -> Clause -> IO Bool
locked Solver{..} c@Clause{..} = (c ==) <$> (getNthClause reason . lit2var =<< getNth lits 1)
data StatIndex =
NumOfBackjump
| NumOfRestart
deriving (Bounded, Enum, Eq, Ord, Read, Show)
incrementStat :: Solver -> StatIndex -> Int -> IO ()
incrementStat (config -> collectStats -> False) _ _ = return ()
incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i
getStats :: Solver -> IO [(StatIndex, Int)]
getStats (config -> collectStats -> False) = return []
getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex]
addClause :: Solver -> Vec -> IO Bool
addClause s@Solver{..} vecLits = do
result <- clauseNew s vecLits False
case result of
(False, _) -> return False
(True, c) -> do
unless (c == NullClause) $ pushClause clauses c
return True
clauseNew :: Solver -> Vec -> Bool -> IO (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
case () of
_ | y == l -> do
swapBetween ps j n
modifyNth ps (subtract 1) 0
handle j l (n 1)
_ | y == l -> setNth ps 0 0 >> return True
_ -> handle (j + 1) l n
loopForLearnt :: Int -> IO Bool
loopForLearnt i = do
n <- getNth ps 0
if n < i
then return False
else do
l <- getNth ps i
sat <- handle (i + 1) l n
if sat
then return True
else loopForLearnt $ i + 1
loop :: Int -> IO Bool
loop i = do
n <- getNth ps 0
if n < i
then return False
else do
l <- getNth ps i
sat <- valueLit s l
case sat of
1 -> setNth ps 0 0 >> return True
1 -> do
swapBetween ps i n
modifyNth ps (subtract 1) 0
loop i
_ -> do
sat' <- handle (i + 1) l n
if sat'
then return True
else loop $ i + 1
if isLearnt then loopForLearnt 1 else loop 1
k <- getNth ps 0
case k of
0 -> return (exit, NullClause)
1 -> do
l <- getNth ps 1
(, NullClause) <$> enqueue s l NullClause
_ -> do
c <- newClauseFromVec isLearnt ps
let vec = asVec 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 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
max_i <- findMax 0 0 0
swapBetween vec 1 max_i
claBumpActivity s c
forM_ [0 .. k 1] $ varBumpActivity s . lit2var <=< getNth vec
l0 <- negateLit <$> getNth vec 0
pushClauseWithKey (getNthWatcher watches l0) c 0
l1 <- negateLit <$> getNth vec 1
pushClauseWithKey (getNthWatcher watches l1) c 0
return (True, c)
enqueue :: Solver -> Lit -> Clause -> IO Bool
enqueue s@Solver{..} p from = do
let signumP = if positiveLit p then lTrue else lFalse
let v = lit2var p
val <- valueVar s v
if val /= lBottom
then do
return $ val == signumP
else do
setNth assigns v $! signumP
setNth level v =<< decisionLevel s
setNthClause reason v from
pushToStack trail p
return True
assume :: Solver -> Lit -> IO Bool
assume s@Solver{..} p = do
pushToStack trailLim =<< sizeOfStack trail
enqueue s p NullClause
cancelUntil :: Solver -> Int -> IO ()
cancelUntil s@Solver{..} lvl = do
dl <- decisionLevel s
when (lvl < dl) $ do
let tr = asVec trail
let tl = asVec trailLim
lim <- getNth tl lvl
ts <- sizeOfStack trail
ls <- sizeOfStack trailLim
let
loopOnTrail :: Int -> IO ()
loopOnTrail ((lim <=) -> False) = return ()
loopOnTrail c = do
x <- lit2var <$> getNth tr c
setNth phases x =<< getNth assigns x
setNth assigns x lBottom
setNthClause reason x NullClause
undo s x
loopOnTrail $ c 1
loopOnTrail $ ts 1
shrinkStack trail (ts lim)
shrinkStack trailLim (ls lvl)
setInt qHead =<< sizeOfStack trail
instance VarOrder Solver where
newVar _ = return 0
update = increaseHeap
undo s v = inHeap s v >>= (`unless` insertHeap s v)
select s = do
let
asg = assigns s
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
varBumpActivity :: Solver -> Var -> IO ()
varBumpActivity s@Solver{..} !x = do
!a <- (+) <$> getNthDouble x activities <*> getDouble varInc
if 1e100 < a
then varRescaleActivity s
else setNthDouble x activities a
update s x
varDecayActivity :: Solver -> IO ()
varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config)
varRescaleActivity :: Solver -> IO ()
varRescaleActivity Solver{..} = do
forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (* 1e-100)
modifyDouble varInc (* 1e-100)
claBumpActivity :: Solver -> Clause -> IO ()
claBumpActivity s@Solver{..} Clause{..} = do
a <- (+) <$> getDouble activity <*> getDouble claInc
if 1e100 < a
then claRescaleActivity s
else setDouble activity a
claDecayActivity :: Solver -> IO ()
claDecayActivity Solver{..} = modifyDouble claInc (/ clauseDecayRate config)
claRescaleActivity :: Solver -> IO ()
claRescaleActivity Solver{..} = do
vec <- getClauseVector learnts
n <- numberOfClauses learnts
let
loopOnVector :: Int -> IO ()
loopOnVector ((< n) -> False) = return ()
loopOnVector i = do
c <- getNthClause vec i
modifyDouble (activity c) (* 1e-20)
loopOnVector $ i + 1
loopOnVector 0
modifyDouble claInc (* 1e-20)
data VarHeap = VarHeap
{
heap :: Vec
, idxs :: Vec
}
newVarHeap :: Int -> IO VarHeap
newVarHeap n = VarHeap <$> newSizedVecIntFromList lst <*> newSizedVecIntFromList lst
where
lst = [1 .. n]
numElementsInHeap :: Solver -> IO Int
numElementsInHeap (order -> heap -> h) = getNth h 0
inHeap :: Solver -> Var -> IO Bool
inHeap (order -> idxs -> at) n = (/= 0) <$> getNth at n
increaseHeap :: Solver -> Int -> IO ()
increaseHeap s@(order -> idxs -> at) n = inHeap s n >>= (`when` (percolateUp s =<< getNth at n))
percolateUp :: Solver -> Int -> IO ()
percolateUp Solver{..} start = do
let VarHeap to at = order
v <- getNth to start
ac <- getNthDouble v activities
let
loop :: Int -> IO ()
loop i = do
let iP = div i 2
if iP == 0
then setNth to i v >> setNth at v i
else do
v' <- getNth to iP
acP <- getNthDouble v' activities
if ac > acP
then setNth to i v' >> setNth at v' i >> loop iP
else setNth to i v >> setNth at v i
loop start
percolateDown :: Solver -> Int -> IO ()
percolateDown Solver{..} start = do
let (VarHeap to at) = order
n <- getNth to 0
v <- getNth to start
ac <- getNthDouble v activities
let
loop :: Int -> IO ()
loop i = do
let iL = 2 * i
if iL <= n
then do
let iR = iL + 1
l <- getNth to iL
r <- getNth to iR
acL <- getNthDouble l activities
acR <- getNthDouble r activities
let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL)
if ac' > ac
then setNth to i child >> setNth at child i >> loop ci
else setNth to i v >> setNth at v i
else setNth to i v >> setNth at v i
loop start
insertHeap :: Solver -> Var -> IO ()
insertHeap s@(order -> VarHeap to at) v = do
n <- (1 +) <$> getNth to 0
setNth at v n
setNth to n v
setNth to 0 n
percolateUp s n
getHeapRoot :: Solver -> IO Int
getHeapRoot s@(order -> VarHeap to at) = do
r <- getNth to 1
l <- getNth to =<< getNth to 0
setNth to 1 l
setNth at l 1
setNth at r 0
modifyNth to (subtract 1) 0
n <- getNth to 0
when (1 < n) $ percolateDown s 1
return r