{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO.BCD2
-- Copyright   :  (c) Masahiro Sakai 2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Reference:
--
-- * Federico Heras, Antonio Morgado, João Marques-Silva,
--   Core-Guided binary search algorithms for maximum satisfiability,
--   Twenty-Fifth AAAI Conference on Artificial Intelligence, 2011.
--   <http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3713>
--
-- * A. Morgado, F. Heras, and J. Marques-Silva,
--   Improvements to Core-Guided binary search for MaxSAT,
--   in Theory and Applications of Satisfiability Testing (SAT 2012),
--   pp. 284-297.
--   <https://doi.org/10.1007/978-3-642-31612-8_22>
--   <http://ulir.ul.ie/handle/10344/2771>
--
-----------------------------------------------------------------------------
module ToySolver.SAT.PBO.BCD2
  ( Options (..)
  , solve
  ) where

import Control.Concurrent.STM
import Control.Monad
import Data.IORef
import Data.Default.Class
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Vector as V
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.PBO.Context as C
import qualified ToySolver.Combinatorial.SubsetSum as SubsetSum
import Text.Printf

-- | Options for BCD2 algorithm.
--
-- The default value can be obtained by 'def'.
data Options
  = Options
  { Options -> Bool
optEnableHardening :: Bool
  , Options -> Bool
optEnableBiasedSearch :: Bool
  , Options -> Bool
optSolvingNormalFirst :: Bool
  }

instance Default Options where
  def :: Options
def =
    Options
    { optEnableHardening :: Bool
optEnableHardening = Bool
True
    , optEnableBiasedSearch :: Bool
optEnableBiasedSearch = Bool
True
    , optSolvingNormalFirst :: Bool
optSolvingNormalFirst = Bool
True
    }

data CoreInfo
  = CoreInfo
  { CoreInfo -> LitSet
coreLits :: SAT.LitSet
  , CoreInfo -> IORef Integer
coreLBRef :: !(IORef Integer)
  , CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors :: !(IORef (Map Integer SAT.Lit))
  }

newCoreInfo :: SAT.LitSet -> Integer -> IO CoreInfo
newCoreInfo :: LitSet -> Integer -> IO CoreInfo
newCoreInfo LitSet
lits Integer
lb = do
  IORef Integer
lbRef <- forall a. a -> IO (IORef a)
newIORef Integer
lb
  IORef (Map Integer Lit)
selsRef <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty
  forall (m :: * -> *) a. Monad m => a -> m a
return
    CoreInfo
    { coreLits :: LitSet
coreLits = LitSet
lits
    , coreLBRef :: IORef Integer
coreLBRef = IORef Integer
lbRef
    , coreUBSelectors :: IORef (Map Integer Lit)
coreUBSelectors = IORef (Map Integer Lit)
selsRef
    }

deleteCoreInfo :: SAT.Solver -> CoreInfo -> IO ()
deleteCoreInfo :: Solver -> CoreInfo -> IO ()
deleteCoreInfo Solver
solver CoreInfo
core = do
  Map Integer Lit
m <- forall a. IORef a -> IO a
readIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core)
  -- Delete soft upperbound constraints by fixing selector variables
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [a]
Map.elems Map Integer Lit
m) forall a b. (a -> b) -> a -> b
$ \Lit
sel ->
    forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [-Lit
sel]

getCoreLB :: CoreInfo -> IO Integer
getCoreLB :: CoreInfo -> IO Integer
getCoreLB = forall a. IORef a -> IO a
readIORef forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreInfo -> IORef Integer
coreLBRef

solve :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
solve :: forall cxt. Context cxt => cxt -> Solver -> Options -> IO ()
solve cxt
cxt Solver
solver Options
opt = forall cxt. Context cxt => cxt -> Solver -> Options -> IO ()
solveWBO (forall a. Context a => a -> Normalized a
C.normalize cxt
cxt) Solver
solver Options
opt

