module SAT.Mios.Main
(
Solver
, newSolver
, setAssign
, addClause
, dumpSolver
, simplifyDB
, solve
)
where
import Control.Monad (unless, void, when)
import Data.Bits
import Data.Foldable (foldrM)
import Data.Int
import SAT.Mios.Types
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
import SAT.Mios.Solver
import SAT.Mios.ClausePool
import SAT.Mios.Criteria
removeWatch :: Solver -> Clause -> IO ()
removeWatch Solver{..} c = do
let lstack = lits c
l1 <- negateLit <$> getNth lstack 1
markClause (getNthWatcher watches l1) c
l2 <- negateLit <$> getNth lstack 2
markClause (getNthWatcher watches l2) c
putBackToPool clsPool c
newLearntClause :: Solver -> Stack -> IO Int
newLearntClause s@Solver{..} ps = do
k <- get' ps
case k of
1 -> do l <- getNth ps 1
unsafeEnqueue s l NullClause
return 1
_ -> do c <- makeClauseFromStack clsPool ps
let lstack = lits c
findMax :: Int -> Int -> Int -> IO Int
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
claBumpActivity s c
pushTo learnts c
l1 <- getNth lstack 1
l2 <- getNth lstack 2
pushClauseWithKey (getNthWatcher watches (negateLit l1)) c l2
pushClauseWithKey (getNthWatcher watches (negateLit l2)) c l1
unsafeEnqueue s l1 c
lbd <- lbdOf s (lits c)
set' (rank c) lbd
return lbd
simplify :: Solver -> Clause -> IO Bool
simplify s c = do
n <- get' c
let lstack = lits c
loop ::Int -> IO Bool
loop ((<= n) -> False) = return False
loop i = do v <- valueLit s =<< getNth lstack i
if v == 1 then return True else loop (i + 1)
loop 1
analyze :: Solver -> Clause -> IO Int
analyze s@Solver{..} confl = do
reset litsLearnt
pushTo litsLearnt 0
dl <- decisionLevel s
let loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int
loopOnClauseChain c p ti bl pathC = do
d <- get' (rank c)
when (0 /= d) $ claBumpActivity s c
when (2 < d) $ do
nblevels <- lbdOf s (lits c)
when (nblevels + 1 < d) $
set' (rank c) nblevels
sc <- get' c
let lstack = lits c
loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int)
loopOnLiterals ((<= sc) -> False) b pc = return (b, pc)
loopOnLiterals j b pc = do
(q :: Lit) <- getNth lstack j
let v = lit2var q
sn <- getNth an'seen v
l <- getNth level v
if sn == 0 && 0 < l
then do
varBumpActivity s v
setNth an'seen v 1
if dl <= l
then do
r <- getNth reason v
when (r /= NullClause) $ do
ra <- get' (rank r)
when (0 /= ra) $ pushTo an'lastDL q
loopOnLiterals (j + 1) b (pc + 1)
else pushTo litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc
else loopOnLiterals (j + 1) b pc
(b', pathC') <- loopOnLiterals (if p == bottomLit then 1 else 2) bl pathC
let nextPickedUpLit :: Int -> IO Int
nextPickedUpLit i = do x <- getNth an'seen . lit2var =<< getNth trail i
if x == 0 then nextPickedUpLit (i 1) else return (i 1)
ti' <- nextPickedUpLit (ti + 1)
nextP <- getNth trail (ti' + 1)
let nextV = lit2var nextP
confl' <- getNth reason nextV
setNth an'seen nextV 0
if 1 < pathC'
then loopOnClauseChain confl' nextP (ti' 1) b' (pathC' 1)
else setNth litsLearnt 1 (negateLit nextP) >> return b'
ti <- subtract 1 <$> get' trail
levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0
n <- get' litsLearnt
reset an'stack
reset an'toClear
pushTo an'toClear =<< getNth litsLearnt 1
let merger :: Int -> Int64 -> IO Int64
merger ((<= n) -> False) b = return b
merger i b = do l <- getNth litsLearnt i
pushTo an'toClear l
merger (i + 1) . setBit b . (63 .&.) =<< getNth level (lit2var l)
levels <- merger 2 0
let loopOnLits :: Int -> Int -> IO ()
loopOnLits ((<= n) -> False) n' = shrinkBy litsLearnt $ n n' + 1
loopOnLits i j = do
l <- getNth litsLearnt i
c1 <- (NullClause ==) <$> getNth reason (lit2var l)
if c1
then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1)
else do
c2 <- not <$> analyzeRemovable s l levels
if c2
then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1)
else loopOnLits (i + 1) j
loopOnLits 2 2
nld <- get' an'lastDL
r <- get' litsLearnt
let loopOnLastDL :: Int -> IO ()
loopOnLastDL ((<= nld) -> False) = return ()
loopOnLastDL i = do v <- lit2var <$> getNth an'lastDL i
r' <- get' =<< getNth reason v
when (r < r') $ varBumpActivity s v
loopOnLastDL $ i + 1
loopOnLastDL 1
reset an'lastDL
k <- get' an'toClear
let cleaner :: Int -> IO ()
cleaner ((<= k) -> False) = return ()
cleaner i = do v <- lit2var <$> getNth an'toClear i
setNth an'seen v 0
cleaner $ i + 1
cleaner 1
return levelToReturn
analyzeRemovable :: Solver -> Lit -> Int64 -> IO Bool
analyzeRemovable Solver{..} p minLevel = do
reset an'stack
pushTo an'stack p
top <- get' an'toClear
let
loopOnStack :: IO Bool
loopOnStack = do
k <- get' an'stack
if 0 == k
then return True
else do
sl <- lastOf an'stack
popFrom an'stack
c <- getNth reason (lit2var sl)
nl <- get' c
let
lstack = lits c
loopOnLit :: Int -> IO Bool
loopOnLit ((<= nl) -> False) = loopOnStack
loopOnLit i = do
p' <- getNth lstack i
let v' = lit2var p'
l' <- getNth level v'
c1 <- (1 /=) <$> getNth an'seen v'
if c1 && (0 /= l')
then do
c3 <- (NullClause /=) <$> getNth reason v'
if c3 && testBit minLevel (l' .&. 63)
then do
setNth an'seen v' 1
pushTo an'stack p'
pushTo an'toClear p'
loopOnLit $ i + 1
else do
top' <- get' an'toClear
let clearAll :: Int -> IO ()
clearAll ((<= top') -> False) = return ()
clearAll j = do x <- getNth an'toClear j; setNth an'seen (lit2var x) 0; clearAll (j + 1)
clearAll $ top + 1
shrinkBy an'toClear $ top' top
return False
else loopOnLit $ i + 1
loopOnLit 2
loopOnStack
analyzeFinal :: Solver -> Clause -> Bool -> IO ()
analyzeFinal Solver{..} confl skipFirst = do
reset conflicts
rl <- get' rootLevel
unless (rl == 0) $ do
n <- get' confl
let lstack = lits confl
loopOnConfl :: Int -> IO ()
loopOnConfl ((<= n) -> False) = return ()
loopOnConfl i = do
(x :: Var) <- lit2var <$> getNth lstack i
lvl <- getNth level x
when (0 < lvl) $ setNth an'seen x 1
loopOnConfl $ i + 1
loopOnConfl $ if skipFirst then 2 else 1
tls <- get' trailLim
trs <- get' trail
tlz <- getNth trailLim 1
let loopOnTrail :: Int -> IO ()
loopOnTrail ((tlz <=) -> False) = return ()
loopOnTrail i = do
(l :: Lit) <- getNth trail (i + 1)
let (x :: Var) = lit2var l
saw <- getNth an'seen x
when (saw == 1) $ do
(r :: Clause) <- getNth reason x
if r == NullClause
then pushTo conflicts (negateLit l)
else do
k <- get' r
let lstack' = lits r
loopOnLits :: Int -> IO ()
loopOnLits ((<= k) -> False) = return ()
loopOnLits j = do
(v :: Var) <- lit2var <$> getNth lstack' j
lv <- getNth level v
when (0 < lv) $ setNth an'seen v 1
loopOnLits $ i + 1
loopOnLits 2
setNth an'seen x 0
loopOnTrail $ i 1
loopOnTrail =<< if tls <= rl then return (trs 1) else getNth trailLim (rl + 1)
propagate :: Solver -> IO Clause
propagate s@Solver{..} = do
let
while :: Clause -> Bool -> IO Clause
while confl False = return confl
while confl True = do
(p :: Lit) <- getNth trail . (1 +) =<< get' qHead
modify' qHead (+ 1)
incrementStat s NumOfPropagation 1
let (ws :: ClauseExtManager) = getNthWatcher watches p
!falseLit = negateLit p
end <- get' ws
cvec <- getClauseVector ws
bvec <- getKeyVector ws
let copy :: Int -> Int -> IO ()
copy ((< end) -> False) _ = return ()
copy !i' !j' = do setNth cvec j' =<< getNth cvec i'
setNth bvec j' =<< getNth bvec i'
copy (i' + 1) (j' + 1)
let forClause :: Int -> Int -> IO Clause
forClause i@((< end) -> False) !j = shrinkBy ws (i j) >> return confl
forClause !i !j = do
(blocker :: Lit) <- getNth bvec i
bv <- if blocker == 0 then return LiftedF else valueLit s blocker
if bv == LiftedT
then do unless (i == j) $ do (c :: Clause) <- getNth cvec i
setNth cvec j c
setNth bvec j blocker
forClause (i + 1) (j + 1)
else do
(c :: Clause) <- getNth cvec i
let !lstack = lits c
tmp <- getNth lstack 1
first <- if falseLit == tmp
then do l2 <- getNth lstack 2
setNth lstack 2 tmp
setNth lstack 1 l2
return l2
else return tmp
fv <- valueLit s first
if fv == LiftedT
then do unless (i == j) $ setNth cvec j c
setNth bvec j first
forClause (i + 1) (j + 1)
else do cs <- get' c
let newWatch :: Int -> IO LiftedBool
newWatch ((<= cs) -> False) = do
setNth cvec j c
setNth bvec j first
if fv == LiftedF
then do ((== 0) <$> decisionLevel s) >>= (`when` set' ok LiftedF)
set' qHead =<< get' trail
copy (i + 1) (j + 1)
return LiftedF
else do unsafeEnqueue s first c
return LBottom
newWatch !k = do (l' :: Lit) <- getNth lstack k
lv <- valueLit s l'
if lv /= LiftedF
then do setNth lstack 2 l'
setNth lstack k falseLit
pushClauseWithKey (getNthWatcher watches (negateLit l')) c first
return LiftedT
else newWatch $! k + 1
ret <- newWatch 3
case ret of
LiftedT -> forClause (i + 1) j
LBottom -> forClause (i + 1) (j + 1)
_ -> shrinkBy ws (i j) >> return c
c <- forClause 0 0
while c =<< ((<) <$> get' qHead <*> get' trail)
while NullClause =<< ((<) <$> get' qHead <*> get' trail)
reduceDB :: Solver -> IO ()
reduceDB s@Solver{..} = do
n <- nLearnts s
cvec <- getClauseVector learnts
let loop :: Int -> IO ()
loop ((< n) -> False) = return ()
loop i = do
removeWatch s =<< getNth cvec i
loop $ i + 1
k <- sortClauses s learnts $ div n 2
loop k
reset watches
shrinkBy learnts (n k)
incrementStat s NumOfReduction 1
rankWidth :: Int
rankWidth = 10
activityWidth :: Int
activityWidth = 50
indexWidth :: Int
indexWidth = 32
rankMax :: Int
rankMax = 2 ^ rankWidth 1
activityMax :: Int
activityMax = 2 ^ activityWidth 1
indexMax :: Int
indexMax = 2 ^ indexWidth 1
sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int
sortClauses s cm limit' = do
n <- get' cm
vec <- getClauseVector cm
bvec <- getKeyVector cm
keys <- newVec (2 * n) 0 :: IO (Vec Int)
at <- (0.1 *) . (/ fromIntegral n) <$> get' (claInc s)
let shiftLBD = activityWidth
shiftIndex = shiftL 1 indexWidth
am = fromIntegral activityMax :: Double
scaleAct :: Double -> Int
scaleAct x
| x < 1e-20 = activityMax
| otherwise = floor $ am * (1 logBase 10 (x * 1e20) / 40)
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
then do setNth keys (2 * i) 0
assignKey (i + 1) (t + 1)
else do a <- get' (activity c)
r <- get' (rank c)
l <- locked s c
let d =if | l -> 0
| a < at -> rankMax
| otherwise -> min rankMax r
setNth keys (2 * i) $ shiftL d shiftLBD + scaleAct a
assignKey (i + 1) $ if l then t + 1 else t
limit <- max limit' <$> assignKey 0 0
let limit2 = 2 * limit
sortOnRange :: Int -> Int -> IO ()
sortOnRange left right
| limit2 < 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)
| otherwise = do
let p = 2 * div (left + right) 4
pivot <- getNth keys p
swapBetween keys p left
swapBetween keys (p + 1) (left + 1)
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
nextR :: Int -> IO Int
nextR i = do v <- getNth keys i; if pivot < v then nextR (i 2) 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)
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)
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
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
seek $ i + 1
seek 0
return limit
simplifyDB :: Solver -> IO Bool
simplifyDB s@Solver{..} = do
good <- (LiftedT ==) <$> get' ok
if good
then do
p <- propagate s
if p /= NullClause
then set' ok LiftedF >> return False
else do
let
for :: ClauseExtManager -> IO ()
for mgr = do
vec' <- getClauseVector mgr
n' <- get' mgr
let
loopOnVector :: Int -> Int -> IO ()
loopOnVector ((< n') -> False) j = shrinkBy mgr (n' j)
loopOnVector i j = do
c <- getNth vec' i
l <- locked s c
r <- if l then return False else simplify s c
if r
then removeWatch s c >> loopOnVector (i + 1) j
else unless (i == j) (setNth vec' j c) >> loopOnVector (i + 1) (j + 1)
loopOnVector 0 0
for clauses
for learnts
reset watches
return True
else return False
search :: Solver -> IO Bool
search s@Solver{..} = do
let loop :: Bool -> IO Bool
loop restart = do
confl <- propagate s
d <- decisionLevel s
if confl /= NullClause
then do incrementStat s NumOfBackjump 1
r <- get' rootLevel
if d == r
then analyzeFinal s confl False >> return False
else do backtrackLevel <- analyze s confl
(s `cancelUntil`) . max backtrackLevel =<< get' rootLevel
lbd' <- newLearntClause s litsLearnt
k <- get' litsLearnt
when (k == 1) $ do
(v :: Var) <- lit2var <$> getNth litsLearnt 1
setNth level v 0
varDecayActivity s
claDecayActivity s
modify' learntSCnt (subtract 1)
cnt <- get' learntSCnt
when (cnt == 0) $ do
t' <- (* 1.5) <$> get' learntSAdj
set' learntSAdj t'
set' learntSCnt $ floor t'
modify' maxLearnts (+ 300)
loop =<< checkRestartCondition s lbd'
else do when (d == 0) . void $ simplifyDB s
k1 <- get' learnts
k2 <- nAssigns s
nl <- floor <$> get' maxLearnts
when (nl < k1 k2) $ do
reduceDB s
when (2 == dumpStat config) $ dumpSolver DumpCSV s
if | k2 == nVars -> return True
| restart -> do
(s `cancelUntil`) =<< get' rootLevel
loop False
| otherwise -> do
v <- select s
oldVal <- getNth phases v
unsafeAssume s $ var2lit v (0 < oldVal)
loop False
loop False
solve :: (Foldable t) => Solver -> t Lit -> IO SolverResult
solve s@Solver{..} assumps = do
let inject :: Lit -> Bool -> IO Bool
inject _ False = return False
inject a True = do
b <- assume s a
if not b
then do (confl :: Clause) <- getNth reason (lit2var a)
analyzeFinal s confl True
pushTo conflicts (negateLit a)
cancelUntil s 0
return False
else do confl <- propagate s
if confl /= NullClause
then do analyzeFinal s confl True
cancelUntil s 0
return False
else return True
good <- simplifyDB s
x <- if good then foldrM inject True assumps else return False
if x
then do set' rootLevel =<< decisionLevel s
status <- search s
let toInt :: Var -> IO Lit
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
cancelUntil s 0
flag <- get' ok
if | status && flag == LiftedT -> return $ Right (SAT asg1)
| not status && flag == LiftedF -> return $ Right (UNSAT asg2)
| otherwise -> return $ Left InternalInconsistent
else return $ Right (UNSAT [])
unsafeEnqueue :: Solver -> Lit -> Clause -> IO ()
unsafeEnqueue s@Solver{..} p from = do
let v = lit2var p
setNth assigns v $ lit2lbool p
setNth level v =<< decisionLevel s
setNth reason v from
pushTo trail p
unsafeAssume :: Solver -> Lit -> IO ()
unsafeAssume s@Solver{..} p = do
pushTo trailLim =<< get' trail
unsafeEnqueue s p NullClause