module SAT
(
Solver
, newSolver
, Var
, Lit
, literal
, litNot
, litVar
, litPolarity
, Clause
, newVar
, newVars
, newVars_
, addClause
, addAtLeast
, addAtMost
, addExactly
, addPBAtLeast
, addPBAtMost
, addPBExactly
, addPBAtLeastSoft
, addPBAtMostSoft
, addPBExactlySoft
, solve
, solveWith
, BudgetExceeded (..)
, Model
, model
, failedAssumptions
, RestartStrategy (..)
, setRestartStrategy
, defaultRestartStrategy
, setRestartFirst
, defaultRestartFirst
, setRestartInc
, defaultRestartInc
, setLearntSizeFirst
, defaultLearntSizeFirst
, setLearntSizeInc
, defaultLearntSizeInc
, setCCMin
, defaultCCMin
, LearningStrategy (..)
, setLearningStrategy
, defaultLearningStrategy
, setVarPolarity
, setLogger
, setCheckModel
, setRandomFreq
, defaultRandomFreq
, setRandomSeed
, setConfBudget
, nVars
, nAssigns
, nClauses
, nLearnt
, varBumpActivity
, varDecayActivity
) where
import Prelude hiding (log)
import Control.Monad
import Control.Exception
#if MIN_VERSION_array(0,4,0)
import Data.Array.IO hiding (unsafeFreeze)
import Data.Array.Unsafe (unsafeFreeze)
#else
import Data.Array.IO
#endif
import Data.Array.Base (unsafeRead, unsafeWrite)
import Data.IORef
import Data.List
import Data.Maybe
import Data.Ord
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Set as Set
import qualified Data.IndexedPriorityQueue as PQ
import qualified Data.SeqQueue as SQ
import Data.Time
import Data.Typeable
import System.CPUTime
import qualified System.Random as Rand
import Text.Printf
import Data.LBool
import SAT.Types
type Level = Int
levelRoot :: Level
levelRoot = 1
data Assignment
= Assignment
{ aValue :: !Bool
, aLevel :: !Level
, aReason :: !(Maybe SomeConstraint)
, aBacktrackCBs :: !(IORef [IO ()])
}
data VarData
= VarData
{ vdAssignment :: !(IORef (Maybe Assignment))
, vdPolarity :: !(IORef Bool)
, vdPosLitData :: !LitData
, vdNegLitData :: !LitData
, vdActivity :: !(IORef VarActivity)
}
newtype LitData
= LitData
{
ldWatches :: IORef [SomeConstraint]
}
newVarData :: IO VarData
newVarData = do
ainfo <- newIORef Nothing
polarity <- newIORef True
pos <- newLitData
neg <- newLitData
activity <- newIORef 0
return $ VarData ainfo polarity pos neg activity
newLitData :: IO LitData
newLitData = do
ws <- newIORef []
return $ LitData ws
varData :: Solver -> Var -> IO VarData
varData s !v = do
a <- readIORef (svVarData s)
unsafeRead a (v1)
litData :: Solver -> Lit -> IO LitData
litData s !l =
if litPolarity l
then do
vd <- varData s l
return $ vdPosLitData vd
else do
vd <- varData s (negate l)
return $ vdNegLitData vd
varValue :: Solver -> Var -> IO LBool
varValue s !v = do
vd <- varData s v
m <- readIORef (vdAssignment vd)
case m of
Nothing -> return lUndef
Just x -> return $! (liftBool $! aValue x)
litValue :: Solver -> Lit -> IO LBool
litValue s !l = do
if litPolarity l
then varValue s l
else do
m <- varValue s (negate l)
return $! lnot m
varLevel :: Solver -> Var -> IO Level
varLevel s !v = do
vd <- varData s v
m <- readIORef (vdAssignment vd)
case m of
Nothing -> error ("varLevel: unassigned var " ++ show v)
Just a -> return (aLevel a)
litLevel :: Solver -> Lit -> IO Level
litLevel s l = varLevel s (litVar l)
varReason :: Solver -> Var -> IO (Maybe SomeConstraint)
varReason s !v = do
vd <- varData s v
m <- readIORef (vdAssignment vd)
case m of
Nothing -> error ("varReason: unassigned var " ++ show v)
Just a -> return (aReason a)
data Solver
= Solver
{ svOk :: !(IORef Bool)
, svVarQueue :: !PQ.PriorityQueue
, svTrail :: !(IORef [Lit])
, svVarCounter :: !(IORef Int)
, svVarData :: !(IORef (IOArray Int VarData))
, svClauseDB :: !(IORef [SomeConstraint])
, svLearntDB :: !(IORef (Int,[SomeConstraint]))
, svAssumptions :: !(IORef (IOUArray Int Lit))
, svLevel :: !(IORef Level)
, svBCPQueue :: !(SQ.SeqQueue Lit)
, svModel :: !(IORef (Maybe Model))
, svNDecision :: !(IORef Int)
, svNRandomDecision :: !(IORef Int)
, svNConflict :: !(IORef Int)
, svNRestart :: !(IORef Int)
, svNAssigns :: !(IORef Int)
, svNFixed :: !(IORef Int)
, svNLearntGC :: !(IORef Int)
, svNRemovedConstr :: !(IORef Int)
, svVarDecay :: !(IORef Double)
, svVarInc :: !(IORef Double)
, svClaDecay :: !(IORef Double)
, svClaInc :: !(IORef Double)
, svRestartStrategy :: !(IORef RestartStrategy)
, svRestartFirst :: !(IORef Int)
, svRestartInc :: !(IORef Double)
, svLearntSizeFirst :: !(IORef Int)
, svLearntSizeInc :: !(IORef Double)
, svLearntLim :: !(IORef Int)
, svLearntLimAdjCnt :: !(IORef Int)
, svLearntLimSeq :: !(IORef [(Int,Int)])
, svCCMin :: !(IORef Int)
, svLearningStrategy :: !(IORef LearningStrategy)
, svLogger :: !(IORef (Maybe (String -> IO ())))
, svStartWC :: !(IORef UTCTime)
, svLastStatWC :: !(IORef UTCTime)
, svCheckModel :: !(IORef Bool)
, svRandomFreq :: !(IORef Double)
, svRandomGen :: !(IORef Rand.StdGen)
, svFailedAssumptions :: !(IORef [Lit])
, svConfBudget :: !(IORef Int)
}
markBad :: Solver -> IO ()
markBad solver = writeIORef (svOk solver) False
bcpEnqueue :: Solver -> Lit -> IO ()
bcpEnqueue solver l = SQ.enqueue (svBCPQueue solver) l
bcpDequeue :: Solver -> IO (Maybe Lit)
bcpDequeue solver = SQ.dequeue (svBCPQueue solver)
assignBy :: Constraint c => Solver -> Lit -> c -> IO Bool
assignBy solver lit c = assign_ solver lit (Just (toConstraint c))
assign :: Solver -> Lit -> IO Bool
assign solver lit = assign_ solver lit Nothing
assign_ :: Solver -> Lit -> Maybe SomeConstraint -> IO Bool
assign_ solver !lit reason = assert (validLit lit) $ do
vd <- varData solver (litVar lit)
m <- readIORef (vdAssignment vd)
case m of
Just a -> return $ litPolarity lit == aValue a
Nothing -> do
lv <- readIORef (svLevel solver)
bt <- newIORef []
writeIORef (vdAssignment vd) $ Just $
Assignment
{ aValue = litPolarity lit
, aLevel = lv
, aReason = reason
, aBacktrackCBs = bt
}
modifyIORef (svTrail solver) (lit:)
modifyIORef' (svNAssigns solver) (+1)
when (lv == levelRoot) $ modifyIORef' (svNFixed solver) (+1)
bcpEnqueue solver lit
when debugMode $ logIO solver $ do
let r = case reason of
Nothing -> ""
Just _ -> " by propagation"
return $ printf "assign(level=%d): %d%s" lv lit r
return True
unassign :: Solver -> Var -> IO ()
unassign solver !v = assert (validVar v) $ do
vd <- varData solver v
m <- readIORef (vdAssignment vd)
case m of
Nothing -> error "unassign: should not happen"
Just a -> do
writeIORef (vdPolarity vd) (aValue a)
readIORef (aBacktrackCBs a) >>= sequence_
writeIORef (vdAssignment vd) Nothing
modifyIORef' (svNAssigns solver) (subtract 1)
PQ.enqueue (svVarQueue solver) v
addBacktrackCB :: Solver -> Var -> IO () -> IO ()
addBacktrackCB solver !v callback = do
vd <- varData solver v
m <- readIORef (vdAssignment vd)
case m of
Nothing -> error "addBacktrackCB: should not happen"
Just a -> modifyIORef (aBacktrackCBs a) (callback :)
watch :: Constraint c => Solver -> Lit -> c -> IO ()
watch solver !lit c = do
when debugMode $ do
lits <- watchedLiterals solver c
unless (lit `elem` lits) $ error "watch: should not happen"
ld <- litData solver lit
modifyIORef (ldWatches ld) (toConstraint c : )
watches :: Solver -> Lit -> IO [SomeConstraint]
watches solver !lit = do
ld <- litData solver lit
readIORef (ldWatches ld)
addToDB :: Constraint c => Solver -> c -> IO ()
addToDB solver c = do
modifyIORef (svClauseDB solver) (toConstraint c : )
when debugMode $ logIO solver $ do
str <- showConstraint solver c
return $ printf "constraint %s is added" str
sanityCheck solver
addToLearntDB :: Constraint c => Solver -> c -> IO ()
addToLearntDB solver c = do
modifyIORef (svLearntDB solver) $ \(n,xs) -> (n+1, toConstraint c : xs)
when debugMode $ logIO solver $ do
str <- showConstraint solver c
return $ printf "constraint %s is added" str
sanityCheck solver
reduceDB :: Solver -> IO ()
reduceDB solver = do
(_,cs) <- readIORef (svLearntDB solver)
xs <- forM cs $ \c -> do
p <- constrIsProtected solver c
actval <- constrActivity solver c
return (c, (p, actval))
let ys = sortBy (comparing snd) xs
(zs,ws) = splitAt (length ys `div` 2) ys
let loop [] ret = return ret
loop ((c,(isShort,_)) : rest) ret = do
flag <- if isShort
then return True
else isLocked solver c
if flag
then loop rest (c:ret)
else do
detach solver c
loop rest ret
zs2 <- loop zs []
let cs2 = zs2 ++ map fst ws
n2 = length cs2
writeIORef (svLearntDB solver) (n2,cs2)
type VarActivity = Double
varActivity :: Solver -> Var -> IO VarActivity
varActivity solver !v = do
vd <- varData solver v
readIORef (vdActivity vd)
varDecayActivity :: Solver -> IO ()
varDecayActivity solver = do
d <- readIORef (svVarDecay solver)
modifyIORef' (svVarInc solver) (d*)
varBumpActivity :: Solver -> Var -> IO ()
varBumpActivity solver !v = do
inc <- readIORef (svVarInc solver)
vd <- varData solver v
modifyIORef' (vdActivity vd) (+inc)
PQ.update (svVarQueue solver) v
aval <- readIORef (vdActivity vd)
when (aval > 1e20) $
varRescaleAllActivity solver
varRescaleAllActivity :: Solver -> IO ()
varRescaleAllActivity solver = do
vs <- variables solver
forM_ vs $ \v -> do
vd <- varData solver v
modifyIORef' (vdActivity vd) (* 1e-20)
modifyIORef' (svVarInc solver) (* 1e-20)
variables :: Solver -> IO [Var]
variables solver = do
n <- nVars solver
return [1 .. n]
nVars :: Solver -> IO Int
nVars solver = do
vcnt <- readIORef (svVarCounter solver)
return $! (vcnt1)
nAssigns :: Solver -> IO Int
nAssigns solver = readIORef (svNAssigns solver)
nClauses :: Solver -> IO Int
nClauses solver = do
xs <- readIORef (svClauseDB solver)
return $ length xs
nLearnt :: Solver -> IO Int
nLearnt solver = do
(n,_) <- readIORef (svLearntDB solver)
return n
learntConstraints :: Solver -> IO [SomeConstraint]
learntConstraints solver = do
(_,cs) <- readIORef (svLearntDB solver)
return cs
newSolver :: IO Solver
newSolver = do
rec
ok <- newIORef True
vcnt <- newIORef 1
trail <- newIORef []
vars <- newIORef =<< newArray_ (1,0)
vqueue <- PQ.newPriorityQueueBy (ltVar solver)
db <- newIORef []
db2 <- newIORef (0,[])
as <- newIORef =<< newArray_ (0,1)
lv <- newIORef levelRoot
q <- SQ.newFifo
m <- newIORef Nothing
ndecision <- newIORef 0
nranddec <- newIORef 0
nconflict <- newIORef 0
nrestart <- newIORef 0
nassigns <- newIORef 0
nfixed <- newIORef 0
nlearntgc <- newIORef 0
nremoved <- newIORef 0
claDecay <- newIORef (1 / 0.999)
claInc <- newIORef 1
varDecay <- newIORef (1 / 0.95)
varInc <- newIORef 1
restartStrat <- newIORef defaultRestartStrategy
restartFirst <- newIORef defaultRestartFirst
restartInc <- newIORef defaultRestartInc
learning <- newIORef defaultLearningStrategy
learntSizeFirst <- newIORef defaultLearntSizeFirst
learntSizeInc <- newIORef defaultLearntSizeInc
ccMin <- newIORef defaultCCMin
checkModel <- newIORef False
learntLim <- newIORef undefined
learntLimAdjCnt <- newIORef (1)
learntLimSeq <- newIORef undefined
logger <- newIORef Nothing
startWC <- newIORef undefined
lastStatWC <- newIORef undefined
randfreq <- newIORef defaultRandomFreq
randgen <- newIORef =<< Rand.newStdGen
failed <- newIORef []
confBudget <- newIORef (1)
let solver =
Solver
{ svOk = ok
, svVarCounter = vcnt
, svVarQueue = vqueue
, svTrail = trail
, svVarData = vars
, svClauseDB = db
, svLearntDB = db2
, svAssumptions = as
, svLevel = lv
, svBCPQueue = q
, svModel = m
, svNDecision = ndecision
, svNRandomDecision = nranddec
, svNConflict = nconflict
, svNRestart = nrestart
, svNAssigns = nassigns
, svNFixed = nfixed
, svNLearntGC = nlearntgc
, svNRemovedConstr = nremoved
, svVarDecay = varDecay
, svVarInc = varInc
, svClaDecay = claDecay
, svClaInc = claInc
, svRestartStrategy = restartStrat
, svRestartFirst = restartFirst
, svRestartInc = restartInc
, svLearningStrategy = learning
, svLearntSizeFirst = learntSizeFirst
, svLearntSizeInc = learntSizeInc
, svCCMin = ccMin
, svLearntLim = learntLim
, svLearntLimAdjCnt = learntLimAdjCnt
, svLearntLimSeq = learntLimSeq
, svLogger = logger
, svStartWC = startWC
, svLastStatWC = lastStatWC
, svCheckModel = checkModel
, svRandomFreq = randfreq
, svRandomGen = randgen
, svFailedAssumptions = failed
, svConfBudget = confBudget
}
return solver
ltVar :: Solver -> Var -> Var -> IO Bool
ltVar solver v1 v2 = do
a1 <- varActivity solver v1
a2 <- varActivity solver v2
return $! a1 > a2
newVar :: Solver -> IO Var
newVar s = do
v <- readIORef (svVarCounter s)
writeIORef (svVarCounter s) (v+1)
vd <- newVarData
a <- readIORef (svVarData s)
(_,ub) <- getBounds a
if v <= ub
then writeArray a v vd
else do
let ub' = max 2 (ub * 3 `div` 2)
a' <- newArray_ (1,ub')
forM_ [1..ub] $ \v2 -> do
vd2 <- readArray a v2
writeArray a' v2 vd2
writeArray a' v vd
writeIORef (svVarData s) a'
PQ.enqueue (svVarQueue s) v
return v
newVars :: Solver -> Int -> IO [Var]
newVars s n = replicateM n (newVar s)
newVars_ :: Solver -> Int -> IO ()
newVars_ s n = replicateM_ n (newVar s)
addClause :: Solver -> Clause -> IO ()
addClause solver lits = do
d <- readIORef (svLevel solver)
assert (d == levelRoot) $ return ()
lits2 <- instantiateClause solver lits
case normalizeClause =<< lits2 of
Nothing -> return ()
Just [] -> markBad solver
Just [lit] -> do
ret <- assign solver lit
assert ret $ return ()
ret2 <- deduce solver
case ret2 of
Nothing -> return ()
Just _ -> markBad solver
Just lits3 -> do
clause <- newClauseData lits3 False
attach solver clause
addToDB solver clause
addAtLeast :: Solver
-> [Lit]
-> Int
-> IO ()
addAtLeast solver lits n = do
d <- readIORef (svLevel solver)
assert (d == levelRoot) $ return ()
(lits',n') <- liftM normalizeAtLeast $ instantiateAtLeast solver (lits,n)
let len = length lits'
if n' <= 0 then return ()
else if n' > len then markBad solver
else if n' == 1 then addClause solver lits'
else if n' == len then do
forM_ lits' $ \l -> do
ret <- assign solver l
assert ret $ return ()
ret2 <- deduce solver
case ret2 of
Nothing -> return ()
Just _ -> markBad solver
else do
c <- newAtLeastData lits' n' False
attach solver c
addToDB solver c
addAtMost :: Solver
-> [Lit]
-> Int
-> IO ()
addAtMost solver lits n = addAtLeast solver lits' (lenn)
where
len = length lits
lits' = map litNot lits
addExactly :: Solver
-> [Lit]
-> Int
-> IO ()
addExactly solver lits n = do
addAtLeast solver lits n
addAtMost solver lits n
addPBAtLeast :: Solver
-> [(Integer,Lit)]
-> Integer
-> IO ()
addPBAtLeast solver ts n = do
d <- readIORef (svLevel solver)
assert (d == levelRoot) $ return ()
(ts',degree) <- liftM normalizePBAtLeast $ instantiatePB solver (ts,n)
let cs = map fst ts'
slack = sum cs degree
if degree <= 0 then return ()
else if slack < 0 then markBad solver
else if Set.size (Set.fromList cs) == 1 then do
let c = head cs
addAtLeast solver (map snd ts') (fromInteger ((degree+c1) `div` c))
else do
c <- newPBAtLeastData ts' degree False
attach solver c
addToDB solver c
ret <- pbPropagate solver c
if not ret
then do
markBad solver
else do
ret2 <- deduce solver
case ret2 of
Nothing -> return ()
Just _ -> markBad solver
addPBAtMost :: Solver
-> [(Integer,Lit)]
-> Integer
-> IO ()
addPBAtMost solver ts n = addPBAtLeast solver [(c,l) | (c,l) <- ts] (negate n)
addPBExactly :: Solver
-> [(Integer,Lit)]
-> Integer
-> IO ()
addPBExactly solver ts n = do
(ts2,n2) <- liftM normalizePBExactly $ instantiatePB solver (ts,n)
addPBAtLeast solver ts2 n2
addPBAtMost solver ts2 n2
addPBAtLeastSoft
:: Solver
-> Lit
-> [(Integer,Lit)]
-> Integer
-> IO ()
addPBAtLeastSoft solver sel lhs rhs = do
(lhs', rhs') <- liftM normalizePBAtLeast $ instantiatePB solver (lhs,rhs)
addPBAtLeast solver ((rhs', litNot sel) : lhs') rhs'
addPBAtMostSoft
:: Solver
-> Lit
-> [(Integer,Lit)]
-> Integer
-> IO ()
addPBAtMostSoft solver sel lhs rhs =
addPBAtLeastSoft solver sel [(negate c, lit) | (c,lit) <- lhs] (negate rhs)
addPBExactlySoft
:: Solver
-> Lit
-> [(Integer,Lit)]
-> Integer
-> IO ()
addPBExactlySoft solver sel lhs rhs = do
(lhs2, rhs2) <- liftM normalizePBExactly $ instantiatePB solver (lhs,rhs)
addPBAtLeastSoft solver sel lhs2 rhs2
addPBAtMostSoft solver sel lhs2 rhs2
solve :: Solver -> IO Bool
solve solver = do
as <- newArray_ (0,1)
writeIORef (svAssumptions solver) as
solve_ solver
solveWith :: Solver
-> [Lit]
-> IO Bool
solveWith solver ls = do
as <- newListArray (0, length ls 1) ls
writeIORef (svAssumptions solver) as
solve_ solver
solve_ :: Solver -> IO Bool
solve_ solver = do
log solver "Solving starts ..."
resetStat solver
writeIORef (svModel solver) Nothing
writeIORef (svFailedAssumptions solver) []
ok <- readIORef (svOk solver)
if not ok
then return False
else do
when debugMode $ dumpVarActivity solver
d <- readIORef (svLevel solver)
assert (d == levelRoot) $ return ()
restartStrategy <- readIORef (svRestartStrategy solver)
restartFirst <- readIORef (svRestartFirst solver)
restartInc <- readIORef (svRestartInc solver)
let restartSeq = mkRestartSeq restartStrategy restartFirst restartInc
let learntSizeAdj = do
(size,adj) <- shift (svLearntLimSeq solver)
writeIORef (svLearntLim solver) size
writeIORef (svLearntLimAdjCnt solver) adj
onConflict = do
cnt <- readIORef (svLearntLimAdjCnt solver)
if (cnt==0)
then learntSizeAdj
else writeIORef (svLearntLimAdjCnt solver) $! cnt1
cnt <- readIORef (svLearntLimAdjCnt solver)
when (cnt == 1) $ do
learntSizeFirst <- readIORef (svLearntSizeFirst solver)
learntSizeInc <- readIORef (svLearntSizeInc solver)
nc <- nClauses solver
nv <- nVars solver
let initialLearntLim = if learntSizeFirst > 0 then learntSizeFirst else max ((nc + nv) `div` 3) 16
learntSizeSeq = iterate (ceiling . (learntSizeInc*) . fromIntegral) initialLearntLim
learntSizeAdjSeq = iterate (\x -> (x * 3) `div` 2) (100::Int)
writeIORef (svLearntLimSeq solver) (zip learntSizeSeq learntSizeAdjSeq)
learntSizeAdj
let loop [] = error "solve_: should not happen"
loop (conflict_lim:rs) = do
printStat solver True
ret <- search solver conflict_lim onConflict
case ret of
SRFinished x -> return $ Just x
SRBudgetExceeded -> return Nothing
SRRestart -> do
modifyIORef' (svNRestart solver) (+1)
backtrackTo solver levelRoot
loop rs
printStatHeader solver
startCPU <- getCPUTime
startWC <- getCurrentTime
writeIORef (svStartWC solver) startWC
result <- loop restartSeq
endCPU <- getCPUTime
endWC <- getCurrentTime
when (result == Just True) $ do
checkModel <- readIORef (svCheckModel solver)
when checkModel $ checkSatisfied solver
constructModel solver
backtrackTo solver levelRoot
when debugMode $ dumpVarActivity solver
when debugMode $ dumpClaActivity solver
printStat solver True
(log solver . printf "#cpu_time = %.3fs") (fromIntegral (endCPU startCPU) / 10^(12::Int) :: Double)
(log solver . printf "#wall_clock_time = %.3fs") (realToFrac (endWC `diffUTCTime` startWC) :: Double)
(log solver . printf "#decision = %d") =<< readIORef (svNDecision solver)
(log solver . printf "#random_decision = %d") =<< readIORef (svNRandomDecision solver)
(log solver . printf "#conflict = %d") =<< readIORef (svNConflict solver)
(log solver . printf "#restart = %d") =<< readIORef (svNRestart solver)
case result of
Just x -> return x
Nothing -> throw BudgetExceeded
data BudgetExceeded = BudgetExceeded
deriving (Show, Typeable)
instance Exception BudgetExceeded
data SearchResult
= SRFinished Bool
| SRRestart
| SRBudgetExceeded
search :: Solver -> Int -> IO () -> IO SearchResult
search solver !conflict_lim onConflict = loop 0
where
loop :: Int -> IO SearchResult
loop !c = do
sanityCheck solver
conflict <- deduce solver
sanityCheck solver
case conflict of
Nothing -> do
lv <- readIORef (svLevel solver)
when (lv == levelRoot) $ simplify solver
n <- nLearnt solver
m <- nAssigns solver
learnt_lim <- readIORef (svLearntLim solver)
when (learnt_lim >= 0 && n m > learnt_lim) $ do
modifyIORef' (svNLearntGC solver) (+1)
reduceDB solver
r <- pickAssumption
case r of
Nothing -> return (SRFinished False)
Just lit
| lit /= litUndef -> decide solver lit >> loop c
| otherwise -> do
lit2 <- pickBranchLit solver
if lit2 == litUndef
then return (SRFinished True)
else decide solver lit2 >> loop c
Just constr -> do
varDecayActivity solver
constrDecayActivity solver
onConflict
modifyIORef' (svNConflict solver) (+1)
d <- readIORef (svLevel solver)
when debugMode $ logIO solver $ do
str <- showConstraint solver constr
return $ printf "conflict(level=%d): %s" d str
when (c `mod` 100 == 0) $ do
printStat solver False
modifyIORef' (svConfBudget solver) $ \confBudget ->
if confBudget > 0 then confBudget 1 else confBudget
confBudget <- readIORef (svConfBudget solver)
if d == levelRoot
then markBad solver >> return (SRFinished False)
else if confBudget==0 then
return SRBudgetExceeded
else if conflict_lim >= 0 && c+1 >= conflict_lim then
return SRRestart
else do
b <- handleConflict constr
if b
then loop (c+1)
else markBad solver >> return (SRFinished False)
pickAssumption :: IO (Maybe Lit)
pickAssumption = do
!as <- readIORef (svAssumptions solver)
!b <- getBounds as
let go = do
d <- readIORef (svLevel solver)
if not (inRange b (d+1))
then return (Just litUndef)
else do
l <- readArray as (d+1)
val <- litValue solver l
if val == lTrue then do
modifyIORef' (svLevel solver) (+1)
go
else if val == lFalse then do
core <- analyzeFinal solver l
writeIORef (svFailedAssumptions solver) core
return Nothing
else
return (Just l)
go
handleConflict :: SomeConstraint -> IO Bool
handleConflict constr = do
strat <- readIORef (svLearningStrategy solver)
case strat of
LearningClause -> do
(learntClause, level) <- analyzeConflict solver constr
backtrackTo solver level
case learntClause of
[] -> error "search(LearningClause): should not happen"
[lit] -> do
ret <- assign solver lit
assert ret $ return ()
return ()
lit:_ -> do
cl <- newClauseData learntClause True
attach solver cl
addToLearntDB solver cl
assignBy solver lit cl
constrBumpActivity solver cl
return True
LearningHybrid -> do
(learntClause, level, pb) <- analyzeConflictHybrid solver constr
level2 <- pbBacktrackLevel solver pb
let level3 = min level level2
pbdata <- newPBAtLeastData (fst pb) (snd pb) True
attach solver pbdata
addToLearntDB solver pbdata
backtrackTo solver level3
slack <- readIORef (pbSlack pbdata)
if slack < 0
then do
if level3 == levelRoot
then return False
else handleConflict (toConstraint pbdata)
else do
case learntClause of
[] -> error "search(LearningHybrid): should not happen"
[lit] -> do
ret <- assign solver lit
assert ret $ return ()
return ()
lit:_ -> do
cl <- newClauseData learntClause True
attach solver cl
addToLearntDB solver cl
when (level3 == level) $ do
assignBy solver lit cl
constrBumpActivity solver cl
pbPropagate solver pbdata
return True
model :: Solver -> IO Model
model solver = do
m <- readIORef (svModel solver)
return (fromJust m)
failedAssumptions :: Solver -> IO [Lit]
failedAssumptions solver = readIORef (svFailedAssumptions solver)
simplify :: Solver -> IO ()
simplify solver = do
let loop [] rs !n = return (rs,n)
loop (y:ys) rs !n = do
b1 <- isSatisfied solver y
b2 <- isLocked solver y
if b1 && not b2
then do
detach solver y
loop ys rs (n+1)
else loop ys (y:rs) n
do
xs <- readIORef (svClauseDB solver)
(ys,n) <- loop xs [] (0::Int)
modifyIORef' (svNRemovedConstr solver) (+n)
writeIORef (svClauseDB solver) ys
do
(m,xs) <- readIORef (svLearntDB solver)
(ys,n) <- loop xs [] (0::Int)
writeIORef (svLearntDB solver) (mn, ys)
setRestartStrategy :: Solver -> RestartStrategy -> IO ()
setRestartStrategy solver s = writeIORef (svRestartStrategy solver) s
defaultRestartStrategy :: RestartStrategy
defaultRestartStrategy = MiniSATRestarts
setRestartFirst :: Solver -> Int -> IO ()
setRestartFirst solver !n = writeIORef (svRestartFirst solver) n
defaultRestartFirst :: Int
defaultRestartFirst = 100
setRestartInc :: Solver -> Double -> IO ()
setRestartInc solver !r = writeIORef (svRestartInc solver) r
defaultRestartInc :: Double
defaultRestartInc = 1.5
data LearningStrategy
= LearningClause
| LearningHybrid
setLearningStrategy :: Solver -> LearningStrategy -> IO ()
setLearningStrategy solver l = writeIORef (svLearningStrategy solver) $! l
defaultLearningStrategy :: LearningStrategy
defaultLearningStrategy = LearningClause
setLearntSizeFirst :: Solver -> Int -> IO ()
setLearntSizeFirst solver !x = writeIORef (svLearntSizeFirst solver) x
defaultLearntSizeFirst :: Int
defaultLearntSizeFirst = 1
setLearntSizeInc :: Solver -> Double -> IO ()
setLearntSizeInc solver !r = writeIORef (svLearntSizeInc solver) r
defaultLearntSizeInc :: Double
defaultLearntSizeInc = 1.1
setCCMin :: Solver -> Int -> IO ()
setCCMin solver !v = writeIORef (svCCMin solver) v
defaultCCMin :: Int
defaultCCMin = 2
setVarPolarity :: Solver -> Var -> Bool -> IO ()
setVarPolarity solver v val = do
vd <- varData solver v
writeIORef (vdPolarity vd) val
setCheckModel :: Solver -> Bool -> IO ()
setCheckModel solver flag = do
writeIORef (svCheckModel solver) flag
setRandomFreq :: Solver -> Double -> IO ()
setRandomFreq solver r = do
writeIORef (svRandomFreq solver) r
defaultRandomFreq :: Double
defaultRandomFreq = 0.005
setRandomSeed :: Solver -> Int -> IO ()
setRandomSeed solver seed = do
writeIORef (svRandomGen solver) (Rand.mkStdGen seed)
setConfBudget :: Solver -> Maybe Int -> IO ()
setConfBudget solver (Just b) | b >= 0 = writeIORef (svConfBudget solver) b
setConfBudget solver _ = writeIORef (svConfBudget solver) (1)
pickBranchLit :: Solver -> IO Lit
pickBranchLit !solver = do
let vqueue = svVarQueue solver
let withRandGen :: (Rand.StdGen -> (a, Rand.StdGen)) -> IO a
withRandGen f = do
randgen <- readIORef (svRandomGen solver)
let (r, randgen') = f randgen
writeIORef (svRandomGen solver) randgen'
return r
!randfreq <- readIORef (svRandomFreq solver)
!size <- PQ.queueSize vqueue
!r <- withRandGen Rand.random
var <-
if (r < randfreq && size >= 2)
then do
a <- PQ.getHeapArray vqueue
i <- withRandGen $ Rand.randomR (0, size1)
var <- readArray a i
val <- varValue solver var
if val == lUndef
then do
modifyIORef' (svNRandomDecision solver) (1+)
return var
else return litUndef
else
return litUndef
let loop :: IO Var
loop = do
m <- PQ.dequeue vqueue
case m of
Nothing -> return litUndef
Just var2 -> do
val2 <- varValue solver var2
if val2 /= lUndef
then loop
else return var2
var2 <-
if var==litUndef
then loop
else return var
if var2==litUndef
then return litUndef
else do
vd <- varData solver var2
p <- readIORef (vdPolarity vd)
return $! literal var2 p
decide :: Solver -> Lit -> IO ()
decide solver !lit = do
modifyIORef' (svNDecision solver) (+1)
modifyIORef' (svLevel solver) (+1)
when debugMode $ do
val <- litValue solver lit
when (val /= lUndef) $ error "decide: should not happen"
assign solver lit
return ()
deduce :: Solver -> IO (Maybe SomeConstraint)
deduce solver = loop
where
loop :: IO (Maybe SomeConstraint)
loop = do
r <- bcpDequeue solver
case r of
Nothing -> return Nothing
Just lit -> do
ret <- processLit lit
case ret of
Just _ -> return ret
Nothing -> loop
processLit :: Lit -> IO (Maybe SomeConstraint)
processLit !lit = do
let lit2 = litNot lit
ld <- litData solver lit2
let wsref = ldWatches ld
let loop2 [] = return Nothing
loop2 (w:ws) = do
ok <- propagate solver w lit2
if ok
then loop2 ws
else do
modifyIORef wsref (++ws)
return (Just w)
ws <- readIORef wsref
writeIORef wsref []
loop2 ws
analyzeConflict :: Constraint c => Solver -> c -> IO (Clause, Level)
analyzeConflict solver constr = do
d <- readIORef (svLevel solver)
let split :: [Lit] -> IO (LitSet, LitSet)
split = go (IS.empty, IS.empty)
where
go (xs,ys) [] = return (xs,ys)
go (xs,ys) (l:ls) = do
lv <- litLevel solver l
if lv == levelRoot then
go (xs,ys) ls
else if lv >= d then
go (IS.insert l xs, ys) ls
else
go (xs, IS.insert l ys) ls
let loop :: LitSet -> LitSet -> IO LitSet
loop lits1 lits2
| sz==1 = do
return $ lits1 `IS.union` lits2
| sz>=2 = do
ret <- popTrail solver
case ret of
Nothing -> do
error $ printf "analyzeConflict: should not happen: empty trail: loop %s %s"
(show lits1) (show lits2)
Just l -> do
if litNot l `IS.notMember` lits1
then do
unassign solver (litVar l)
loop lits1 lits2
else do
m <- varReason solver (litVar l)
case m of
Nothing -> error "analyzeConflict: should not happen"
Just constr2 -> do
constrBumpActivity solver constr2
xs <- reasonOf solver constr2 (Just l)
forM_ xs $ \lit -> varBumpActivity solver (litVar lit)
unassign solver (litVar l)
(ys,zs) <- split xs
loop (IS.delete (litNot l) lits1 `IS.union` ys)
(lits2 `IS.union` zs)
| otherwise = error "analyzeConflict: should not happen: reason of current level is empty"
where
sz = IS.size lits1
constrBumpActivity solver constr
conflictClause <- reasonOf solver constr Nothing
forM_ conflictClause $ \lit -> varBumpActivity solver (litVar lit)
(ys,zs) <- split conflictClause
lits <- loop ys zs
lits2 <- minimizeConflictClause solver lits
xs <- liftM (sortBy (flip (comparing snd))) $
forM (IS.toList lits2) $ \l -> do
lv <- litLevel solver l
return (l,lv)
let level = case xs of
[] -> error "analyzeConflict: should not happen"
[_] -> levelRoot
_:(_,lv):_ -> lv
return (map fst xs, level)
analyzeFinal :: Solver -> Lit -> IO [Lit]
analyzeFinal solver p = do
lits <- readIORef (svTrail solver)
let go :: [Lit] -> VarSet -> [Lit] -> IO [Lit]
go [] _ result = return result
go (l:ls) seen result = do
lv <- litLevel solver l
if lv == levelRoot then
return result
else if litVar l `IS.member` seen then do
r <- varReason solver (litVar l)
case r of
Nothing -> do
let seen' = IS.delete (litVar l) seen
go ls seen' (l : result)
Just constr -> do
c <- reasonOf solver constr (Just l)
let seen' = IS.delete (litVar l) seen `IS.union` IS.fromList [litVar l2 | l2 <- c]
go ls seen' result
else
go ls seen result
go lits (IS.singleton (litVar p)) [p]
analyzeConflictHybrid :: Constraint c => Solver -> c -> IO (Clause, Level, ([(Integer,Lit)], Integer))
analyzeConflictHybrid solver constr = do
d <- readIORef (svLevel solver)
let split :: [Lit] -> IO (LitSet, LitSet)
split = go (IS.empty, IS.empty)
where
go (xs,ys) [] = return (xs,ys)
go (xs,ys) (l:ls) = do
lv <- litLevel solver l
if lv == levelRoot then
go (xs,ys) ls
else if lv >= d then
go (IS.insert l xs, ys) ls
else
go (xs, IS.insert l ys) ls
let loop :: LitSet -> LitSet -> ([(Integer,Lit)],Integer) -> IO (LitSet, ([(Integer,Lit)],Integer))
loop lits1 lits2 pb
| sz==1 = do
return $ (lits1 `IS.union` lits2, pb)
| sz>=2 = do
ret <- popTrail solver
case ret of
Nothing -> do
error $ printf "analyzeConflictHybrid: should not happen: empty trail: loop %s %s"
(show lits1) (show lits2)
Just l -> do
m <- varReason solver (litVar l)
case m of
Nothing -> error "analyzeConflictHybrid: should not happen"
Just constr2 -> do
xs <- reasonOf solver constr2 (Just l)
(lits1',lits2') <-
if litNot l `IS.notMember` lits1
then return (lits1,lits2)
else do
constrBumpActivity solver constr2
forM_ xs $ \lit -> varBumpActivity solver (litVar lit)
(ys,zs) <- split xs
return (IS.delete (litNot l) lits1 `IS.union` ys, lits2 `IS.union` zs)
pb2 <- toPBAtLeast solver constr2
o <- pbOverSAT solver pb2
let pb3 = if o then ([(1,l2) | l2 <- l:xs],1) else pb2
let pb' =
if any (\(_,l2) -> litNot l == l2) (fst pb)
then cutResolve pb pb3 (litVar l)
else pb
unassign solver (litVar l)
loop lits1' lits2' pb'
| otherwise = error "analyzeConflictHybrid: should not happen: reason of current level is empty"
where
sz = IS.size lits1
constrBumpActivity solver constr
conflictClause <- reasonOf solver constr Nothing
pbConfl <- toPBAtLeast solver constr
forM_ conflictClause $ \lit -> varBumpActivity solver (litVar lit)
(ys,zs) <- split conflictClause
(lits, pb) <- loop ys zs pbConfl
lits2 <- minimizeConflictClause solver lits
xs <- liftM (sortBy (flip (comparing snd))) $
forM (IS.toList lits2) $ \l -> do
lv <- litLevel solver l
return (l,lv)
let level = case xs of
[] -> error "analyzeConflict: should not happen"
[_] -> levelRoot
_:(_,lv):_ -> lv
return (map fst xs, level, pb)
pbBacktrackLevel :: Solver -> ([(Integer,Lit)],Integer) -> IO Level
pbBacktrackLevel _ ([], rhs) = assert (rhs > 0) $ return levelRoot
pbBacktrackLevel solver (lhs, rhs) = do
let go lvs lhs' s =
case IS.minView lvs of
Nothing -> error "pbBacktrackLevel: should not happen"
Just (lv2, lvs2) -> do
let s2 = s sum [c | (c,_,lv3) <- lhs', Just lv2 == lv3]
lhs2 = [x | x@(_,_,lv3) <- lhs', Just lv2 /= lv3]
if s2 < 0 then
return lv2
else if takeWhile (\(c,_,_) -> c > s) lhs2 /= [] then
return lv2 --unit
else
go lvs2 lhs2 s2
lhs' <- forM (sortBy (flip (comparing fst)) lhs) $ \(c, lit) -> do
v <- litValue solver lit
if v /= lFalse
then return (c, lit, Nothing)
else do
lv <- litLevel solver lit
return (c, lit, Just lv)
let lvs = IS.fromList [lv | (_,_,Just lv) <- lhs']
s0 = sum [c | (c,_) <- lhs] rhs
go lvs lhs' s0
minimizeConflictClause :: Solver -> LitSet -> IO LitSet
minimizeConflictClause solver lits = do
ccmin <- readIORef (svCCMin solver)
if ccmin >= 2 then
minimizeConflictClauseRecursive solver lits
else if ccmin >= 1 then
minimizeConflictClauseLocal solver lits
else
return lits
minimizeConflictClauseLocal :: Solver -> LitSet -> IO LitSet
minimizeConflictClauseLocal solver lits = do
let xs = IS.toAscList lits
ys <- filterM (liftM not . isRedundant) xs
when debugMode $ do
log solver "minimizeConflictClauseLocal:"
log solver $ show xs
log solver $ show ys
return $ IS.fromAscList $ ys
where
isRedundant :: Lit -> IO Bool
isRedundant lit = do
c <- varReason solver (litVar lit)
case c of
Nothing -> return False
Just c2 -> do
ls <- reasonOf solver c2 (Just (litNot lit))
allM test ls
test :: Lit -> IO Bool
test lit = do
lv <- litLevel solver lit
return $ lv == levelRoot || lit `IS.member` lits
minimizeConflictClauseRecursive :: Solver -> LitSet -> IO LitSet
minimizeConflictClauseRecursive solver lits = do
let
isRedundant :: Lit -> IO Bool
isRedundant lit = do
c <- varReason solver (litVar lit)
case c of
Nothing -> return False
Just c2 -> do
ls <- reasonOf solver c2 (Just (litNot lit))
go ls IS.empty
go :: [Lit] -> IS.IntSet -> IO Bool
go [] _ = return True
go (lit : ls) seen = do
lv <- litLevel solver lit
if lv == levelRoot || lit `IS.member` lits || lit `IS.member` seen
then go ls seen
else do
c <- varReason solver (litVar lit)
case c of
Nothing -> return False
Just c2 -> do
ls2 <- reasonOf solver c2 (Just (litNot lit))
go (ls2 ++ ls) (IS.insert lit seen)
let xs = IS.toAscList lits
ys <- filterM (liftM not . isRedundant) xs
when debugMode $ do
log solver "minimizeConflictClauseRecursive:"
log solver $ show xs
log solver $ show ys
return $ IS.fromAscList $ ys
popTrail :: Solver -> IO (Maybe Lit)
popTrail solver = do
m <- readIORef (svTrail solver)
case m of
[] -> return Nothing
l:ls -> do
writeIORef (svTrail solver) ls
return $ Just l
backtrackTo :: Solver -> Int -> IO ()
backtrackTo solver level = do
when debugMode $ log solver $ printf "backtrackTo: %d" level
writeIORef (svTrail solver) =<< loop =<< readIORef (svTrail solver)
SQ.clear (svBCPQueue solver)
writeIORef (svLevel solver) level
where
loop :: [Lit] -> IO [Lit]
loop [] = return []
loop lls@(l:ls) = do
lv <- litLevel solver l
if lv <= level
then return lls
else unassign solver (litVar l) >> loop ls
constructModel :: Solver -> IO ()
constructModel solver = do
n <- nVars solver
(marr::IOUArray Var Bool) <- newArray_ (1,n)
forM_ [1..n] $ \v -> do
vd <- varData solver v
a <- readIORef (vdAssignment vd)
writeArray marr v (aValue (fromJust a))
m <- unsafeFreeze marr
writeIORef (svModel solver) (Just m)
constrDecayActivity :: Solver -> IO ()
constrDecayActivity solver = do
d <- readIORef (svClaDecay solver)
modifyIORef' (svClaInc solver) (d*)
constrRescaleAllActivity :: Solver -> IO ()
constrRescaleAllActivity solver = do
xs <- learntConstraints solver
forM_ xs $ \c -> constrRescaleActivity solver c
modifyIORef' (svClaInc solver) (* 1e-20)
resetStat :: Solver -> IO ()
resetStat solver = do
writeIORef (svNDecision solver) 0
writeIORef (svNRandomDecision solver) 0
writeIORef (svNConflict solver) 0
writeIORef (svNRestart solver) 0
writeIORef (svNLearntGC solver) 0
printStatHeader :: Solver -> IO ()
printStatHeader solver = do
log solver $ "============================[ Search Statistics ]============================"
log solver $ " Time | Restart | Decision | Conflict | LEARNT | Fixed | Removed "
log solver $ " | | | | Limit GC | Var | Constra "
log solver $ "============================================================================="
printStat :: Solver -> Bool -> IO ()
printStat solver force = do
nowWC <- getCurrentTime
b <- if force
then return True
else do
lastWC <- readIORef (svLastStatWC solver)
return $ (nowWC `diffUTCTime` lastWC) > 1
when b $ do
startWC <- readIORef (svStartWC solver)
let tm = showTimeDiff $ nowWC `diffUTCTime` startWC
restart <- readIORef (svNRestart solver)
dec <- readIORef (svNDecision solver)
conflict <- readIORef (svNConflict solver)
learntLim <- readIORef (svLearntLim solver)
learntGC <- readIORef (svNLearntGC solver)
fixed <- readIORef (svNFixed solver)
removed <- readIORef (svNRemovedConstr solver)
log solver $ printf "%s | %7d | %8d | %8d | %8d %6d | %8d | %8d"
tm restart dec conflict learntLim learntGC fixed removed
writeIORef (svLastStatWC solver) nowWC
showTimeDiff :: NominalDiffTime -> String
showTimeDiff sec
| si < 100 = printf "%4.1fs" (fromRational s :: Double)
| si <= 9999 = printf "%4ds" si
| mi < 100 = printf "%4.1fm" (fromRational m :: Double)
| mi <= 9999 = printf "%4dm" mi
| hi < 100 = printf "%4.1fs" (fromRational h :: Double)
| otherwise = printf "%4dh" hi
where
s :: Rational
s = realToFrac sec
si :: Integer
si = round s
m :: Rational
m = s / 60
mi :: Integer
mi = round m
h :: Rational
h = m / 60
hi :: Integer
hi = round h
class Constraint a where
toConstraint :: a -> SomeConstraint
showConstraint :: Solver -> a -> IO String
attach :: Solver -> a -> IO ()
watchedLiterals :: Solver -> a -> IO [Lit]
basicPropagate :: Solver -> SomeConstraint -> a -> Lit -> IO Bool
basicReasonOf :: Solver -> a -> Maybe Lit -> IO Clause
toPBAtLeast :: Solver -> a -> IO ([(Integer,Lit)], Integer)
isSatisfied :: Solver -> a -> IO Bool
constrIsProtected :: Solver -> a -> IO Bool
constrIsProtected _ _ = return False
constrActivity :: Solver -> a -> IO Double
constrBumpActivity :: Solver -> a -> IO ()
constrBumpActivity _ _ = return ()
constrRescaleActivity :: Solver -> a -> IO ()
constrRescaleActivity _ _ = return ()
detach :: Constraint a => Solver -> a -> IO ()
detach solver c = do
let c2 = toConstraint c
lits <- watchedLiterals solver c
forM_ lits $ \lit -> do
ld <- litData solver lit
modifyIORef' (ldWatches ld) (delete c2)
propagate :: Solver -> SomeConstraint -> Lit -> IO Bool
propagate solver c l = basicPropagate solver c c l
reasonOf :: Constraint a => Solver -> a -> Maybe Lit -> IO Clause
reasonOf solver c x = do
when debugMode $
case x of
Nothing -> return ()
Just lit -> do
val <- litValue solver lit
unless (lTrue == val) $ do
str <- showConstraint solver c
error (printf "reasonOf: value of literal %d should be True but %s (basicReasonOf %s %s)" lit (show val) str (show x))
cl <- basicReasonOf solver c x
when debugMode $ do
forM_ cl $ \lit -> do
val <- litValue solver lit
unless (lFalse == val) $ do
str <- showConstraint solver c
error (printf "reasonOf: value of literal %d should be False but %s (basicReasonOf %s %s)" lit (show val) str (show x))
return cl
isLocked :: Solver -> SomeConstraint -> IO Bool
isLocked solver c = anyM p =<< watchedLiterals solver c
where
p :: Lit -> IO Bool
p lit = do
val <- litValue solver lit
if val /= lTrue
then return False
else do
m <- varReason solver (litVar lit)
case m of
Nothing -> return False
Just c2 -> return $! c == c2
data SomeConstraint
= ConstrClause !ClauseData
| ConstrAtLeast !AtLeastData
| ConstrPBAtLeast !PBAtLeastData
deriving Eq
instance Constraint SomeConstraint where
toConstraint = id
showConstraint s (ConstrClause c) = showConstraint s c
showConstraint s (ConstrAtLeast c) = showConstraint s c
showConstraint s (ConstrPBAtLeast c) = showConstraint s c
attach s (ConstrClause c) = attach s c
attach s (ConstrAtLeast c) = attach s c
attach s (ConstrPBAtLeast c) = attach s c
watchedLiterals s (ConstrClause c) = watchedLiterals s c
watchedLiterals s (ConstrAtLeast c) = watchedLiterals s c
watchedLiterals s (ConstrPBAtLeast c) = watchedLiterals s c
basicPropagate s this (ConstrClause c) lit = basicPropagate s this c lit
basicPropagate s this (ConstrAtLeast c) lit = basicPropagate s this c lit
basicPropagate s this (ConstrPBAtLeast c) lit = basicPropagate s this c lit
basicReasonOf s (ConstrClause c) l = basicReasonOf s c l
basicReasonOf s (ConstrAtLeast c) l = basicReasonOf s c l
basicReasonOf s (ConstrPBAtLeast c) l = basicReasonOf s c l
toPBAtLeast s (ConstrClause c) = toPBAtLeast s c
toPBAtLeast s (ConstrAtLeast c) = toPBAtLeast s c
toPBAtLeast s (ConstrPBAtLeast c) = toPBAtLeast s c
isSatisfied s (ConstrClause c) = isSatisfied s c
isSatisfied s (ConstrAtLeast c) = isSatisfied s c
isSatisfied s (ConstrPBAtLeast c) = isSatisfied s c
constrIsProtected s (ConstrClause c) = constrIsProtected s c
constrIsProtected s (ConstrAtLeast c) = constrIsProtected s c
constrIsProtected s (ConstrPBAtLeast c) = constrIsProtected s c
constrActivity s (ConstrClause c) = constrActivity s c
constrActivity s (ConstrAtLeast c) = constrActivity s c
constrActivity s (ConstrPBAtLeast c) = constrActivity s c
constrBumpActivity s (ConstrClause c) = constrBumpActivity s c
constrBumpActivity s (ConstrAtLeast c) = constrBumpActivity s c
constrBumpActivity s (ConstrPBAtLeast c) = constrBumpActivity s c
constrRescaleActivity s (ConstrClause c) = constrRescaleActivity s c
constrRescaleActivity s (ConstrAtLeast c) = constrRescaleActivity s c
constrRescaleActivity s (ConstrPBAtLeast c) = constrRescaleActivity s c
data ClauseData
= ClauseData
{ claLits :: !(IOUArray Int Lit)
, claActivity :: !(IORef Double)
}
instance Eq ClauseData where
c1 == c2 = claActivity c1 == claActivity c2
newClauseData :: Clause -> Bool -> IO ClauseData
newClauseData ls learnt = do
let size = length ls
a <- newListArray (0, size1) ls
act <- newIORef $! (if learnt then 0 else 1)
return (ClauseData a act)
instance Constraint ClauseData where
toConstraint = ConstrClause
showConstraint _ this = do
lits <- getElems (claLits this)
return (show lits)
attach solver this = do
lits <- getElems (claLits this)
case lits of
l1:l2:_ -> do
watch solver l1 this
watch solver l2 this
_ -> return ()
watchedLiterals _ this = do
lits <- getElems (claLits this)
case lits of
l1:l2:_ -> return [l1, l2]
_ -> return []
basicPropagate !s this this2 !falsifiedLit = do
preprocess
!lit0 <- unsafeRead a 0
!val0 <- litValue s lit0
if val0 == lTrue
then do
watch s falsifiedLit this
return True
else do
(!lb,!ub) <- getBounds a
assert (lb==0) $ return ()
i <- findForWatch 2 ub
case i of
1 -> do
when debugMode $ logIO s $ do
str <- showConstraint s this
return $ printf "basicPropagate: %s is unit" str
watch s falsifiedLit this
assignBy s lit0 this
_ -> do
!lit1 <- unsafeRead a 1
!liti <- unsafeRead a i
unsafeWrite a 1 liti
unsafeWrite a i lit1
watch s liti this
return True
where
a = claLits this2
preprocess :: IO ()
preprocess = do
!l0 <- unsafeRead a 0
!l1 <- unsafeRead a 1
assert (l0==falsifiedLit || l1==falsifiedLit) $ return ()
when (l0==falsifiedLit) $ do
unsafeWrite a 0 l1
unsafeWrite a 1 l0
findForWatch :: Int -> Int -> IO Int
findForWatch i end | i > end = return (1)
findForWatch i end = do
val <- litValue s =<< unsafeRead a i
if val /= lFalse
then return i
else findForWatch (i+1) end
basicReasonOf _ this l = do
lits <- getElems (claLits this)
case l of
Nothing -> return lits
Just lit -> do
assert (lit == head lits) $ return ()
return $ tail lits
toPBAtLeast _ (ClauseData a _) = do
lits <- getElems a
return ([(1,l) | l <- lits], 1)
isSatisfied solver this = do
lits <- getElems (claLits this)
vals <- mapM (litValue solver) lits
return $ lTrue `elem` vals
constrIsProtected _ this = do
size <- liftM rangeSize (getBounds (claLits this))
return $! size <= 2
constrActivity _ this = do
let act = claActivity this
readIORef act
constrBumpActivity solver this = do
let act = claActivity this
aval <- readIORef act
when (aval >= 0) $ do
inc <- readIORef (svClaInc solver)
let aval2 = aval+inc
writeIORef act $! aval2
when (aval2 > 1e20) $
constrRescaleAllActivity solver
constrRescaleActivity _ this = do
let act = claActivity this
aval <- readIORef act
when (aval >= 0) $ writeIORef act $! (aval * 1e-20)
instantiateClause :: Solver -> Clause -> IO (Maybe Clause)
instantiateClause solver = loop []
where
loop :: [Lit] -> [Lit] -> IO (Maybe Clause)
loop ret [] = return $ Just ret
loop ret (l:ls) = do
val <- litValue solver l
if val==lTrue then
return Nothing
else if val==lFalse then
loop ret ls
else
loop (l : ret) ls
data AtLeastData
= AtLeastData
{ atLeastLits :: IOUArray Int Lit
, atLeastNum :: !Int
, atLeastActivity :: !(IORef Double)
}
deriving Eq
newAtLeastData :: [Lit] -> Int -> Bool -> IO AtLeastData
newAtLeastData ls n learnt = do
let size = length ls
a <- newListArray (0, size1) ls
act <- newIORef $! (if learnt then 0 else 1)
return (AtLeastData a n act)
instance Constraint AtLeastData where
toConstraint = ConstrAtLeast
showConstraint _ this = do
lits <- getElems (atLeastLits this)
return $ show lits ++ " >= " ++ show (atLeastNum this)
attach solver this = do
lits <- getElems (atLeastLits this)
let n = atLeastNum this
let ws = if length lits > n then take (n+1) lits else []
forM_ ws $ \l -> watch solver l this
watchedLiterals _ this = do
lits <- getElems (atLeastLits this)
let n = atLeastNum this
let ws = if length lits > n then take (n+1) lits else []
return ws
basicPropagate s this this2 falsifiedLit = do
preprocess
when debugMode $ do
litn <- readArray a n
unless (litn == falsifiedLit) $ error "AtLeastData.basicPropagate: should not happen"
(lb,ub) <- getBounds a
assert (lb==0) $ return ()
ret <- findForWatch (n+1) ub
case ret of
Nothing -> do
when debugMode $ logIO s $ do
str <- showConstraint s this
return $ printf "basicPropagate: %s is unit" str
watch s falsifiedLit this
let loop :: Int -> IO Bool
loop i
| i >= n = return True
| otherwise = do
liti <- readArray a i
ret2 <- assignBy s liti this
if ret2
then loop (i+1)
else return False
loop 0
Just i -> do
liti <- readArray a i
litn <- readArray a n
writeArray a i litn
writeArray a n liti
watch s liti this
return True
where
a = atLeastLits this2
n = atLeastNum this2
preprocess :: IO ()
preprocess = loop 0
where
loop :: Int -> IO ()
loop i
| i >= n = return ()
| otherwise = do
li <- readArray a i
if (li /= falsifiedLit)
then loop (i+1)
else do
ln <- readArray a n
writeArray a n li
writeArray a i ln
findForWatch :: Int -> Int -> IO (Maybe Int)
findForWatch i end | i > end = return Nothing
findForWatch i end = do
val <- litValue s =<< readArray a i
if val /= lFalse
then return (Just i)
else findForWatch (i+1) end
basicReasonOf s this concl = do
lits <- getElems (atLeastLits this)
let n = atLeastNum this
case concl of
Nothing -> do
let f :: [Lit] -> IO Lit
f [] = error "AtLeastData.basicReasonOf: should not happen"
f (l:ls) = do
val <- litValue s l
if val == lFalse
then return l
else f ls
lit <- f (take n lits)
return $ lit : drop n lits
Just lit -> do
assert (lit `elem` take n lits) $ return ()
return $ drop n lits
toPBAtLeast _ this = do
lits <- getElems (atLeastLits this)
return ([(1,l) | l <- lits], fromIntegral (atLeastNum this))
isSatisfied solver this = do
lits <- getElems (atLeastLits this)
vals <- mapM (litValue solver) lits
return $ length [v | v <- vals, v == lTrue] >= atLeastNum this
constrActivity _ this = do
let act = atLeastActivity this
readIORef act
constrBumpActivity solver this = do
let act = atLeastActivity this
aval <- readIORef act
when (aval >= 0) $ do
inc <- readIORef (svClaInc solver)
let aval2 = aval+inc
writeIORef act $! aval2
when (aval2 > 1e20) $
constrRescaleAllActivity solver
constrRescaleActivity _ this = do
let act = atLeastActivity this
aval <- readIORef act
when (aval >= 0) $ writeIORef act $! (aval * 1e-20)
instantiateAtLeast :: Solver -> ([Lit],Int) -> IO ([Lit],Int)
instantiateAtLeast solver (xs,n) = loop ([],n) xs
where
loop :: ([Lit],Int) -> [Lit] -> IO ([Lit],Int)
loop ret [] = return ret
loop (ys,m) (l:ls) = do
val <- litValue solver l
if val == lTrue then
loop (ys, m1) ls
else if val == lFalse then
loop (ys, m) ls
else
loop (l:ys, m) ls
data PBAtLeastData
= PBAtLeastData
{ pbTerms :: !(LitMap Integer)
, pbDegree :: !Integer
, pbSlack :: !(IORef Integer)
, pbActivity :: !(IORef Double)
, pbReasons :: !(IORef (LitMap [(Lit, Integer)]))
}
deriving Eq
newPBAtLeastData :: [(Integer,Lit)] -> Integer -> Bool -> IO PBAtLeastData
newPBAtLeastData ts degree learnt = do
let slack = sum (map fst ts) degree
m = IM.fromList [(l,c) | (c,l) <- ts]
s <- newIORef slack
act <- newIORef $! (if learnt then 0 else 1)
rs <- newIORef IM.empty
return (PBAtLeastData m degree s act rs)
instance Constraint PBAtLeastData where
toConstraint = ConstrPBAtLeast
showConstraint _ this = do
return $ show [(c,l) | (l,c) <- IM.toList (pbTerms this)] ++ " >= " ++ show (pbDegree this)
attach solver this = do
forM_ (IM.keys (pbTerms this)) $ \l -> watch solver l this
cs <- forM (IM.toList (pbTerms this)) $ \(l,c) -> do
v <- litValue solver l
if v == lFalse
then do
addBacktrackCB solver (litVar l) $ modifyIORef' (pbSlack this) (+ c)
return 0
else return c
writeIORef (pbSlack this) $! sum cs pbDegree this
watchedLiterals _ this = do
return $ IM.keys $ pbTerms this
basicPropagate solver this this2 falsifiedLit = do
watch solver falsifiedLit this
let c = pbTerms this2 IM.! falsifiedLit
let slack = pbSlack this2
modifyIORef' slack (subtract c)
addBacktrackCB solver (litVar falsifiedLit) $ modifyIORef' slack (+ c)
pbPropagate solver this2
basicReasonOf solver this l = do
let m = pbTerms this
xs <-
case l of
Just lit -> do
rs <- readIORef (pbReasons this)
return $ sortBy (flip (comparing snd)) $ (rs IM.! lit)
Nothing -> do
tmp <- filterM (\(lit,_) -> liftM (lFalse ==) (litValue solver lit)) (IM.toList m)
return $ sortBy (flip (comparing snd)) $ tmp
let max_slack = sum (map snd $ IM.toList m) pbDegree this
case l of
Nothing -> return $ f max_slack xs
Just lit -> return $ f (max_slack (m IM.! lit)) xs
where
f :: Integer -> [(Lit,Integer)] -> [Lit]
f s xs = go s xs []
go :: Integer -> [(Lit,Integer)] -> [Lit] -> [Lit]
go s _ ret | s < 0 = ret
go _ [] _ = error "PBAtLeastData.basicReasonOf: should not happen"
go s ((lit,c):xs) ret = go (s c) xs (lit:ret)
toPBAtLeast _ this = do
return ([(c,l) | (l,c) <- IM.toList (pbTerms this)], pbDegree this)
isSatisfied solver this = do
xs <- forM (IM.toList (pbTerms this)) $ \(l,c) -> do
v <- litValue solver l
if v == lTrue
then return c
else return 0
return $ sum xs >= pbDegree this
constrActivity _ this = do
let act = pbActivity this
readIORef act
constrBumpActivity solver this = do
let act = pbActivity this
aval <- readIORef act
when (aval >= 0) $ do
inc <- readIORef (svClaInc solver)
let aval2 = aval+inc
writeIORef act $! aval2
when (aval2 > 1e20) $
constrRescaleAllActivity solver
constrRescaleActivity _ this = do
let act = pbActivity this
aval <- readIORef act
when (aval >= 0) $ writeIORef act $! (aval * 1e-20)
instantiatePB :: Solver -> ([(Integer,Lit)],Integer) -> IO ([(Integer,Lit)],Integer)
instantiatePB solver (xs,n) = loop ([],n) xs
where
loop :: ([(Integer,Lit)],Integer) -> [(Integer,Lit)] -> IO ([(Integer,Lit)],Integer)
loop ret [] = return ret
loop (ys,m) ((c,l):ts) = do
val <- litValue solver l
if val == lTrue then
loop (ys, mc) ts
else if val == lFalse then
loop (ys, m) ts
else
loop ((c,l):ys, m) ts
pbPropagate :: Solver -> PBAtLeastData -> IO Bool
pbPropagate solver this = do
let slack = pbSlack this
s <- readIORef slack
if s < 0
then return False
else do
ref <- newIORef Nothing
let m = do
x <- readIORef ref
case x of
Just r -> return r
Nothing -> do
let isFalse (l,_) = liftM (lFalse==) (litValue solver l)
r <- filterM isFalse $ IM.toAscList $ pbTerms this
writeIORef ref (Just r)
return r
forM_ (IM.toList (pbTerms this)) $ \(l1,c1) -> do
when (c1 > s) $ do
v <- litValue solver l1
when (v == lUndef) $ do
r <- m
modifyIORef (pbReasons this) (IM.insert l1 r)
assignBy solver l1 this
constrBumpActivity solver this
return ()
return True
pbOverSAT :: Solver -> ([(Integer,Lit)],Integer) -> IO Bool
pbOverSAT solver (lhs, rhs) = do
ss <- forM lhs $ \(c,l) -> do
v <- litValue solver l
if v /= lFalse
then return c
else return 0
return $! sum ss > rhs
data RestartStrategy = MiniSATRestarts | ArminRestarts | LubyRestarts
deriving (Show, Eq, Ord)
mkRestartSeq :: RestartStrategy -> Int -> Double -> [Int]
mkRestartSeq MiniSATRestarts = miniSatRestartSeq
mkRestartSeq ArminRestarts = arminRestartSeq
mkRestartSeq LubyRestarts = lubyRestartSeq
miniSatRestartSeq :: Int -> Double -> [Int]
miniSatRestartSeq start inc = iterate (ceiling . (inc *) . fromIntegral) start
arminRestartSeq :: Int -> Double -> [Int]
arminRestartSeq start inc = go (fromIntegral start) (fromIntegral start)
where
go !inner !outer = round inner : go inner' outer'
where
(inner',outer') =
if inner >= outer
then (fromIntegral start, outer * inc)
else (inner * inc, outer)
lubyRestartSeq :: Int -> Double -> [Int]
lubyRestartSeq start inc = map (ceiling . (fromIntegral start *) . luby inc) [0..]
luby :: Double -> Integer -> Double
luby y x = go2 size1 sequ1 x
where
(size1, sequ1) = go 1 0
go :: Integer -> Integer -> (Integer, Integer)
go size sequ
| size < x+1 = go (2*size+1) (sequ+1)
| otherwise = (size, sequ)
go2 :: Integer -> Integer -> Integer -> Double
go2 size sequ x2
| size1 /= x2 = let size' = (size1) `div` 2 in go2 size' (sequ 1) (x2 `mod` size')
| otherwise = y ^ sequ
allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
allM p = go
where
go [] = return True
go (x:xs) = do
b <- p x
if b
then go xs
else return False
anyM :: Monad m => (a -> m Bool) -> [a] -> m Bool
anyM p = go
where
go [] = return False
go (x:xs) = do
b <- p x
if b
then return True
else go xs
#if !MIN_VERSION_base(4,6,0)
modifyIORef' :: IORef a -> (a -> a) -> IO ()
modifyIORef' ref f = do
x <- readIORef ref
writeIORef ref $! f x
#endif
shift :: IORef [a] -> IO a
shift ref = do
(x:xs) <- readIORef ref
writeIORef ref xs
return x
debugMode :: Bool
debugMode = False
checkSatisfied :: Solver -> IO ()
checkSatisfied solver = do
cls <- readIORef (svClauseDB solver)
forM_ cls $ \c -> do
b <- isSatisfied solver c
unless b $ do
s <- showConstraint solver c
log solver $ "BUG: " ++ s ++ " is violated"
sanityCheck :: Solver -> IO ()
sanityCheck _ | not debugMode = return ()
sanityCheck solver = do
cls <- readIORef (svClauseDB solver)
forM_ cls $ \constr -> do
lits <- watchedLiterals solver constr
forM_ lits $ \l -> do
ws <- watches solver l
unless (constr `elem` ws) $ error $ printf "sanityCheck:A:%s" (show lits)
vs <- variables solver
let lits = [l | v <- vs, l <- [literal v True, literal v False]]
forM_ lits $ \l -> do
cs <- watches solver l
forM_ cs $ \constr -> do
lits2 <- watchedLiterals solver constr
unless (l `elem` lits2) $ do
error $ printf "sanityCheck:C:%d %s" l (show lits2)
dumpVarActivity :: Solver -> IO ()
dumpVarActivity solver = do
log solver "Variable activity:"
vs <- variables solver
forM_ vs $ \v -> do
activity <- varActivity solver v
log solver $ printf "activity(%d) = %d" v activity
dumpClaActivity :: Solver -> IO ()
dumpClaActivity solver = do
log solver "Learnt clause activity:"
xs <- learntConstraints solver
forM_ xs $ \c -> do
s <- showConstraint solver c
aval <- constrActivity solver c
log solver $ printf "activity(%s) = %f" s aval
setLogger :: Solver -> (String -> IO ()) -> IO ()
setLogger solver logger = do
writeIORef (svLogger solver) (Just logger)
log :: Solver -> String -> IO ()
log solver msg = logIO solver (return msg)
logIO :: Solver -> IO String -> IO ()
logIO solver action = do
m <- readIORef (svLogger solver)
case m of
Nothing -> return ()
Just logger -> action >>= logger