-----------------------------------------------------------------------------
-- |
-- 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.List
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 -> [Int] -> Options -> IO ()
enumMCSAssumptions Solver
solver [Int]
sels Options
opt = do
  IORef [(Int, CS)]
candRef <- forall a. a -> IO (IORef a)
newIORef [(CS -> Int
IS.size CS
cs, CS
cs) | CS
cs <- Options -> [CS]
optKnownCSes Options
opt]
  IORef [(Int, CS)] -> Int -> IO ()
loop IORef [(Int, CS)]
candRef Int
1

  where
    log :: String -> IO ()
    log :: String -> IO ()
log = Options -> String -> IO ()
optLogger Options
opt

    mcsFound :: MCS -> IO ()
    mcsFound :: CS -> IO ()
mcsFound CS
mcs = do
      Options -> CS -> IO ()
optOnMCSFound Options
opt CS
mcs
      forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver (CS -> [Int]
IS.toList CS
mcs)

    loop :: IORef [(Int, LitSet)] -> Int -> IO ()
    loop :: IORef [(Int, CS)] -> Int -> IO ()
loop IORef [(Int, CS)]
candRef Int
k = do
      String -> IO ()
log forall a b. (a -> b) -> a -> b
$ String
"CAMUS: k = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
k
      [(Int, CS)]
cand <- forall a. IORef a -> IO a
readIORef IORef [(Int, CS)]
candRef

      Bool
ret <- if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, CS)]
cand) then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else Solver -> IO Bool
SAT.solve Solver
solver
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ret forall a b. (a -> b) -> a -> b
$ do
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, CS)]
cand forall a b. (a -> b) -> a -> b
$ \(Int
size,CS
cs) -> do
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
size forall a. Eq a => a -> a -> Bool
== Int
k) forall a b. (a -> b) -> a -> b
$ do
            -- If a candidate MCS is not superset of already obtained MCS,
            -- we are sure that it is actually an MCS.
            CS -> IO ()
mcsFound CS
cs
        forall a. IORef a -> a -> IO ()
writeIORef IORef [(Int, CS)]
candRef [(Int
size,CS
cs) | (Int
size,CS
cs) <- [(Int, CS)]
cand, Int
size forall a. Eq a => a -> a -> Bool
/= Int
k]

        Int
vk <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Solver
solver
        forall (m :: * -> *) a.
AddPBLin m a =>
a -> Int -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Int
vk [(Integer
1,-Int
sel) | Int
sel <- [Int]
sels] (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k)
        let loop2 :: IO ()
loop2 = do
              Bool
ret2 <- Solver -> [Int] -> IO Bool
SAT.solveWith Solver
solver [Int
vk]
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ret2 forall a b. (a -> b) -> a -> b
$ do
                Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
                let mcs :: CS
mcs = [Int] -> CS
IS.fromList [Int
sel | Int
sel <- [Int]
sels, Bool -> Bool
not (forall m. IModel m => m -> Int -> Bool
evalLit Model
m Int
sel)]
                CS -> IO ()
mcsFound CS
mcs
                forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [(Int, CS)]
candRef (forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
_,CS
cs) -> Bool -> Bool
not (CS
mcs CS -> CS -> Bool
`IS.isSubsetOf` CS
cs)))
                IO ()
loop2
        IO ()
loop2
        forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver [-Int
vk]
        IORef [(Int, CS)] -> Int -> IO ()
loop IORef [(Int, CS)]
candRef (Int
kforall a. Num a => a -> a -> a
+Int
1)

allMCSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO [MCS]
allMCSAssumptions :: Solver -> [Int] -> Options -> IO [CS]
allMCSAssumptions Solver
solver [Int]
sels Options
opt = do
  IORef [CS]
ref <- forall a. a -> IO (IORef a)
newIORef []
  let opt2 :: Options
opt2 =
        Options
opt
        { optOnMCSFound :: CS -> IO ()
optOnMCSFound = \CS
mcs -> do
            forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [CS]
ref (CS
mcsforall a. a -> [a] -> [a]
:)
            Options -> CS -> IO ()
optOnMCSFound Options
opt CS
mcs
        }
  Solver -> [Int] -> Options -> IO ()
enumMCSAssumptions Solver
solver [Int]
sels Options
opt2
  forall a. IORef a -> IO a
readIORef IORef [CS]
ref

allMUSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO ([MUS], [MCS])
allMUSAssumptions :: Solver -> [Int] -> Options -> IO ([CS], [CS])
allMUSAssumptions Solver
solver [Int]
sels Options
opt = do
  String -> IO ()
log String
"CAMUS: MCS enumeration begins"
  [CS]
mcses <- Solver -> [Int] -> Options -> IO [CS]
allMCSAssumptions Solver
solver [Int]
sels Options
opt
  String -> IO ()
log String
"CAMUS: MCS enumeration done"
  let muses :: [CS]
muses = Set CS -> [CS]
HittingSet.enumMinimalHittingSets forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [CS]
mcses
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Options -> CS -> IO ()
optOnMUSFound Options
opt) [CS]
muses
  forall (m :: * -> *) a. Monad m => a -> m a
return ([CS]
muses, [CS]
mcses)
  where
    log :: String -> IO ()
    log :: String -> IO ()
log = Options -> String -> IO ()
optLogger Options
opt