{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO.BCD
-- Copyright   :  (c) Masahiro Sakai 2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  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.BCD
  ( solve
  ) where

import Control.Concurrent.STM
import Control.Monad
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Data.List
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.PBO.Context as C
import Text.Printf

data CoreInfo
  = CoreInfo
  { CoreInfo -> LitSet
coreLits :: SAT.LitSet
  , CoreInfo -> Integer
coreLB   :: !Integer
  , CoreInfo -> Integer
coreUB   :: !Integer
  }

coreMidValue :: CoreInfo -> Integer
coreMidValue :: CoreInfo -> Integer
coreMidValue CoreInfo
c = (CoreInfo -> Integer
coreLB CoreInfo
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ CoreInfo -> Integer
coreUB CoreInfo
c) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2

coreUnion :: CoreInfo -> CoreInfo -> CoreInfo
coreUnion :: CoreInfo -> CoreInfo -> CoreInfo
coreUnion CoreInfo
c1 CoreInfo
c2
  = CoreInfo :: LitSet -> Integer -> Integer -> CoreInfo
CoreInfo
  { coreLits :: LitSet
coreLits = LitSet -> LitSet -> LitSet
IntSet.union (CoreInfo -> LitSet
coreLits CoreInfo
c1) (CoreInfo -> LitSet
coreLits CoreInfo
c2)
  , coreLB :: Integer
coreLB = CoreInfo -> Integer
coreLB CoreInfo
c1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ CoreInfo -> Integer
coreLB CoreInfo
c2
  , coreUB :: Integer
coreUB = CoreInfo -> Integer
coreUB CoreInfo
c1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ CoreInfo -> Integer
coreUB CoreInfo
c2
  }

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

solveWBO :: C.Context cxt => cxt -> SAT.Solver -> IO ()
solveWBO :: cxt -> Solver -> IO ()
solveWBO cxt
cxt Solver
solver = do
  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 }
  Integer
ub <- 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
  (LitSet, LitSet) -> [CoreInfo] -> Integer -> IO ()
loop ([Key] -> LitSet
IntSet.fromList [Key
lit | (Key
lit,Integer
_) <- [(Key, Integer)]
sels], LitSet
IntSet.empty) [] Integer
ub

  where
    obj :: SAT.PBLinSum
    obj :: PBLinSum
obj = cxt -> PBLinSum
forall a. Context a => a -> PBLinSum
C.getObjectiveFunction cxt
cxt

    sels :: [(SAT.Lit, Integer)]
    sels :: [(Key, Integer)]
sels = [(-Key
lit, Integer
w) | (Integer
w,Key
lit) <- PBLinSum
obj]

    weights :: SAT.LitMap Integer
    weights :: LitMap Integer
weights = [(Key, Integer)] -> LitMap Integer
forall a. [(Key, a)] -> IntMap a
IntMap.fromList [(Key, Integer)]
sels

    coreNew :: SAT.LitSet -> CoreInfo
    coreNew :: LitSet -> CoreInfo
coreNew LitSet
cs = CoreInfo :: LitSet -> Integer -> Integer -> CoreInfo
CoreInfo{ coreLits :: LitSet
coreLits = LitSet
cs, coreLB :: Integer
coreLB = Integer
0, coreUB :: Integer
coreUB = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [LitMap Integer
weights LitMap Integer -> Key -> Integer
forall a. IntMap a -> Key -> a
IntMap.! Key
lit | Key
lit <- LitSet -> [Key]
IntSet.toList LitSet
cs] }

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

    loop :: (SAT.LitSet, SAT.LitSet) -> [CoreInfo] -> Integer -> IO ()
    loop :: (LitSet, LitSet) -> [CoreInfo] -> Integer -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) [CoreInfo]
cores Integer
ub = do
      let lb :: Integer
lb = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [CoreInfo -> Integer
coreLB CoreInfo
info | CoreInfo
info <- [CoreInfo]
cores]
      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
