{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.SAT.PBO.UnsatBased
( solve
) where
import Control.Monad
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.PBO.Context as C
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 }
let sels0 :: [(Lit, Integer)]
sels0 = [(-Lit
v, Integer
c) | (Integer
c,Lit
v) <- forall a. Context a => a -> PBLinSum
C.getObjectiveFunction cxt
cxt]
Integer -> LitMap Integer -> IO ()
loop Integer
0 (forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit, Integer)]
sels0)
where
loop :: Integer -> SAT.LitMap Integer -> IO ()
loop :: Integer -> LitMap Integer -> IO ()
loop !Integer
lb LitMap Integer
sels = do
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
lb
Bool
ret <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (forall a. IntMap a -> [Lit]
IntMap.keys LitMap Integer
sels)
if Bool
ret then do
Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else do
LitSet
core <- Solver -> IO LitSet
SAT.getFailedAssumptions Solver
solver
if LitSet -> Bool
IntSet.null LitSet
core then
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
else do
let !min_c :: Integer
min_c = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys LitMap Integer
sels LitSet
core
!lb' :: Integer
lb' = Integer
lb forall a. Num a => a -> a -> a
+ Integer
min_c
[(Lit, Lit)]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (LitSet -> [Lit]
IntSet.toList LitSet
core) forall a b. (a -> b) -> a -> b
$ \Lit
sel -> do
Lit
r <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, Lit
r)
forall (m :: * -> *) a.
AddCardinality m a =>
a -> [Lit] -> Lit -> m ()
SAT.addExactly Solver
solver (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Lit, Lit)]
xs) Lit
1
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
l | Lit
l <- LitSet -> [Lit]
IntSet.toList LitSet
core]
LitMap Integer
ys <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IntMap.unions forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Lit, Lit)]
xs forall a b. (a -> b) -> a -> b
$ \(Lit
sel, Lit
r) -> do
Lit
sel' <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
sel', Lit
r, Lit
sel]
let c :: Integer
c = LitMap Integer
sels forall a. IntMap a -> Lit -> a
IntMap.! Lit
sel
if Integer
c forall a. Ord a => a -> a -> Bool
> Integer
min_c
then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit
sel', Integer
min_c), (Lit
sel, Integer
c forall a. Num a => a -> a -> a
- Integer
min_c)]
else forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Lit -> a -> IntMap a
IntMap.singleton Lit
sel' Integer
min_c
let sels' :: LitMap Integer
sels' = forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union LitMap Integer
ys (forall a. IntMap a -> LitSet -> IntMap a
IntMap.withoutKeys LitMap Integer
sels LitSet
core)
Integer -> LitMap Integer -> IO ()
loop Integer
lb' LitMap Integer
sels'