module SAT.Mios.Solver
(
Solver (..)
, newSolver
, nAssigns
, nClauses
, nLearnts
, decisionLevel
, valueVar
, valueLit
, locked
, addClause
, enqueue
, assume
, cancelUntil
, getModel
, claBumpActivity
, claRescaleActivityAfterRestart
, varBumpActivity
, varDecayActivity
, claActivityThreshold
, StatIndex (..)
, getStat
, setStat
, incrementStat
, getStats
)
where
import Control.Monad ((<=<), forM_, unless, when)
import SAT.Mios.Types
import SAT.Mios.Internal
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
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
, varInc :: !DoubleSingleton
, rootLevel :: !IntSingleton
, ok :: !BoolSingleton
, an'seen :: !Vec
, an'toClear :: !Stack
, an'stack :: !Stack
, pr'seen :: !Vec
, 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
<*> newInt 0
<*> newBool True
<*> newVec (nv + 1)
<*> newStack nv
<*> newStack nv
<*> newVecWith (nv + 1) (1)
<*> 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 = sizeOfStack . trailLim
valueVar :: Solver -> Var -> IO Int
valueVar = getNth . assigns
valueLit :: Solver -> Lit -> IO Int
valueLit (assigns -> a) !p = (\x -> if positiveLit p then x else negate x) <$> getNth a (lit2var p)
locked :: Solver -> Clause -> IO Bool
locked s c = (c ==) <$> (getNthClause (reason s) . lit2var =<< getNth (lits c) 1)
data StatIndex =
NumOfBackjump
| NumOfRestart
deriving (Bounded, Enum, Eq, Ord, Read, Show)
getStat :: Solver -> StatIndex -> IO Int
getStat (stats -> v) (fromEnum -> i) = getNth v i
setStat :: Solver -> StatIndex -> Int -> IO ()
setStat (stats -> v) (fromEnum -> i) x = setNth v i x
incrementStat :: Solver -> StatIndex -> Int -> IO ()
incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i
getStats :: Solver -> IO [(StatIndex, Int)]
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 p = do
pushToStack (trailLim s) =<< sizeOfStack (trail s)
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
varActivityThreshold :: Double
varActivityThreshold = 1e100
claActivityThreshold :: Double
claActivityThreshold = 1e20
varBumpActivity :: Solver -> Var -> IO ()
varBumpActivity s@Solver{..} x = do
!a <- (+) <$> getNthDouble x activities <*> getDouble varInc
setNthDouble x activities a
when (varActivityThreshold < a) $ varRescaleActivity s
update s x
varDecayActivity :: Solver -> IO ()
varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config)
varRescaleActivity :: Solver -> IO ()
varRescaleActivity Solver{..} = do
forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (/ varActivityThreshold)
modifyDouble varInc (/ varActivityThreshold)
claBumpActivity :: Solver -> Clause -> IO ()
claBumpActivity s Clause{..} = do
dl <- decisionLevel s
a <- (fromIntegral dl +) <$> getDouble activity
setDouble activity a
when (claActivityThreshold <= a) $ claRescaleActivity s
claRescaleActivity :: Solver -> IO ()
claRescaleActivity Solver{..} = do
vec <- getClauseVector learnts
n <- numberOfClauses learnts
let
loopOnVector :: Int -> IO ()
loopOnVector ((< n) -> False) = return ()
loopOnVector i = do
c <- getNthClause vec i
modifyDouble (activity c) (/ claActivityThreshold)
loopOnVector $ i + 1
loopOnVector 0
claRescaleActivityAfterRestart :: Solver -> IO ()
claRescaleActivityAfterRestart Solver{..} = do
vec <- getClauseVector learnts
n <- numberOfClauses learnts
let
loopOnVector :: Int -> IO ()
loopOnVector ((< n) -> False) = return ()
loopOnVector i = do
c <- getNthClause vec i
d <- sizeOfClause c
if d < 9
then modifyDouble (activity c) sqrt
else setDouble (activity c) 0
setBool (protected c) False
loopOnVector $ i + 1
loopOnVector 0
data VarHeap = VarHeap
{
heap :: Vec
, idxs :: Vec
}
newVarHeap :: Int -> IO VarHeap
newVarHeap n = do
v1 <- newVec (n + 1)
v2 <- newVec (n + 1)
let
loop :: Int -> IO ()
loop ((<= n) -> False) = setNth v1 0 n >> setNth v2 0 n
loop i = setNth v1 i i >> setNth v2 i i >> loop (i + 1)
loop 1
return $ VarHeap v1 v2
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