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

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

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

    loop :: (SAT.LitSet, SAT.LitSet) -> (Integer, Integer) -> IO ()
    loop :: (LitSet, LitSet) -> (Integer, Integer) -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) (Integer
lb, Integer
ub)
      | Integer
lb Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
ub = cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
      | Bool
otherwise = do
          let mid :: Integer
mid = (Integer
lb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
ub) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2
          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 -> String
forall r. PrintfType r => String -> r
printf String
"BC: %d <= obj <= %d; guessing obj <= %d" Integer
lb Integer
ub Integer
mid
          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 [(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 LitSet
relaxed)] Integer
mid
          Bool
ret <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (Lit
sel 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
"BC: 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 -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [Lit
sel]
            Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub'
            (LitSet, LitSet) -> (Integer, Integer) -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) (Integer
lb, Integer
ub')
          else do
            LitSet
core <- Solver -> IO LitSet
SAT.getFailedAssumptions Solver
solver
            Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
sel] -- delete temporary constraint
            let core2 :: LitSet
core2 = LitSet
core LitSet -> LitSet -> LitSet
`IntSet.intersection` LitSet
unrelaxed
            if LitSet -> Bool
IntSet.null LitSet
core2 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 -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"BC: updating lower bound: %d -> %d" Integer
lb (Integer
midInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)
              cxt -> Integer -> IO ()
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt (Integer
midInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)
              (LitSet, LitSet) -> (Integer, Integer) -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) (Integer
midInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1, Integer
ub)
            else do
              let unrelaxed' :: LitSet
unrelaxed' = LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
core2
                  relaxed' :: LitSet
relaxed'   = LitSet
relaxed LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
core2
              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 -> String
forall r. PrintfType r => String -> r
printf String
"BC: #unrelaxed=%d, #relaxed=%d" (LitSet -> Lit
IntSet.size LitSet
unrelaxed') (LitSet -> Lit
IntSet.size LitSet
relaxed')
              (LitSet, LitSet) -> (Integer, Integer) -> IO ()
loop (LitSet
unrelaxed', LitSet
relaxed') (Integer
lb, Integer
ub)