{-# 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 :: Bool -> Bool -> Bool -> Options
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 <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
lb
  IORef (Map Integer Lit)
selsRef <- Map Integer Lit -> IO (IORef (Map Integer Lit))
forall a. a -> IO (IORef a)
newIORef Map Integer Lit
forall k a. Map k a
Map.empty
  CoreInfo -> IO CoreInfo
forall (m :: * -> *) a. Monad m => a -> m a
return
    CoreInfo :: LitSet -> IORef Integer -> IORef (Map Integer Lit) -> CoreInfo
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 <- IORef (Map Integer Lit) -> IO (Map Integer Lit)
forall a. IORef a -> IO a
readIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core)
  -- Delete soft upperbound constraints by fixing selector variables
  [Lit] -> (Lit -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Integer Lit -> [Lit]
forall k a. Map k a -> [a]
Map.elems Map Integer Lit
m) ((Lit -> IO ()) -> IO ()) -> (Lit -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Lit
sel ->
    Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
sel]

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

solve :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
solve :: cxt -> Solver -> Options -> IO ()
solve cxt
cxt Solver
solver Options
opt = Normalized cxt -> Solver -> Options -> IO ()
forall cxt. Context cxt => cxt -> Solver -> Options -> IO ()
solveWBO (cxt -> Normalized cxt
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 :: cxt -> Solver -> Options -> IO ()
solveWBO cxt
cxt Solver
solver Options
opt = do
  cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall r. PrintfType r => String -> r
printf String
"BCD2: Hardening is %s." (if Options -> Bool
optEnableHardening Options
opt then String
"enabled" else String
"disabled")
  cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String
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 ((Config -> Config) -> IO ()) -> (Config -> Config) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Config
config -> Config
config{ configEnableBackwardSubsumptionRemoval :: Bool
SAT.configEnableBackwardSubsumptionRemoval = Bool
True }

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

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

  IORef [CoreInfo]
coresRef <- [CoreInfo] -> IO (IORef [CoreInfo])
forall a. a -> IO (IORef a)
newIORef []
  let getLB :: IO Integer
getLB = do
        [CoreInfo]
xs <- IORef [CoreInfo] -> IO [CoreInfo]
forall a. IORef a -> IO a
readIORef IORef [CoreInfo]
coresRef
        (Integer -> CoreInfo -> IO Integer)
-> Integer -> [CoreInfo] -> IO Integer
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; Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> IO Integer) -> Integer -> IO Integer
forall a b. (a -> b) -> a -> b
$! Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v }) Integer
0 [CoreInfo]
xs

  IORef (LitMap Integer)
deductedWeightRef <- LitMap Integer -> IO (IORef (LitMap Integer))
forall a. a -> IO (IORef a)
newIORef LitMap Integer
weights
  let deductWeight :: Integer -> CoreInfo -> IO ()
deductWeight Integer
d CoreInfo
core =
        IORef (LitMap Integer)
-> (LitMap Integer -> LitMap Integer) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (LitMap Integer)
deductedWeightRef ((LitMap Integer -> LitMap Integer) -> IO ())
-> (LitMap Integer -> LitMap Integer) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer)
-> LitMap Integer -> LitMap Integer -> LitMap Integer
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (LitMap Integer -> LitMap Integer -> LitMap Integer)
-> LitMap Integer -> LitMap Integer -> LitMap Integer
forall a b. (a -> b) -> a -> b
$
          [(Lit, Integer)] -> LitMap Integer
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit
lit, - Integer
d) | Lit
lit <- LitSet -> [Lit]
IntSet.toList (CoreInfo -> LitSet
coreLits CoreInfo
core)]
      updateLB :: Integer -> CoreInfo -> IO ()
updateLB Integer
oldLB CoreInfo
core = do
        Integer
newLB <- IO Integer
getLB
        cxt -> Integer -> IO ()
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
newLB
        Integer -> CoreInfo -> IO ()
deductWeight (Integer
newLB Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
oldLB) CoreInfo
core
        Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Solver
