{-# 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 forall a. Num a => a -> a -> a
+ CoreInfo -> Integer
coreUB CoreInfo
c) forall a. Integral a => a -> a -> a
`div` Integer
2

coreUnion :: CoreInfo -> CoreInfo -> CoreInfo
coreUnion :: CoreInfo -> CoreInfo -> CoreInfo
coreUnion CoreInfo
c1 CoreInfo
c2
  = 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 forall a. Num a => a -> a -> a
+ CoreInfo -> Integer
coreLB CoreInfo
c2
  , coreUB :: Integer
coreUB = CoreInfo -> Integer
coreUB CoreInfo
c1 forall a. Num a => a -> a -> a
+ CoreInfo -> Integer
coreUB CoreInfo
c2
  }

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 }
  Integer
ub <- 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
  (LitSet, LitSet) -> [CoreInfo] -> Integer -> IO ()
loop ([Lit] -> LitSet
IntSet.fromList [Lit
lit | (Lit
lit,Integer
_) <- [(Lit, Integer)]
sels], LitSet
IntSet.empty) [] Integer
ub

  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

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

    coreCostFun :: CoreInfo -> SAT.PBLinSum
    coreCostFun :: CoreInfo -> PBLinSum
coreCostFun CoreInfo
c = [(Integer
w, -Lit
lit)  | (Lit
lit, Integer
w) <- forall a. IntMap a -> [(Lit, a)]
IntMap.toList (forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys LitMap Integer
weights (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 = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [CoreInfo -> Integer
coreLB CoreInfo
info | CoreInfo
info <- [CoreInfo]
cores]
      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
"BCD: %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
"BCD: #cores=%d, #unrelaxed=%d, #relaxed=%d"
        (forall (t :: * -> *) a. Foldable t => t a -> Lit
length [CoreInfo]
cores) (LitSet -> Lit
IntSet.size LitSet
unrelaxed) (LitSet -> Lit
IntSet.size LitSet
relaxed)

      IntMap CoreInfo
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
info -> 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
info) (CoreInfo -> Integer
coreMidValue CoreInfo
info)
        forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, CoreInfo
info)

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

      if Bool
ret then do
        Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
        let val :: Integer
val = forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
        let ub' :: Integer
ub' = Integer
val forall a. Num a => a -> a -> a
- Integer
1
        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
"BCD: updating upper bound: %d -> %d" Integer
ub Integer
ub'
        forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
        forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub'
        let cores' :: [CoreInfo]
cores' = forall a b. (a -> b) -> [a] -> [b]
map (\CoreInfo
info -> CoreInfo
info{ coreUB :: Integer
coreUB = 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 -> [Lit]
IntSet.toList LitSet
core of
          [] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          [Lit
sel] | Just CoreInfo
info <- forall a. Lit -> IntMap a -> Maybe a
IntMap.lookup Lit
sel IntMap CoreInfo
sels -> do
            let info' :: CoreInfo
info'  = CoreInfo
info{ coreLB :: Integer
coreLB = CoreInfo -> Integer
coreMidValue CoreInfo
info forall a. Num a => a -> a -> a
+ Integer
1 }
                cores' :: [CoreInfo]
cores' = forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ forall a. Lit -> a -> IntMap a -> IntMap a
IntMap.insert Lit
sel CoreInfo
info' IntMap CoreInfo
sels
            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
"BCD: updating lower bound of a core"
            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
          [Lit]
_ -> do
            let torelax :: LitSet
torelax     = LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IntSet.intersection` LitSet
core
                intersected :: [CoreInfo]
intersected = forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys IntMap CoreInfo
sels LitSet
core
                rest :: [CoreInfo]
rest        = forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> LitSet -> IntMap a
IntMap.withoutKeys IntMap CoreInfo
sels LitSet
core
                mergedCore :: CoreInfo
mergedCore  = 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 forall a. a -> [a] -> [a]
: [CoreInfo]
rest
            if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoreInfo]
intersected then 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
"BCD: found a new core of size %d" (LitSet -> Lit
IntSet.size LitSet
torelax)
            else 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
"BCD: merging cores"
            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
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. IntMap a -> [Lit]
IntMap.keys IntMap CoreInfo
sels) forall a b. (a -> b) -> a -> b
$ \Lit
sel -> forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
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
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\CoreInfo
info -> CoreInfo -> Integer
coreLB CoreInfo
info forall a. Ord a => a -> a -> Bool
> CoreInfo -> Integer
coreUB CoreInfo
info) [CoreInfo]
cores = 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