{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
module ToySolver.SAT.PBO.MSU4
( solve
) where
import Control.Concurrent.STM
import Control.Monad
import qualified Data.IntSet as IS
import qualified Data.IntMap as IM
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.PBO.Context as C
import Text.Printf
solve :: C.Context cxt => cxt -> SAT.Solver -> IO ()
solve :: forall cxt. Context cxt => cxt -> Solver -> IO ()
solve cxt
cxt Solver
solver = forall cxt. Context cxt => cxt -> Solver -> IO ()
solveWBO (forall a. Context a => a -> Normalized a
C.normalize cxt
cxt) Solver
solver
solveWBO :: C.Context cxt => cxt -> SAT.Solver -> IO ()
solveWBO :: forall cxt. Context cxt => cxt -> Solver -> IO ()
solveWBO cxt
cxt Solver
solver = do
Solver -> (Config -> Config) -> IO ()
SAT.modifyConfig Solver
solver forall a b. (a -> b) -> a -> b
$ \Config
config -> Config
config{ configEnableBackwardSubsumptionRemoval :: Bool
SAT.configEnableBackwardSubsumptionRemoval = Bool
True }
(LitSet, LitSet) -> Integer -> IO ()
loop (forall a. IntMap a -> LitSet
IM.keysSet LitMap Integer
weights, LitSet
IS.empty) Integer
0
where
obj :: SAT.PBLinSum
obj :: PBLinSum
obj = forall a. Context a => a -> PBLinSum
C.getObjectiveFunction cxt
cxt
sels :: [(SAT.Lit, Integer)]
sels :: [(Lit, Integer)]
sels = [(-Lit
lit, Integer
w) | (Integer
w,Lit
lit) <- PBLinSum
obj]
weights :: SAT.LitMap Integer
weights :: LitMap Integer
weights = forall a. [(Lit, a)] -> IntMap a
IM.fromList [(Lit, Integer)]
sels
loop :: (SAT.LitSet, SAT.LitSet) -> Integer -> IO ()
loop :: (LitSet, LitSet) -> Integer -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) Integer
lb = do
Bool
ret <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (LitSet -> [Lit]
IS.toList LitSet
unrelaxed)
if Bool
ret then do
Model
currModel <- Solver -> IO Model
SAT.getModel Solver
solver
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
currModel
let violated :: [Integer]
violated = [LitMap Integer
weights forall a. IntMap a -> Lit -> a
IM.! Lit
l | Lit
l <- LitSet -> [Lit]
IS.toList LitSet
relaxed, forall m. IModel m => m -> Lit -> Bool
SAT.evalLit Model
currModel Lit
l forall a. Eq a => a -> a -> Bool
== Bool
False]
currVal :: Integer
currVal = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer]
violated
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver [(Integer
c,-Lit
l) | (Lit
l,Integer
c) <- [(Lit, Integer)]
sels] (Integer
currVal forall a. Num a => a -> a -> a
- Integer
1)
(LitSet, LitSet) -> Integer -> IO ()
cont (LitSet
unrelaxed, LitSet
relaxed) Integer
lb
else do
LitSet
core <- Solver -> IO LitSet
SAT.getFailedAssumptions Solver
solver
let ls :: LitSet
ls = LitSet
core LitSet -> LitSet -> LitSet
`IS.intersection` LitSet
unrelaxed
if LitSet -> Bool
IS.null LitSet
ls then do
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
else do
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
l | Lit
l <- LitSet -> [Lit]
IS.toList LitSet
core]
let min_weight :: Integer
min_weight = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [LitMap Integer
weights forall a. IntMap a -> Lit -> a
IM.! Lit
l | Lit
l <- LitSet -> [Lit]
IS.toList LitSet
ls]
lb' :: Integer
lb' = Integer
lb forall a. Num a => a -> a -> a
+ Integer
min_weight
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"MSU4: found a core: size = %d, minimal weight = %d" (LitSet -> Lit
IS.size LitSet
core) Integer
min_weight
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
lb'
(LitSet, LitSet) -> Integer -> IO ()
cont (LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IS.difference` LitSet
ls, LitSet
relaxed LitSet -> LitSet -> LitSet
`IS.union` LitSet
ls) Integer
lb'
cont :: (SAT.LitSet, SAT.LitSet) -> Integer -> IO ()
cont :: (LitSet, LitSet) -> Integer -> IO ()
cont (LitSet
unrelaxed, LitSet
relaxed) Integer
lb = do
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
Bool
b <- forall a. Context a => a -> STM Bool
C.isFinished cxt
cxt
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
b then forall (m :: * -> *) a. Monad m => a -> m a
return () else (LitSet, LitSet) -> Integer -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) Integer
lb