module SAT.Mios.Main
(
simplifyDB
, solve
)
where
import Control.Monad (unless, void, when)
import Data.Bits
import Data.Foldable (foldrM)
import SAT.Mios.Types
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
import SAT.Mios.Solver
rankOf :: Clause -> IO Int
rankOf = get'
removeWatch :: Solver -> Clause -> IO ()
removeWatch (watches -> w) c = do
let lvec = asUVector c
l1 <- negateLit <$> getNth lvec 0
markClause (getNthWatcher w l1) c
l2 <- negateLit <$> getNth lvec 1
markClause (getNthWatcher w l2) c
newLearntClause :: Solver -> Stack -> IO ()
newLearntClause s@Solver{..} ps = do
good <- get' ok
when good $ do
k <- get' ps
case k of
1 -> do
l <- getNth ps 1
unsafeEnqueue s l NullClause
_ -> do
c <- newClauseFromStack True ps
let vec = asUVector c
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
swapBetween vec 1 =<< findMax 0 0 0
set' (activity c) . fromIntegral =<< decisionLevel s
pushTo learnts c
l <- getNth vec 0
pushClauseWithKey (getNthWatcher watches (negateLit l)) c 0
l1 <- negateLit <$> getNth vec 1
pushClauseWithKey (getNthWatcher watches l1) c 0
unsafeEnqueue s l c
set' (protected c) True
simplify :: Solver -> Clause -> IO Bool
simplify s c = do
n <- get' c
let
lvec = asUVector c
loop ::Int -> IO Bool
loop ((< n) -> False) = return False
loop i = do
v <- valueLit s =<< getNth lvec i
if v == 1 then return True else loop (i + 1)
loop 0
analyze :: Solver -> Clause -> IO Int
analyze s@Solver{..} confl = do
reset litsLearnt
pushTo litsLearnt 0
dl <- decisionLevel s
let
litsVec = asUVector litsLearnt
trailVec = asUVector trail
loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int
loopOnClauseChain c p ti bl pathC = do
when (learnt c) $ do
claBumpActivity s c
sc <- get' c
let
lvec = asUVector c
loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int)
loopOnLiterals ((< sc) -> False) b pc = return (b, pc)
loopOnLiterals j b pc = do
(q :: Lit) <- getNth lvec 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 && learnt r) $ 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 0 else 1) bl pathC
let
nextPickedUpLit :: Int -> IO Int
nextPickedUpLit i = do
x <- getNth an'seen . lit2var =<< getNth trailVec i
if x == 0 then nextPickedUpLit $ i 1 else return i
ti' <- nextPickedUpLit ti
nextP <- getNth trailVec ti'
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 litsVec 0 (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 litsVec 0
let
merger :: Int -> Int -> IO Int
merger ((< n) -> False) b = return b
merger i b = do
l <- getNth litsVec i
pushTo an'toClear l
merger (i + 1) . setBit b . (31 .&.) =<< getNth level (lit2var l)
levels <- merger 1 0
let
loopOnLits :: Int -> Int -> IO ()
loopOnLits ((< n) -> False) n' = shrinkBy litsLearnt $ n n'
loopOnLits i j = do
l <- getNth litsVec i
c1 <- (NullClause ==) <$> getNth reason (lit2var l)
if c1
then setNth litsVec j l >> loopOnLits (i + 1) (j + 1)
else do
c2 <- not <$> analyzeRemovable s l levels
if c2
then setNth litsVec j l >> loopOnLits (i + 1) (j + 1)
else loopOnLits (i + 1) j
loopOnLits 1 1
nld <- get' an'lastDL
r <- get' litsLearnt
let
vec = asUVector an'lastDL
loopOnLastDL :: Int -> IO ()
loopOnLastDL ((< nld) -> False) = return ()
loopOnLastDL i = do
v <- lit2var <$> getNth vec i
r' <- rankOf =<< getNth reason v
when (r < r') $ varBumpActivity s v
loopOnLastDL $ i + 1
loopOnLastDL 0
reset an'lastDL
k <- get' an'toClear
let
vec' = asUVector an'toClear
cleaner :: Int -> IO ()
cleaner ((< k) -> False) = return ()
cleaner i = do
v <- lit2var <$> getNth vec' i
setNth an'seen v 0
cleaner $ i + 1
cleaner 0
return levelToReturn
analyzeRemovable :: Solver -> Lit -> Int -> 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
cvec = asUVector c
loopOnLit :: Int -> IO Bool
loopOnLit ((< nl) -> False) = loopOnStack
loopOnLit i = do
p' <- getNth cvec 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' .&. 31)
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
vec = asUVector an'toClear
clearAll :: Int -> IO ()
clearAll ((< top') -> False) = return ()
clearAll j = do x <- getNth vec j; setNth an'seen (lit2var x) 0; clearAll (j + 1)
clearAll top
shrinkBy an'toClear $ top' top
return False
else loopOnLit $ i + 1
loopOnLit 1
loopOnStack
analyzeFinal :: Solver -> Clause -> Bool -> IO ()
analyzeFinal Solver{..} confl skipFirst = do
reset conflicts
rl <- get' rootLevel
unless (rl == 0) $ do
n <- get' confl
let
lvec = asUVector confl
loopOnConfl :: Int -> IO ()
loopOnConfl ((< n) -> False) = return ()
loopOnConfl i = do
(x :: Var) <- lit2var <$> getNth lvec i
lvl <- getNth level x
when (0 < lvl) $ setNth an'seen x 1
loopOnConfl $ i + 1
loopOnConfl $ if skipFirst then 1 else 0
tls <- get' trailLim
trs <- get' trail
tlz <- getNth (asUVector trailLim) 0
let
trailVec = asUVector trail
loopOnTrail :: Int -> IO ()
loopOnTrail ((tlz <=) -> False) = return ()
loopOnTrail i = do
(l :: Lit) <- getNth trailVec i
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
cvec = asUVector r
loopOnLits :: Int -> IO ()
loopOnLits ((< k) -> False) = return ()
loopOnLits j = do
(v :: Var) <- lit2var <$> getNth cvec j
lv <- getNth level v
when (0 < lv) $ setNth an'seen v 1
loopOnLits $ i + 1
loopOnLits 1
setNth an'seen x 0
loopOnTrail $ i 1
loopOnTrail =<< if tls <= rl then return (trs 1) else getNth (asUVector trailLim) rl
propagate :: Solver -> IO Clause
propagate s@Solver{..} = do
let
trailVec = asUVector trail
while :: Clause -> Bool -> IO Clause
while confl False = return confl
while confl True = do
(p :: Lit) <- getNth trailVec =<< get' qHead
modify' qHead (+ 1)
let (ws :: ClauseExtManager) = getNthWatcher watches p
end <- get' ws
cvec <- getClauseVector ws
bvec <- getKeyVector ws
let
forClause :: Clause -> Int -> Int -> IO Clause
forClause confl i@((< end) -> False) j = do
shrinkBy ws (i j)
while confl =<< ((<) <$> get' qHead <*> get' trail)
forClause confl i j = do
(l :: Lit) <- getNth bvec i
bv <- if l == 0 then return lFalse else valueLit s l
if bv == lTrue
then do
unless (i == j) $ do
(c :: Clause) <- getNth cvec i
setNth cvec j c
setNth bvec j l
forClause confl (i + 1) (j + 1)
else do
(c :: Clause) <- getNth cvec i
let
lits = asUVector c
falseLit = negateLit p
((falseLit ==) <$> getNth lits 0) >>= (`when` swapBetween lits 0 1)
(first :: Lit) <- getNth lits 0
val <- valueLit s first
if val == lTrue
then setNth cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1)
else do
cs <- get' c
let
forLit :: Int -> IO Clause
forLit ((< cs) -> False) = do
setNth cvec j c
setNth bvec j 0
result <- enqueue s first c
if not result
then do
((== 0) <$> decisionLevel s) >>= (`when` set' ok False)
set' qHead =<< get' trail
let
copy i'@((< end) -> False) j' = forClause c i' j'
copy i' j' = do
setNth cvec j' =<< getNth cvec i'
setNth bvec j' =<< getNth bvec i'
copy (i' + 1) (j' + 1)
copy (i + 1) (j + 1)
else forClause confl (i + 1) (j + 1)
forLit k = do
(l :: Lit) <- getNth lits k
lv <- valueLit s l
if lv /= lFalse
then do
swapBetween lits 1 k
pushClauseWithKey (getNthWatcher watches (negateLit l)) c l
forClause confl (i + 1) j
else forLit $ k + 1
forLit 2
forClause confl 0 0
while NullClause =<< ((<) <$> get' qHead <*> get' trail)
reduceDB :: Solver -> IO ()
reduceDB s@Solver{..} = do
n <- nLearnts s
vec <- getClauseVector learnts
let
loop :: Int -> IO ()
loop ((< n) -> False) = return ()
loop i = (removeWatch s =<< getNth vec i) >> loop (i + 1)
k <- sortClauses s learnts (div n 2)
loop k
reset watches
shrinkBy learnts (n k)
(rankWidth :: Int, activityWidth :: Int, indexWidth :: Int) = (l, a, w (l + a + 1))
where
w = finiteBitSize (0:: Int)
(l, a) = case () of
_ | 64 <= w -> (8, 25)
_ | 60 <= w -> (8, 24)
_ | 32 <= w -> (6, 7)
_ | 29 <= w -> (6, 5)
sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int
sortClauses s cm nneeds = do
let
rankMax :: Int
rankMax = 2 ^ rankWidth 1
activityMax :: Int
activityMax = 2 ^ activityWidth 1
activityScale :: Double
activityScale = fromIntegral activityMax
indexMax :: Int
indexMax = (2 ^ indexWidth 1)
n <- get' cm
vec <- getClauseVector cm
keys <- getKeyVector cm
let
assignKey :: Int -> Int -> IO Int
assignKey ((< n) -> False) m = return m
assignKey i m = do
c <- getNth vec i
k <- (\k -> if k == 2 then return k else fromEnum <$> get' (protected c)) =<< get' c
case k of
1 -> set' (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1)
2 -> setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)
_ -> do
l <- locked s c
if l
then setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)
else do
d <- rankOf c
b <- floor . (activityScale *) . (1 ) . logBase claActivityThreshold . max 1 <$> get' (activity c)
setNth keys i $ shiftL (min rankMax d) (activityWidth + indexWidth) + shiftL b indexWidth + i
assignKey (i + 1) m
limit <- min n . (+ nneeds) <$> assignKey 0 0
let
sortOnRange :: Int -> Int -> IO ()
sortOnRange left right
| limit < left = return ()
| left >= right = return ()
| left + 1 == right = do
a <- getNth keys left
b <- getNth keys right
unless (a < b) $ swapBetween keys left right
| otherwise = do
let p = div (left + right) 2
pivot <- getNth keys p
swapBetween keys p left
let
nextL :: Int -> IO Int
nextL i@((<= right) -> False) = return i
nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 1) else return i
nextR :: Int -> IO Int
nextR i = do v <- getNth keys i; if pivot < v then nextR (i 1) else return i
divide :: Int -> Int -> IO Int
divide l r = do
l' <- nextL l
r' <- nextR r
if l' < r' then swapBetween keys l' r' >> divide (l' + 1) (r' 1) else return r'
m <- divide (left + 1) right
swapBetween keys left m
sortOnRange left (m 1)
sortOnRange (m + 1) right
sortOnRange 0 (n 1)
let
seek :: Int -> IO ()
seek ((< limit) -> False) = return ()
seek i = do
bits <- getNth keys i
when (indexMax < bits) $ do
c <- getNth vec i
let
sweep k = do
k' <- (indexMax .&.) <$> getNth keys k
setNth keys k k
if k' == i
then setNth vec k c
else getNth vec k' >>= setNth vec k >> sweep k'
sweep i
seek $ i + 1
seek 0
return limit
simplifyDB :: Solver -> IO Bool
simplifyDB s@Solver{..} = do
good <- get' ok
if good
then do
p <- propagate s
if p /= NullClause
then set' ok False >> return False
else do
n <- get' trail
let
vec = asUVector trail
loopOnLit ((< n) -> False) = return ()
loopOnLit i = do
l <- getNth vec i
reset . getNthWatcher watches $ l
reset . getNthWatcher watches $ negateLit l
loopOnLit $ i + 1
loopOnLit 0
let
for :: Int -> IO Bool
for ((< 2) -> False) = return True
for t = do
let ptr = if t == 0 then learnts else clauses
vec' <- getClauseVector ptr
n' <- get' ptr
let
loopOnVector :: Int -> Int -> IO Bool
loopOnVector ((< n') -> False) j = shrinkBy ptr (n' j) >> return True
loopOnVector i j = do
c <- getNth vec' i
l <- locked s c
r <- simplify s c
if not l && r
then removeWatch s c >> loopOnVector (i + 1) j
else setNth vec' j c >> loopOnVector (i + 1) (j + 1)
loopOnVector 0 0
ret <- for 0
reset watches
return ret
else return False
search :: Solver -> Int -> Int -> IO Int
search s@Solver{..} nOfConflicts nOfLearnts = do
let
loop :: Int -> IO Int
loop conflictC = do
!confl <- propagate s
d <- decisionLevel s
if confl /= NullClause
then do
incrementStat s NumOfBackjump 1
r <- get' rootLevel
if d == r
then do
analyzeFinal s confl False
return lFalse
else do
backtrackLevel <- analyze s confl
(s `cancelUntil`) . max backtrackLevel =<< get' rootLevel
newLearntClause s litsLearnt
k <- get' litsLearnt
when (k == 1) $ do
(v :: Var) <- lit2var <$> getNth (asUVector litsLearnt) 0
setNth level v 0
varDecayActivity s
loop $ conflictC + 1
else do
when (d == 0) . void $ simplifyDB s
k1 <- get' learnts
k2 <- nAssigns s
when (k1 k2 >= nOfLearnts) $ reduceDB s
case () of
_ | k2 == nVars -> do
let
toInt :: Var -> IO Lit
toInt v = (\p -> if lTrue == p then v else negate v) <$> valueVar s v
setModel :: Int -> IO ()
setModel ((<= nVars) -> False) = return ()
setModel v = (setNth model v =<< toInt v) >> setModel (v + 1)
setModel 1
return lTrue
_ | conflictC >= nOfConflicts -> do
(s `cancelUntil`) =<< get' rootLevel
claRescaleActivityAfterRestart s
incrementStat s NumOfRestart 1
return lBottom
_ -> do
v <- select s
oldVal <- getNth phases v
unsafeAssume s $ var2lit v (0 < oldVal)
loop conflictC
good <- get' ok
if good then loop 0 else return lFalse
solve :: (Foldable t) => Solver -> t Lit -> IO Bool
solve s@Solver{..} assumps = do
let
injector :: Lit -> Bool -> IO Bool
injector _ False = return False
injector 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 injector True assumps else return False
if not x
then return False
else do
set' rootLevel =<< decisionLevel s
nc <- fromIntegral <$> nClauses s
let
while :: Double -> Double -> IO Bool
while nOfConflicts nOfLearnts = do
status <- search s (floor nOfConflicts) (floor nOfLearnts)
if status == lBottom
then while (1.5 * nOfConflicts) (1.1 * nOfLearnts)
else cancelUntil s 0 >> return (status == lTrue)
while 100 (nc / 3.0)
unsafeEnqueue :: Solver -> Lit -> Clause -> IO ()
unsafeEnqueue s@Solver{..} p from = do
let v = lit2var p
setNth assigns v $! if positiveLit p then lTrue else lFalse
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