{-# 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
  { 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 :: forall cxt. Context cxt => 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 :: forall cxt. Context cxt => 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{ SAT.configEnableBackwardSubsumptionRemoval = 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 ([Lit] -> LitSet
IntSet.fromList [Lit
lit | (Lit
lit,Integer
_) <- [(Lit, 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 :: [(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

    coreNew :: SAT.LitSet -> CoreInfo
    coreNew :: LitSet -> CoreInfo
coreNew LitSet
cs = CoreInfo{ coreLits :: LitSet
coreLits = LitSet
cs, coreLB :: Integer
coreLB = Integer
0, coreUB :: Integer
coreUB = [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [LitMap Integer
weights LitMap Integer -> Lit -> Integer
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) <- LitMap Integer -> [(Lit, Integer)]
forall a. IntMap a -> [(Lit, a)]
IntMap.toList (LitMap Integer -> LitSet -> LitMap Integer
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 = [Integer] -> Integer
forall a. Num a => [a] -> a
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 -> Lit -> Lit -> Lit -> String
forall r. PrintfType r => String -> r
printf String
"BCD: #cores=%d, #unrelaxed=%d, #relaxed=%d"
        ([CoreInfo] -> Lit
forall a. [a] -> Lit
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 <- ([(Lit, CoreInfo)] -> IntMap CoreInfo)
-> IO [(Lit, CoreInfo)] -> IO (IntMap CoreInfo)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Lit, CoreInfo)] -> IntMap CoreInfo
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList (IO [(Lit, CoreInfo)] -> IO (IntMap CoreInfo))
-> IO [(Lit, CoreInfo)] -> IO (IntMap CoreInfo)
forall a b. (a -> b) -> a -> b
$ [CoreInfo]
-> (CoreInfo -> IO (Lit, CoreInfo)) -> IO [(Lit, CoreInfo)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [CoreInfo]
cores ((CoreInfo -> IO (Lit, CoreInfo)) -> IO [(Lit, CoreInfo)])
-> (CoreInfo -> IO (Lit, CoreInfo)) -> IO [(Lit, CoreInfo)]
forall a b. (a -> b) -> a -> b
$ \CoreInfo
info -> 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
info) (CoreInfo -> Integer
coreMidValue CoreInfo
info)
        (Lit, CoreInfo) -> IO (Lit, CoreInfo)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, CoreInfo
info)

      Bool
ret <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (IntMap CoreInfo -> [Lit]
forall a. IntMap a -> [Lit]
IntMap.keys IntMap CoreInfo
sels [Lit] -> [Lit] -> [Lit]
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 = 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 = SAT.evalPBLinSum m (coreCostFun 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
          [] -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          [Lit
sel] | Just CoreInfo
info <- Lit -> IntMap CoreInfo -> Maybe CoreInfo
forall a. Lit -> IntMap a -> Maybe a
IntMap.lookup Lit
sel IntMap CoreInfo
sels -> do
            let info' :: CoreInfo
info'  = CoreInfo
info{ coreLB = coreMidValue info + 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
$ Lit -> CoreInfo -> IntMap CoreInfo -> IntMap CoreInfo
forall a. Lit -> a -> IntMap a -> IntMap a
IntMap.insert Lit
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
          [Lit]
_ -> do
            let torelax :: LitSet
torelax     = LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IntSet.intersection` LitSet
core
                intersected :: [CoreInfo]
intersected = IntMap CoreInfo -> [CoreInfo]
forall a. IntMap a -> [a]
IntMap.elems (IntMap CoreInfo -> [CoreInfo]) -> IntMap CoreInfo -> [CoreInfo]
forall a b. (a -> b) -> a -> b
$ IntMap CoreInfo -> LitSet -> IntMap CoreInfo
forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys IntMap CoreInfo
sels LitSet
core
                rest :: [CoreInfo]
rest        = IntMap CoreInfo -> [CoreInfo]
forall a. IntMap a -> [a]
IntMap.elems (IntMap CoreInfo -> [CoreInfo]) -> IntMap CoreInfo -> [CoreInfo]
forall a b. (a -> b) -> a -> b
$ IntMap CoreInfo -> LitSet -> IntMap CoreInfo
forall a. IntMap a -> LitSet -> IntMap a
IntMap.withoutKeys IntMap CoreInfo
sels LitSet
core
                mergedCore :: CoreInfo
mergedCore  = (CoreInfo -> CoreInfo -> CoreInfo)
-> CoreInfo -> [CoreInfo] -> CoreInfo
forall b a. (b -> a -> b) -> b -> [a] -> b
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 a. [a] -> 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 -> Lit -> String
forall r. PrintfType r => String -> r
printf String
"BCD: found a new core of size %d" (LitSet -> Lit
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
            [Lit] -> (Lit -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap CoreInfo -> [Lit]
forall a. IntMap a -> [Lit]
IntMap.keys IntMap CoreInfo
sels) ((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] -- 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