solver (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core) (Integer -> IO ()) -> IO Integer -> IO ()
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 <- STM Integer -> IO Integer
forall a. STM a -> IO a
atomically (STM Integer -> IO Integer) -> STM Integer -> IO Integer
forall a b. (a -> b) -> a -> b
$ cxt -> STM Integer
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 (((Integer, Lit) -> Integer) -> PBLinSum -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Lit) -> Integer
forall a b. (a, b) -> a
fst PBLinSum
obj) Integer
ub1
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
ub2) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"BCD2: refineUB: %d -> %d" Integer
ub1 Integer
ub2
          Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
ub2
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
lb) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt

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

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

          Integer
ub0 <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
lastUBRef
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
ub0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
            cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"BCD2: updating upper bound: %d -> %d" Integer
ub0 Integer
ub
            Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub
            IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
lastUBRef Integer
ub

          [CoreInfo]
cores     <- IORef [CoreInfo] -> IO [CoreInfo]
forall a. IORef a -> IO a
readIORef IORef [CoreInfo]
coresRef
          LitSet
unrelaxed <- IORef LitSet -> IO LitSet
forall a. IORef a -> IO a
readIORef IORef LitSet
unrelaxedRef
          LitSet
relaxed   <- IORef LitSet -> IO LitSet
forall a. IORef a -> IO a
readIORef IORef LitSet
relaxedRef
          LitSet
hardened  <- IORef LitSet -> IO LitSet
forall a. IORef a -> IO a
readIORef IORef LitSet
hardenedRef
          Integer
nsat   <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
nsatRef
          Integer
nunsat <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
nunsatRef
          cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"BCD2: %d <= obj <= %d" Integer
lb Integer
ub
          cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Lit -> Lit -> Lit -> Lit -> String
forall r. PrintfType r => String -> r
printf String
"BCD2: #cores=%d, #unrelaxed=%d, #relaxed=%d, #hardened=%d"
            ([CoreInfo] -> Lit
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)
          cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"BCD2: #sat=%d #unsat=%d bias=%d/%d" Integer
nsat Integer
nunsat Integer
nunsat (Integer
nunsat Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
nsat)

          Maybe Model
lastModel <- STM (Maybe Model) -> IO (Maybe Model)
forall a. STM a -> IO a
atomically (STM (Maybe Model) -> IO (Maybe Model))
-> STM (Maybe Model) -> IO (Maybe Model)
forall a b. (a -> b) -> a -> b
$ cxt -> STM (Maybe Model)
forall a. Context a => a -> STM (Maybe Model)
C.getBestModel cxt
cxt
          IntMap (CoreInfo, Integer)
sels <- ([(Lit, (CoreInfo, Integer))] -> IntMap (CoreInfo, Integer))
-> IO [(Lit, (CoreInfo, Integer))]
-> IO (IntMap (CoreInfo, Integer))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Lit, (CoreInfo, Integer))] -> IntMap (CoreInfo, Integer)
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList (IO [(Lit, (CoreInfo, Integer))]
 -> IO (IntMap (CoreInfo, Integer)))