solveWBO :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
solveWBO :: forall cxt. Context cxt => cxt -> Solver -> Options -> IO ()
solveWBO cxt
cxt Solver
solver Options
opt = do
  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
"BCD2: Hardening is %s." (if Options -> Bool
optEnableHardening Options
opt then String
"enabled" else String
"disabled")
  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
"BCD2: BiasedSearch is %s." (if Options -> Bool
optEnableBiasedSearch Options
opt then String
"enabled" else String
"disabled")

  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 }

  IORef LitSet
unrelaxedRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ Clause -> LitSet
IntSet.fromList [Lit
lit | (Lit
lit,Integer
_) <- [(Lit, Integer)]
sels]
  IORef LitSet
relaxedRef   <- forall a. a -> IO (IORef a)
newIORef LitSet
IntSet.empty
  IORef LitSet
hardenedRef  <- forall a. a -> IO (IORef a)
newIORef LitSet
IntSet.empty
  IORef Integer
nsatRef   <- forall a. a -> IO (IORef a)
newIORef Integer
1
  IORef Integer
nunsatRef <- forall a. a -> IO (IORef a)
newIORef Integer
1

  IORef Integer
lastUBRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ PBLinSum -> Integer
SAT.pbLinUpperBound PBLinSum
obj

  IORef [CoreInfo]
coresRef <- forall a. a -> IO (IORef a)
newIORef []
  let getLB :: IO Integer
getLB = do
        [CoreInfo]
xs <- forall a. IORef a -> IO a
readIORef IORef [CoreInfo]
coresRef
        forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Integer
s CoreInfo
core -> do{ Integer
v <- CoreInfo -> IO Integer
getCoreLB CoreInfo
core; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Integer
s forall a. Num a => a -> a -> a
+ Integer
v }) Integer
0 [CoreInfo]
xs

  IORef (LitMap Integer)
deductedWeightRef <- forall a. a -> IO (IORef a)
newIORef LitMap Integer
weights
  let deductWeight :: Integer -> CoreInfo -> IO ()
deductWeight Integer
d CoreInfo
core =
        forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (LitMap Integer)
deductedWeightRef forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith forall a. Num a => a -> a -> a
(+) forall a b. (a -> b) -> a -> b
$
          forall a. (Lit -> a) -> LitSet -> IntMap a
IntMap.fromSet (forall a b. a -> b -> a
const (- Integer
d)) (CoreInfo -> LitSet
coreLits CoreInfo
core)
      updateLB :: Integer -> CoreInfo -> IO ()
updateLB Integer
oldLB CoreInfo
core = do
        Integer
newLB <- IO Integer
getLB
        forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
newLB
        Integer -> CoreInfo -> IO ()
deductWeight (Integer
newLB forall a. Num a => a -> a -> a
- Integer
oldLB) CoreInfo
core
        forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Solver
solver (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CoreInfo -> IO Integer
getCoreLB CoreInfo
core -- redundant, but useful for direct search

  let loop :: IO ()
loop = do
        Integer
lb <- IO Integer
getLB
        Integer
ub <- do
          Integer
ub1 <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM Integer
C.getSearchUpperBound cxt
cxt
          -- FIXME: The refinement should be done in Context.addSolution,
          -- for generality and to avoid duplicated computation.
          let ub2 :: Integer
ub2 = [Integer] -> Integer -> Integer
refineUB (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst PBLinSum
obj) Integer
ub1
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub1 forall a. Eq a => a -> a -> Bool
/= Integer
ub2) forall a b. (a -> b) -> a -> b
$ 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
"BCD2: refineUB: %d -> %d" Integer
ub1 Integer
ub2
          forall (m :: * -> *) a. Monad m => a -> m a
return Integer
ub2
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub forall a. Ord a => a -> a -> Bool
< Integer
lb) forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> IO ()
C.setFinished cxt
cxt

        Bool
fin <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM Bool
C.isFinished cxt
cxt
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
fin forall a b. (a -> b) -> a -> b
$ do

          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Options -> Bool
