{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO.MSU4
-- Copyright   :  (c) Masahiro Sakai 2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Reference:
--
-- * João P. Marques-Silva and Jordi Planes.
--   Algorithms for Maximum Satisfiability using Unsatisfiable Cores.
--   In Design, Automation and Test in Europe, 2008 (DATE '08). March 2008.
--   pp. 408-413, doi:10.1109/date.2008.4484715.
--   <https://doi.org/10.1109/date.2008.4484715>
--   <http://eprints.soton.ac.uk/265000/1/jpms-date08.pdf>
--   <http://www.csi.ucd.ie/staff/jpms/talks/talksite/jpms-date08.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.SAT.PBO.MSU4
  ( solve
  ) where

import Control.Concurrent.STM
import Control.Monad
import qualified Data.IntSet as IS
import qualified Data.IntMap as IM
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 :: 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 }
  (LitSet, LitSet) -> Integer -> IO ()
loop (IntMap Integer -> LitSet
forall a. IntMap a -> LitSet
IM.keysSet IntMap Integer
weights, LitSet
IS.empty) Integer
0

  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 :: IntMap Integer
weights = [(Lit, Integer)] -> IntMap Integer
forall a. [(Lit, a)] -> IntMap a
IM.fromList [(Lit, Integer)]
sels

    loop :: (SAT.LitSet, SAT.LitSet) -> Integer -> IO ()
    loop :: (LitSet, LitSet) -> Integer -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) Integer
lb = do
      Bool
ret <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (LitSet -> [Lit]
IS.toList LitSet
unrelaxed)
      if Bool
ret then do
        Model
currModel <- Solver -> IO Model
SAT.getModel Solver
solver
        cxt -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
currModel
        let violated :: [Integer]
violated = [IntMap Integer
weights IntMap Integer -> Lit -> Integer
forall a. IntMap a -> Lit -> a
IM.! Lit
l | Lit
l <- LitSet -> [Lit]
IS.toList LitSet
relaxed, Model -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
SAT.evalLit Model
currModel Lit
l Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False]
            currVal :: Integer
currVal = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer]
violated
        Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver [(Integer
c,-Lit
l) | (Lit
l,Integer
c) <- [(Lit, Integer)]
sels] (Integer
currVal Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
        (LitSet, LitSet) -> Integer -> IO ()
cont (LitSet
unrelaxed, LitSet
relaxed) Integer
lb
      else do
        LitSet
core <- Solver -> IO LitSet
SAT.getFailedAssumptions Solver
solver
        let ls :: LitSet
ls = LitSet
core LitSet -> LitSet -> LitSet
`IS.intersection` LitSet
unrelaxed
        if LitSet -> Bool
IS.null LitSet
ls then do
          cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
        else do
          Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
l | Lit
l <- LitSet -> [Lit]
IS.toList LitSet
core] -- optional constraint but sometimes useful
          let min_weight :: Integer
min_weight = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [IntMap Integer
weights IntMap Integer -> Lit -> Integer
forall a. IntMap a -> Lit -> a
IM.! Lit
l | Lit
l <- LitSet -> [Lit]
IS.toList LitSet
ls]
              lb' :: Integer
lb' = Integer
lb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
min_weight
          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
"MSU4: found a core: size = %d, minimal weight = %d" (LitSet -> Lit
IS.size LitSet
core) Integer
min_weight
          cxt -> Integer -> IO ()
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
lb'
          (LitSet, LitSet) -> Integer -> IO ()
cont (LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IS.difference` LitSet
ls, LitSet
relaxed LitSet -> LitSet -> LitSet
`IS.union` LitSet
ls) Integer
lb'

    cont :: (SAT.LitSet, SAT.LitSet) -> Integer -> IO ()
    cont :: (LitSet, LitSet) -> Integer -> IO ()
cont (LitSet
unrelaxed, LitSet
relaxed) Integer
lb = do
      IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM (IO ()) -> IO (IO ())
forall a. STM a -> IO a
atomically (STM (IO ()) -> IO (IO ())) -> STM (IO ()) -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ do
        Bool
b <- cxt -> STM Bool
forall a. Context a => a -> STM Bool
C.isFinished cxt
cxt
        IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ if Bool
b then () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () else (LitSet, LitSet) -> Integer -> IO ()
loop (LitSet
unrelaxed, LitSet
relaxed) Integer
lb