module SAT.PBO.MSU4
( Options (..)
, defaultOptions
, solve
, solveWBO
) where
import qualified Data.IntSet as IS
import qualified Data.IntMap as IM
import qualified SAT as SAT
import SAT.Types
import Text.Printf
data Options
= Options
{ optLogger :: String -> IO ()
, optUpdateBest :: SAT.Model -> Integer -> IO ()
, optUpdateLB :: Integer -> IO ()
}
defaultOptions :: Options
defaultOptions
= Options
{ optLogger = \_ -> return ()
, optUpdateBest = \_ _ -> return ()
, optUpdateLB = \_ -> return ()
}
solve :: SAT.Solver -> [(Integer, SAT.Lit)] -> Options -> IO (Maybe SAT.Model)
solve solver obj opt = do
result <- solveWBO solver [(v, c) | (c,v) <- obj'] opt'
case result of
Nothing -> return Nothing
Just (m,_) -> return (Just m)
where
(obj',offset) = normalizePBSum (obj,0)
opt' =
opt
{ optUpdateBest = \m val -> optUpdateBest opt m (offset + val)
, optUpdateLB = \val -> optUpdateLB opt (offset + val)
}
solveWBO :: SAT.Solver -> [(Lit, Integer)] -> Options -> IO (Maybe (SAT.Model, Integer))
solveWBO solver sels opt = do
optUpdateLB opt 0
loop (IM.keysSet weights) IS.empty 0 Nothing
where
weights = IM.fromList sels
loop :: IS.IntSet -> IS.IntSet -> Integer -> Maybe (SAT.Model, Integer) -> IO (Maybe (SAT.Model, Integer))
loop unrelaxed relaxed lb best = do
ret <- SAT.solveWith solver (IS.toList unrelaxed)
if ret then do
currModel <- SAT.model solver
let violated = [weights IM.! l | l <- IS.toList relaxed, evalLit currModel l == False]
currVal = sum violated
best' <-
case best of
Just (_, bestVal)
| currVal < bestVal -> do
optUpdateBest opt currModel currVal
return $ Just (currModel, currVal)
| otherwise -> do
return best
Nothing -> do
optUpdateBest opt currModel currVal
return $ Just (currModel, currVal)
SAT.addPBAtMost solver [(c,l) | (l,c) <- sels] (currVal 1)
cont unrelaxed relaxed lb best'
else do
core <- SAT.failedAssumptions solver
let ls = IS.fromList core `IS.intersection` unrelaxed
if IS.null ls then do
return best
else do
SAT.addClause solver [l | l <- core]
let min_weight = minimum [weights IM.! l | l <- IS.toList ls]
lb' = lb + min_weight
optLogger opt $ printf "MSU4: found a core: size = %d, minimal weight = %d" (length core) min_weight
optUpdateLB opt lb'
cont (unrelaxed `IS.difference` ls) (relaxed `IS.union` ls) lb' best
cont :: IS.IntSet -> IS.IntSet -> Integer -> Maybe (SAT.Model, Integer) -> IO (Maybe (SAT.Model, Integer))
cont _ _ lb best@(Just (_, bestVal)) | lb == bestVal = return best
cont unrelaxed relaxed lb best = loop unrelaxed relaxed lb best