optEnableHardening Options
opt) forall a b. (a -> b) -> a -> b
$ do
            LitMap Integer
deductedWeight <- forall a. IORef a -> IO a
readIORef IORef (LitMap Integer)
deductedWeightRef
            LitSet
hardened <- forall a. IORef a -> IO a
readIORef IORef LitSet
hardenedRef
            let lits :: LitSet
lits = forall a. IntMap a -> LitSet
IntMap.keysSet (forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (\Integer
w -> Integer
lb forall a. Num a => a -> a -> a
+ Integer
w forall a. Ord a => a -> a -> Bool
> Integer
ub) LitMap Integer
deductedWeight) LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
hardened
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LitSet -> Bool
IntSet.null LitSet
lits) forall a b. (a -> b) -> a -> b
$ do
              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
"BCD2: hardening fixes %d literals" (LitSet -> Lit
IntSet.size LitSet
lits)
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (LitSet -> Clause
IntSet.toList LitSet
lits) forall a b. (a -> b) -> a -> b
$ \Lit
lit -> forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [Lit
lit]
              forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
unrelaxedRef (LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
lits)
              forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
relaxedRef   (LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
lits)
              forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
hardenedRef  (LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
lits)

          Integer
ub0 <- forall a. IORef a -> IO a
readIORef IORef Integer
lastUBRef
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub forall a. Ord a => a -> a -> Bool
< Integer
ub0) forall a b. (a -> b) -> a -> b
$ do
            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
"BCD2: updating upper bound: %d -> %d" Integer
ub0 Integer
ub
            forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub
            forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
lastUBRef Integer
ub

          [CoreInfo]
cores     <- forall a. IORef a -> IO a
readIORef IORef [CoreInfo]
coresRef
          LitSet
unrelaxed <- forall a. IORef a -> IO a
readIORef IORef LitSet
unrelaxedRef
          LitSet
relaxed   <- forall a. IORef a -> IO a
readIORef IORef LitSet
relaxedRef
          LitSet
hardened  <- forall a. IORef a -> IO a
readIORef IORef LitSet
hardenedRef
          Integer
nsat   <- forall a. IORef a -> IO a
readIORef IORef Integer
nsatRef
          Integer
nunsat <- forall a. IORef a -> IO a
readIORef IORef Integer
nunsatRef
          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
"BCD2: %d <= obj <= %d" Integer
lb Integer
ub
          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
"BCD2: #cores=%d, #unrelaxed=%d, #relaxed=%d, #hardened=%d"
            (forall (t :: * -> *) a. Foldable t => t a -> Lit
length [CoreInfo]
cores) (LitSet -> Lit
IntSet.size LitSet
unrelaxed) (LitSet -> Lit
IntSet.size LitSet
relaxed) (LitSet -> Lit
IntSet.size LitSet
hardened)
          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
"BCD2: #sat=%d #unsat=%d bias=%d/%d" Integer
nsat Integer
nunsat Integer
nunsat (Integer
nunsat forall a. Num a => a -> a -> a
+ Integer
nsat)

          Maybe Model
lastModel <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM (Maybe Model)
C.getBestModel cxt
cxt
          IntMap (CoreInfo, Integer)
sels <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [(Lit, a)] -> IntMap a
IntMap.fromList 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 [CoreInfo]
cores forall a b. (a -> b) -> a -> b
$ \CoreInfo
core -> do
            Integer
coreLB <- CoreInfo -> IO Integer
getCoreLB CoreInfo
core
            let coreUB :: Integer
coreUB = PBLinSum -> Integer
SAT.pbLinUpperBound (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core)
            if Integer
coreUB forall a. Ord a => a -> a -> Bool
< Integer
coreLB then do
              -- Note: we have detected unsatisfiability
              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
"BCD2: coreLB (%d) exceeds coreUB (%d)" Integer
coreLB Integer
coreUB
              forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver []
              Lit
