content: -----------------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.SAT.MUS.Enum.CAMUS
  -- Copyright   :  (c) Masahiro Sakai 2012-2014
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  portable
  --
  -- In this module, we assume each soft constraint /C_i/ is represented as a literal.
  -- If a constraint /C_i/ is not a literal, we can represent it as a fresh variable /v/
  -- together with a hard constraint /v ⇒ C_i/.
  --
  -- References:
  --
  -- * [CAMUS] M. Liffiton and K. Sakallah, Algorithms for computing minimal
  --   unsatisfiable subsets of constraints, Journal of Automated Reasoning,
  --   vol. 40, no. 1, pp. 1-33, Jan. 2008.
  --   <http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf>
  --
  -- * [HYCAM] A. Gregoire, B. Mazure, and C. Piette, Boosting a complete
  --   technique to find MSS and MUS: thanks to a local search oracle, in
  --   Proceedings of the 20th international joint conference on Artifical
  --   intelligence, ser. IJCAI'07. San Francisco, CA, USA: Morgan Kaufmann
  --   Publishers Inc., 2007, pp. 2300-2305.
  --   <http://ijcai.org/papers07/Papers/IJCAI07-370.pdf>
  --
  -----------------------------------------------------------------------------
  module ToySolver.SAT.MUS.Enum.CAMUS
    ( module ToySolver.SAT.MUS.Enum.Base
    , allMUSAssumptions
    , allMCSAssumptions
    , enumMCSAssumptions
    ) where
  
  import Control.Monad
  import Data.Array.IArray
  import Data.Default.Class
  import qualified Data.IntSet as IS
  import Data.IORef
  import Data.Set (Set)
  import qualified Data.Set as Set
  import qualified ToySolver.Combinatorial.HittingSet.Simple as HittingSet
  import qualified ToySolver.SAT as SAT
  import ToySolver.SAT.Types
  import ToySolver.SAT.MUS.Enum.Base
  
  enumMCSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO ()
  enumMCSAssumptions solver sels opt = do
    candRef <- newIORef [(IS.size cs, cs) | cs <- optKnownCSes opt]
    loop candRef 1
  
    where
      log :: String -> IO ()
      log = optLogger opt
  
      mcsFound :: MCS -> IO ()
      mcsFound mcs = do
        optOnMCSFound opt mcs
        SAT.addClause solver (IS.toList mcs)
  
      loop :: IORef [(Int, LitSet)] -> Int -> IO ()
      loop candRef k = do
        log $ "CAMUS: k = " ++ show k
        cand <- readIORef candRef
  
        ret <- if not (null cand) then return True else SAT.solve solver
        when ret $ do
          forM_ cand $ \(size,cs) -> do
            when (size == k) $ do
              -- If a candidate MCS is not superset of already obtained MCS,
              -- we are sure that it is actually an MCS.
              mcsFound cs
          writeIORef candRef [(size,cs) | (size,cs) <- cand, size /= k]
  
          vk <- SAT.newVar solver
          SAT.addPBAtMostSoft solver vk [(1,-sel) | sel <- sels] (fromIntegral k)
          let loop2 = do
                ret2 <- SAT.solveWith solver [vk]
                when ret2 $ do
                  m <- SAT.getModel solver
                  let mcs = IS.fromList [sel | sel <- sels, not (evalLit m sel)]
                  mcsFound mcs
                  modifyIORef candRef (filter (\(_,cs) -> not (mcs `IS.isSubsetOf` cs)))
                  loop2
          loop2
          SAT.addClause solver [-vk]
          loop candRef (k+1)
  
  allMCSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO [MCS]
  allMCSAssumptions solver sels opt = do
    ref <- newIORef []
    let opt2 =
          opt
          { optOnMCSFound = \mcs -> do
              modifyIORef ref (mcs:)
              optOnMCSFound opt mcs
          }
    enumMCSAssumptions solver sels opt2
    readIORef ref
  
  allMUSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO ([MUS], [MCS])
  allMUSAssumptions solver sels opt = do
    log "CAMUS: MCS enumeration begins"
    mcses <- allMCSAssumptions solver sels opt
    log "CAMUS: MCS enumeration done"
    let muses = HittingSet.enumMinimalHittingSets $ Set.fromList mcses
    mapM_ (optOnMUSFound opt) muses
    return (muses, mcses)
    where
      log :: String -> IO ()
      log = optLogger opt
  