"BCD: %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 -> Key -> Key -> Key -> String
forall r. PrintfType r => String -> r
printf String
"BCD: #cores=%d, #unrelaxed=%d, #relaxed=%d"
        ([CoreInfo] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [CoreInfo]
cores) (LitSet -> Key
IntSet.size LitSet
unrelaxed) (LitSet -> Key
IntSet.size LitSet
relaxed)

      IntMap CoreInfo
sels <- ([(Key, CoreInfo)] -> IntMap CoreInfo)
-> IO [(Key, CoreInfo)] -> IO (IntMap CoreInfo)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Key, CoreInfo)] -> IntMap CoreInfo
forall a. [(Key, a)] -> IntMap a
IntMap.fromList (IO [(Key, CoreInfo)] -> IO (IntMap CoreInfo))
-> IO [(Key, CoreInfo)] -> IO (IntMap CoreInfo)
forall a b. (a -> b) -> a -> b
$ [CoreInfo]
-> (CoreInfo -> IO (Key, CoreInfo)) -> IO [(Key, CoreInfo)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [CoreInfo]
cores ((CoreInfo -> IO (Key, CoreInfo)) -> IO [(Key, CoreInfo)])
-> (CoreInfo -> IO (Key, CoreInfo)) -> IO [(Key, CoreInfo)]
forall a b. (a -> b) -> a -> b
$ \CoreInfo
info -> do
        Key
sel <- Solver -> IO Key
forall (m :: * -> *) a. NewVar m a => a -> m Key
SAT.newVar Solver
solver
        Solver -> Key -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Key -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Key
sel (CoreInfo -> PBLinSum
coreCostFun CoreInfo
info) (CoreInfo -> Integer
coreMidValue CoreInfo
info)
        (Key, CoreInfo) -> IO (Key, CoreInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (Key
sel, CoreInfo
info)

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

      if Bool
ret then do
        Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
        let val :: Integer
val = cxt -> Model -> Integer
forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
        let ub' :: Integer
ub' = Integer
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
        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
"BCD: updating upper bound: %d -> %d" Integer
ub Integer
ub'
        cxt -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
        Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub'
        let cores' :: [CoreInfo]
cores' = (CoreInfo -> CoreInfo) -> [CoreInfo] -> [CoreInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\CoreInfo
info -> CoreInfo
info{ coreUB :: Integer
coreUB = Model -> PBLinSum -> Integer
forall m. IModel m => m -> PBLinSum -> Integer
SAT.evalPBLinSum Model
m (CoreInfo -> PBLinSum
coreCostFun CoreInfo
info) }) [CoreInfo]
cores
        (LitSet, LitSet) -> [CoreInfo] -> Integer -> IO ()
cont (LitSet
unrelaxed, LitSet
relaxed) [CoreInfo]
cores' Integer
ub'
      else do
        LitSet
core <- Solver -> IO LitSet
SAT.getFailedAssumptions Solver
solver
        case LitSet -> [Key]
IntSet.toList LitSet
core of
          [] -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          [Key
sel] | Just CoreInfo
info <- Key -> IntMap CoreInfo -> Maybe CoreInfo
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
sel IntMap CoreInfo
sels -> do
            let info' :: CoreInfo
info'  = CoreInfo
info{ coreLB :: Integer
coreLB = CoreInfo -> Integer
coreMidValue CoreInfo
info Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 }
                cores' :: [CoreInfo]
cores' = IntMap CoreInfo -> [CoreInfo]
forall a. IntMap a -> [a]
IntMap.elems (IntMap CoreInfo -> [CoreInfo]) -> IntMap CoreInfo -> [CoreInfo]
forall a b. (a -> b) -> a -> b
$ Key -> CoreInfo -> IntMap CoreInfo -> IntMap CoreInfo
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert Key
sel CoreInfo
info' IntMap CoreInfo
sels
            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
"BCD: updating lower bound of a core"
            Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Solver
solver (CoreInfo -> PBLinSum
coreCostFun CoreInfo
info') (CoreInfo -> Integer
coreLB CoreInfo
info') -- redundant, but useful for direct search
            (LitSet, LitSet) -> [CoreInfo] -> Integer -> IO ()
cont (LitSet
unrelaxed, LitSet
relaxed) [CoreInfo]
cores' Integer
ub
          [Key]
_ -> do
            let torelax :: LitSet
torelax     = LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IntSet.intersection` LitSet
core
                intersected :: [CoreInfo]
intersected = [CoreInfo
info | (Key
sel,CoreInfo
info) <- IntMap CoreInfo -> [(Key, CoreInfo)]
forall a. IntMap a -> [(Key, a)]
IntMap.toList IntMap CoreInfo
sels, Key
sel Key -> LitSet -> Bool
`IntSet.member` LitSet
core]
                rest :: [CoreInfo]
rest        = [CoreInfo
info | (Key
sel,CoreInfo
info) <- IntMap CoreInfo -> [(Key, CoreInfo)]
forall a. IntMap a -> [(Key, a)]
IntMap.toList IntMap CoreInfo
sels, Key
sel Key -> LitSet -> Bool
`IntSet.notMember` LitSet
core]
                mergedCore :: CoreInfo
mergedCore  = (CoreInfo -> CoreInfo -> CoreInfo)
-> CoreInfo -> [CoreInfo] -> CoreInfo
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' CoreInfo -> CoreInfo -> CoreInfo
coreUnion (LitSet -> CoreInfo
coreNew LitSet
torelax) [CoreInfo]
intersected
                unrelaxed' :: LitSet
unrelaxed'  = LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
torelax
                relaxed' :: LitSet
relaxed'    = LitSet
relaxed LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
torelax
                cores' :: [CoreInfo]
cores'      = CoreInfo
mergedCore CoreInfo -> [CoreInfo] -> [CoreInfo]
forall a. a -> [a] -> [a]
: [CoreInfo]
rest
            if [CoreInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoreInfo]
intersected then 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 -> Key -> String
forall r. PrintfType r => String -> r
printf String
"BCD: found a new core of size %d" (LitSet -> Key
IntSet.size LitSet
torelax)
            else 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
"BCD: merging cores"
            Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Solver
solver (CoreInfo -> PBLinSum
coreCostFun CoreInfo
mergedCore) (CoreInfo -> Integer
coreLB CoreInfo
mergedCore) -- redundant, but useful for direct search
            [Key] -> (Key -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap CoreInfo -> [Key]
forall a. IntMap a -> [Key]
IntMap.keys IntMap CoreInfo
sels) ((Key -> IO ()) -> IO ()) -> (Key -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Key
sel -> Solver -> [Key] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Key] -> m ()
SAT.addClause Solver
solver [-Key
sel] -- delete temporary constraints
            (LitSet, LitSet) -> [CoreInfo] -> Integer -> IO ()
cont (LitSet
unrelaxed', LitSet
relaxed') [CoreInfo]
cores' Integer
ub

    cont :: (SAT.LitSet, SAT.LitSet) -> [CoreInfo] -> Integer -> IO ()
    cont :: (LitSet, LitSet) -> [CoreInfo] -> Integer -> IO ()
cont (LitSet
unrelaxed, LitSet
relaxed) [CoreInfo]
cores Integer
ub
      | (CoreInfo -> Bool) -> [CoreInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\CoreInfo
info -> CoreInfo -> Integer
coreLB CoreInfo
info Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> CoreInfo -> Integer
coreUB CoreInfo
info) [CoreInfo]
cores = cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
      | Bool
otherwise = (LitSet, LitSet) -> [CoreInfo] -> Integer -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) [CoreInfo]
cores Integer
ub