sel <- CoreInfo -> Integer -> IO Lit
getCoreUBAssumption CoreInfo
core Integer
coreUB
              forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, (CoreInfo
core, Integer
coreUB))
            else do
              let estimated :: Integer
estimated =
                    case Maybe Model
lastModel of
                      Maybe Model
Nothing -> Integer
coreUB
                      Just Model
m  ->
                        -- Since we might have added some hard constraints after obtaining @m@,
                        -- it's possible that @coreLB@ is larger than @SAT.evalPBLinSum m (coreCostFun core)@.
                        Integer
coreLB forall a. Ord a => a -> a -> a
`max` forall m. IModel m => m -> PBLinSum -> Integer
SAT.evalPBLinSum Model
m (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core)
                  mid :: Integer
mid =
                    if Options -> Bool
optEnableBiasedSearch Options
opt
                    then Integer
coreLB forall a. Num a => a -> a -> a
+ (Integer
estimated forall a. Num a => a -> a -> a
- Integer
coreLB) forall a. Num a => a -> a -> a
* Integer
nunsat forall a. Integral a => a -> a -> a
`div` (Integer
nunsat forall a. Num a => a -> a -> a
+ Integer
nsat)
                    else (Integer
coreLB forall a. Num a => a -> a -> a
+ Integer
estimated) forall a. Integral a => a -> a -> a
`div` Integer
2
              Lit
sel <- CoreInfo -> Integer -> IO Lit
getCoreUBAssumption CoreInfo
core Integer
mid
              forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, (CoreInfo
core,Integer
mid))

          Bool
ret <- Solver -> Clause -> IO Bool
SAT.solveWith Solver
solver (forall a. IntMap a -> Clause
IntMap.keys IntMap (CoreInfo, Integer)
sels forall a. [a] -> [a] -> [a]
++ LitSet -> Clause
IntSet.toList LitSet
unrelaxed)

          if Bool
ret then do
            forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Integer
nsatRef (forall a. Num a => a -> a -> a
+Integer
1)
            forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Model
SAT.getModel Solver
solver
            IO ()
loop
          else do
            forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Integer
nunsatRef (forall a. Num a => a -> a -> a
+Integer
1)
            LitSet
failed <- Solver -> IO LitSet
SAT.getFailedAssumptions Solver
solver

            case LitSet -> Clause
IntSet.toList LitSet
failed of
              [] -> forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
              [Lit
sel] | Just (CoreInfo
core,Integer
mid) <- forall a. Lit -> IntMap a -> Maybe a
IntMap.lookup Lit
sel IntMap (CoreInfo, Integer)
sels -> do
                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
"BCD2: updating lower bound of a core"
                let newCoreLB :: Integer
newCoreLB  = Integer
mid forall a. Num a => a -> a -> a
+ Integer
1
                    newCoreLB' :: Integer
newCoreLB' = [Integer] -> Integer -> Integer
refineLB (forall a. IntMap a -> [a]
IntMap.elems (forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys LitMap Integer
weights (CoreInfo -> LitSet
coreLits CoreInfo
core))) Integer
newCoreLB
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
newCoreLB forall a. Eq a => a -> a -> Bool
/= Integer
newCoreLB') forall a b. (a -> b) -> a -> b
$ 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
"BCD2: refineLB: %d -> %d" Integer
newCoreLB Integer
newCoreLB'
                forall a. IORef a -> a -> IO ()
writeIORef (CoreInfo -> IORef Integer
coreLBRef CoreInfo
core) Integer
newCoreLB'
                forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [-Lit
sel] -- Delete soft upperbound constraint(s) by fixing a selector variable
                Integer -> CoreInfo -> IO ()
updateLB Integer
lb CoreInfo
core
                IO ()
loop
              Clause
_ -> do
                let torelax :: LitSet