-> IO [(Lit, (CoreInfo, Integer))]
-> IO (IntMap (CoreInfo, Integer))
forall a b. (a -> b) -> a -> b
$ [CoreInfo]
-> (CoreInfo -> IO (Lit, (CoreInfo, Integer)))
-> IO [(Lit, (CoreInfo, Integer))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [CoreInfo]
cores ((CoreInfo -> IO (Lit, (CoreInfo, Integer)))
 -> IO [(Lit, (CoreInfo, Integer))])
-> (CoreInfo -> IO (Lit, (CoreInfo, Integer)))
-> IO [(Lit, (CoreInfo, Integer))]
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
coreLB then do
              -- Note: we have detected unsatisfiability
              cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"BCD2: coreLB (%d) exceeds coreUB (%d)" Integer
coreLB Integer
coreUB
              Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver []
              Lit
sel <- CoreInfo -> Integer -> IO Lit
getCoreUBAssumption CoreInfo
core Integer
coreUB
              (Lit, (CoreInfo, Integer)) -> IO (Lit, (CoreInfo, Integer))
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 Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`max` Model -> PBLinSum -> Integer
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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
estimated Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
coreLB) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
nunsat Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` (Integer
nunsat Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
nsat)
                    else (Integer
coreLB Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
estimated) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2
              Lit
sel <- CoreInfo -> Integer -> IO Lit
getCoreUBAssumption CoreInfo
core Integer
mid
              (Lit, (CoreInfo, Integer)) -> IO (Lit, (CoreInfo, Integer))
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, (CoreInfo
core,Integer
mid))

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

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

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

                if [(CoreInfo, Integer)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(CoreInfo, Integer)]
intersected then
                  cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Lit -> Integer -> String
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
                  cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Lit -> Lit -> Lit -> Integer -> String
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) ([(CoreInfo, Integer)] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
length [(CoreInfo, Integer)]
intersected) (LitSet -> Lit
IntSet.size LitSet
mergedCoreLits) Integer
mergedCoreLB'
                Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
mergedCoreLB Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
mergedCoreLB') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
                  cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
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 <- STM (Maybe Model) -> IO (Maybe Model)
forall a. STM a -> IO a
atomically (STM (Maybe Model) -> IO (Maybe Model))
-> STM (Maybe Model) -> IO (Maybe Model)
forall a b. (a -> b) -> a -> b
$ cxt -> STM (Maybe Model)
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
        cxt -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt (Model -> IO ()) -> IO Model -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Model
SAT.getModel Solver
solver
      else
        cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
    Maybe Model
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  IO ()
loop

  where
    obj :: SAT.PBLinSum
    obj :: PBLinSum
obj = cxt -> PBLinSum
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 = [(Lit, Integer)] -> LitMap Integer
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit, Integer)]
sels

    coreCostFun :: CoreInfo -> SAT.PBLinSum
    coreCostFun :: CoreInfo -> PBLinSum
coreCostFun CoreInfo
c = [(LitMap Integer
weights LitMap Integer -> Lit -> Integer
forall a. IntMap a -> Lit -> a
IntMap.! Lit
lit, -Lit
lit) | Lit
lit <- LitSet -> [Lit]
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 <- IORef (Map Integer Lit) -> IO (Map Integer Lit)
forall a. IORef a -> IO a
readIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core)
      case Integer
-> Map Integer Lit -> (Map Integer Lit, Maybe Lit, Map Integer Lit)
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
_) -> Lit -> IO 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 <- Solver -> IO Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
          Solver -> Lit -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Lit
sel (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core) Integer
ub
          IORef (Map Integer Lit) -> Map Integer Lit -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core) (Integer -> Lit -> Map Integer Lit -> Map Integer Lit
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
ub Lit
sel Map Integer Lit
m)
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Map Integer Lit -> Bool
forall k a. Map k a -> Bool
Map.null Map Integer Lit
lo) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
            Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [- (Integer, Lit) -> Lit
forall a b. (a, b) -> b
snd (Map Integer Lit -> (Integer, Lit)
forall k a. Map k a -> (k, a)
Map.findMax Map Integer Lit
lo), Lit
sel] -- snd (Map.findMax lo) → sel
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Map Integer Lit -> Bool
forall k a. Map k a -> Bool
Map.null Map Integer Lit
hi) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
            Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [- Lit
sel, (Integer, Lit) -> Lit
forall a b. (a, b) -> b
snd (Map Integer Lit -> (Integer, Lit)
forall k a. Map k a -> (k, a)
Map.findMin Map Integer Lit
hi)] -- sel → Map.findMin hi
          Lit -> IO Lit
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 Vector Integer -> Integer -> Maybe (Integer, Vector Bool)
forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Integer, Vector Bool)
SubsetSum.minSubsetSum ([Integer] -> Vector Integer
forall a. [a] -> Vector a
V.fromList [Integer]
ws) Integer
n of
    Maybe (Integer, Vector Bool)
Nothing -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
w | Integer
w <- [Integer]
ws, Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0] Integer -> Integer -> Integer
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Integer
n
  | Bool
otherwise =
      case Vector Integer -> Integer -> Maybe (Integer, Vector Bool)
forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Integer, Vector Bool)
SubsetSum.maxSubsetSum ([Integer] -> Vector Integer
forall a. [a] -> Vector a
V.fromList [Integer]
ws) Integer
n of
        Maybe (Integer, Vector Bool)
Nothing -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
w | Integer
w <- [Integer]
ws, Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0] Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
        Just (Integer
obj, Vector Bool
_) -> Integer
obj