module SAT.Mios.Solver
(
Solver (..)
, newSolver
, nAssigns
, nClauses
, nLearnts
, decisionLevel
, valueVar
, valueLit
, locked
, setAssign
, enqueue
, assume
, cancelUntil
, StatIndex (..)
, getStat
, setStat
, incrementStat
, getStats
, dumpSolver
)
where
import Control.Monad (unless, when)
import Data.List (intercalate)
import Numeric (showFFloat)
import SAT.Mios.Types
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
import SAT.Mios.ClausePool
data Solver = Solver
{
clauses :: !ClauseExtManager
, learnts :: !ClauseExtManager
, watches :: !WatcherList
, assigns :: !(Vec Int)
, phases :: !(Vec Int)
, trail :: !Stack
, trailLim :: !Stack
, qHead :: !Int'
, reason :: !ClauseVector
, level :: !(Vec Int)
, conflicts :: !Stack
, activities :: !(Vec Double)
, order :: !VarHeap
, config :: !MiosConfiguration
, nVars :: !Int
, claInc :: !Double'
, varInc :: !Double'
, rootLevel :: !Int'
, learntSAdj :: Double'
, learntSCnt :: Int'
, maxLearnts :: Double'
, ok :: !Int'
, an'seen :: !(Vec Int)
, an'toClear :: !Stack
, an'stack :: !Stack
, an'lastDL :: !Stack
, clsPool :: ClausePool
, litsLearnt :: !Stack
, stats :: !(Vec [Int])
, lbd'seen :: !(Vec Int)
, lbd'key :: !Int'
, emaDFast :: !Double'
, emaDSlow :: !Double'
, emaAFast :: !Double'
, emaASlow :: !Double'
, nextRestart :: !Int'
, restartMode :: Int'
}
newSolver :: MiosConfiguration -> CNFDescription -> IO Solver
newSolver conf (CNFDescription nv dummy_nc _) =
Solver
<$> newManager dummy_nc
<*> newManager 2000
<*> newWatcherList nv 2
<*> newVec nv LBottom
<*> newVec nv LBottom
<*> newStack nv
<*> newStack nv
<*> new' 0
<*> newClauseVector (nv + 1)
<*> newVec nv (1)
<*> newStack nv
<*> newVec nv 0
<*> newVarHeap nv
<*> return conf
<*> return nv
<*> new' 1.0
<*> new' 1.0
<*> new' 0
<*> new' 100
<*> new' 100
<*> new' 2000
<*> new' LiftedT
<*> newVec nv 0
<*> newStack nv
<*> newStack nv
<*> newStack nv
<*> newClausePool 10
<*> newStack nv
<*> newVec (fromEnum EndOfStatIndex) 0
<*> newVec nv 0
<*> new' 0
<*> new' 0.0
<*> new' 0.0
<*> new' 0.0
<*> new' 0.0
<*> new' 100
<*> new' 1
nAssigns :: Solver -> IO Int
nAssigns = get' . trail
nClauses :: Solver -> IO Int
nClauses = get' . clauses
nLearnts :: Solver -> IO Int
nLearnts = get' . learnts
decisionLevel :: Solver -> IO Int
decisionLevel = get' . 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 ==) <$> (getNth (reason s) . lit2var =<< getNth (lits c) 1)
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]
setAssign :: Solver -> Int -> LiftedBool -> IO ()
setAssign Solver{..} v x = setNth assigns v x
enqueue :: Solver -> Lit -> Clause -> IO Bool
enqueue s@Solver{..} p from = do
let signumP = lit2lbool p
let v = lit2var p
val <- valueVar s v
if val /= LBottom
then return $ val == signumP
else do setNth assigns v signumP
setNth level v =<< decisionLevel s
setNth reason v from
pushTo trail p
return True
assume :: Solver -> Lit -> IO Bool
assume s p = do
pushTo (trailLim s) =<< get' (trail s)
enqueue s p NullClause
cancelUntil :: Solver -> Int -> IO ()
cancelUntil s@Solver{..} lvl = do
dl <- decisionLevel s
when (lvl < dl) $ do
lim <- getNth trailLim (lvl + 1)
ts <- get' trail
ls <- get' trailLim
let
loopOnTrail :: Int -> IO ()
loopOnTrail ((lim <) -> False) = return ()
loopOnTrail c = do
x <- lit2var <$> getNth trail c
setNth phases x =<< getNth assigns x
setNth assigns x LBottom
setNth reason x NullClause
undo s x
loopOnTrail $ c 1
loopOnTrail ts
shrinkBy trail (ts lim)
shrinkBy trailLim (ls lvl)
set' qHead =<< get' trail
instance VarOrder Solver where
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
data VarHeap = VarHeap
{
heap :: !Stack
, idxs :: !Stack
}
newVarHeap :: Int -> IO VarHeap
newVarHeap n = do
v1 <- newVec n 0
v2 <- newVec n 0
let
loop :: Int -> IO ()
loop ((<= n) -> False) = set' v1 n >> set' v2 n
loop i = setNth v1 i i >> setNth v2 i i >> loop (i + 1)
loop 1
return $ VarHeap v1 v2
numElementsInHeap :: Solver -> IO Int
numElementsInHeap = get' . heap . order
inHeap :: Solver -> Var -> IO Bool
inHeap Solver{..} n = case idxs order of at -> (/= 0) <$> getNth at n
increaseHeap :: Solver -> Int -> IO ()
increaseHeap s@Solver{..} n = case idxs order of
at -> 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 <- getNth activities v
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 <- getNth activities v'
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 <- getNth activities v
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 <- getNth activities l
acR <- getNth activities r
let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL)
if ac' > ac
then setNth to i child >> setNth at child i >> loop ci
else setNth to i v >> setNth at v i
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
set' to 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
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
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
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
dumpSolver DumpJSON _ = return ()