torelax     = LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IntSet.intersection` LitSet
failed
                    intersected :: [(CoreInfo, Integer)]
intersected = forall a. IntMap a -> [a]
IntMap.elems (forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys IntMap (CoreInfo, Integer)
sels LitSet
failed)
                    disjoint :: [CoreInfo]
disjoint    = [CoreInfo
core | (Lit
sel,(CoreInfo
core,Integer
_)) <- forall a. IntMap a -> [(Lit, a)]
IntMap.toList (forall a. IntMap a -> LitSet -> IntMap a
IntMap.withoutKeys IntMap (CoreInfo, Integer)
sels LitSet
failed)]
                forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
unrelaxedRef (LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
torelax)
                forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
relaxedRef (LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
torelax)
                Integer
delta <- do
                  [Integer]
xs1 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(CoreInfo, Integer)]
intersected forall a b. (a -> b) -> a -> b
$ \(CoreInfo
core,Integer
mid) -> do
                    Integer
coreLB <- CoreInfo -> IO Integer
getCoreLB CoreInfo
core
                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer
mid forall a. Num a => a -> a -> a
- Integer
coreLB forall a. Num a => a -> a -> a
+ Integer
1
                  let xs2 :: [Integer]
xs2 = [LitMap Integer
weights forall a. IntMap a -> Lit -> a
IntMap.! Lit
lit | Lit
lit <- LitSet -> Clause
IntSet.toList LitSet
torelax]
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Integer]
xs1 forall a. [a] -> [a] -> [a]
++ [Integer]
xs2)
                let mergedCoreLits :: LitSet
mergedCoreLits = forall (f :: * -> *). Foldable f => f LitSet -> LitSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ LitSet
torelax forall a. a -> [a] -> [a]
: [CoreInfo -> LitSet
coreLits CoreInfo
core | (CoreInfo
core,Integer
_) <- [(CoreInfo, Integer)]
intersected]
                Integer
mergedCoreLB <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((Integer
delta forall a. Num a => a -> a -> a
+) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CoreInfo -> IO Integer
getCoreLB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(CoreInfo, Integer)]
intersected
                let mergedCoreLB' :: Integer
mergedCoreLB' = [Integer] -> Integer -> Integer
refineLB (forall a. IntMap a -> [a]
IntMap.elems (forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys LitMap Integer
weights LitSet
mergedCoreLits)) Integer
mergedCoreLB
                CoreInfo
mergedCore <- LitSet -> Integer -> IO CoreInfo
newCoreInfo LitSet
mergedCoreLits Integer
mergedCoreLB'
                forall a. IORef a -> a -> IO ()
writeIORef IORef [CoreInfo]
coresRef (CoreInfo
mergedCore forall a. a -> [a] -> [a]
: [CoreInfo]
disjoint)
                forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(CoreInfo, Integer)]
intersected forall a b. (a -> b) -> a -> b
$ \(CoreInfo
core, Integer
_) -> Solver -> CoreInfo -> IO ()
deleteCoreInfo Solver
solver CoreInfo
core

                if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(CoreInfo, Integer)]
intersected then
                  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
"BCD2: found a new core of size %d: cost of the new core is >=%d"
                    (LitSet -> Lit
IntSet.size LitSet
torelax) Integer
mergedCoreLB'
                else
                  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
"BCD2: relaxing %d and merging with %d cores into a new core of size %d: cost of the new core is >=%d"
                    (LitSet -> Lit
IntSet.size LitSet
torelax) (forall (t :: * -> *) a. Foldable t => t a -> Lit
length [(CoreInfo, Integer)]
intersected) (LitSet -> Lit
IntSet.size LitSet
mergedCoreLits) Integer
mergedCoreLB'
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
mergedCoreLB forall a. Eq a => a -> a -> Bool
/= Integer
mergedCoreLB') forall a b. (a -> b) -> a -> b
$
                  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
"BCD2: refineLB: %d -> %d" Integer
mergedCoreLB Integer
mergedCoreLB'
                Integer -> CoreInfo -> IO ()
updateLB Integer
lb CoreInfo
mergedCore
                IO ()
loop

  Maybe Model
best <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM (Maybe Model)
C.getBestModel cxt
cxt
  case Maybe Model
best of
    Maybe Model
Nothing | Options -> Bool
optSolvingNormalFirst Options
opt -> do
      Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
      if Bool
ret then
        forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Model
SAT.getModel Solver
solver
      else
        forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
    Maybe Model
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  IO ()
loop

  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
IntMap.fromList [(Lit, Integer)]
sels

    coreCostFun :: CoreInfo -> SAT.PBLinSum
    coreCostFun :: CoreInfo -> PBLinSum
coreCostFun CoreInfo
c = [(LitMap Integer
weights forall a. IntMap a -> Lit -> a
IntMap.! Lit
lit, -Lit
lit) | Lit
lit <- LitSet -> Clause
IntSet.toList (CoreInfo -> LitSet
coreLits CoreInfo
c)]

    getCoreUBAssumption :: CoreInfo -> Integer -> IO SAT.Lit
    getCoreUBAssumption :: CoreInfo -> Integer -> IO Lit
getCoreUBAssumption CoreInfo
core Integer
ub = do
      Map Integer Lit
m <- forall a. IORef a -> IO a
readIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core)
      case forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
Map.splitLookup Integer
ub Map Integer Lit
m of
        (Map Integer Lit
_, Just Lit
sel, Map Integer Lit
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Lit
sel
        (Map Integer Lit
lo, Maybe Lit
Nothing, Map Integer Lit
hi)  -> do
          Lit
sel <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
          forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Lit
sel (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core) Integer
ub
          forall a. IORef a -> a -> IO ()
writeIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
ub Lit
sel Map Integer Lit
m)
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall k a. Map k a -> Bool
Map.null Map Integer Lit
lo) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [- forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMax Map Integer Lit
lo), Lit
sel] -- snd (Map.findMax lo) → sel
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall k a. Map k a -> Bool
Map.null Map Integer Lit
hi) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [- Lit
sel, forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMin Map Integer Lit
hi)] -- sel → Map.findMin hi
          forall (m :: * -> *) a. Monad m => a -> m a
return Lit
sel

-- | The smallest integer greater-than or equal-to @n@ that can be obtained by summing a subset of @ws@.
-- Note that the definition is different from the one in Morgado et al.
refineLB
  :: [Integer] -- ^ @ws@
  -> Integer   -- ^ @n@
  -> Integer
refineLB :: [Integer] -> Integer -> Integer
refineLB [Integer]
ws Integer
n =
  case forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Integer, Vector Bool)
SubsetSum.minSubsetSum (forall a. [a] -> Vector a
V.fromList [Integer]
ws) Integer
n of
    Maybe (Integer, Vector Bool)
Nothing -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
w | Integer
w <- [Integer]
ws, Integer
w forall a. Ord a => a -> a -> Bool
> Integer
0] forall a. Num a => a -> a -> a
+ Integer
1
    Just (Integer
obj, Vector Bool
_) -> Integer
obj

-- | The greatest integer lesser-than or equal-to @n@ that can be obtained by summing a subset of @ws@.
refineUB
  :: [Integer] -- ^ @ws@
  -> Integer   -- ^ @n@
  -> Integer
refineUB :: [Integer] -> Integer -> Integer
refineUB [Integer]
ws Integer
n
  | Integer
n forall a. Ord a => a -> a -> Bool
< Integer
0 = Integer
n
  | Bool
otherwise =
      case forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Integer, Vector Bool)
SubsetSum.maxSubsetSum (forall a. [a] -> Vector a
V.fromList [Integer]
ws) Integer
n of
        Maybe (Integer, Vector Bool)
Nothing -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
w | Integer
w <- [Integer]
ws, Integer
w forall a. Ord a => a -> a -> Bool
< Integer
0] forall a. Num a => a -> a -> a
- Integer
1
        Just (Integer
obj, Vector Bool
_) -> Integer
obj