-----------------------------------------------------------------------------
-- |
-- 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 <- [(Int, CS)] -> IO (IORef [(Int, CS)])
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
      Solver -> [Int] -> IO ()
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 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"CAMUS: k = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k
      [(Int, CS)]
cand <- IORef [(Int, CS)] -> IO [(Int, CS)]
forall a. IORef a -> IO a
readIORef IORef [(Int, CS)]
candRef

      Bool
ret <- if Bool -> Bool
not ([(Int, CS)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, CS)]
cand) then Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else Solver -> IO Bool
SAT.solve Solver
solver
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ret (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        [(Int, CS)] -> ((Int, CS) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, CS)]
cand (((Int, CS) -> IO ()) -> IO ()) -> ((Int, CS) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
size,CS
cs) -> do
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
size Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k) (IO () -> IO ()) -> IO () -> IO ()
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
        IORef [(Int, CS)] -> [(Int, CS)] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef [(Int, CS)]
candRef [(Int
size,CS
cs) | (Int
size,CS
cs) <- [(Int, CS)]
cand, Int
size Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
k]

        Int
vk <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Solver
solver
        Solver -> Int -> PBLinSum -> Integer -> IO ()
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] (Int -> Integer
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]
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ret2 (IO () -> IO ()) -> IO () -> IO ()
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 (Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
evalLit Model
m Int
sel)]
                CS -> IO ()
mcsFound CS
mcs
                IORef [(Int, CS)] -> ([(Int, CS)] -> [(Int, CS)]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [(Int, CS)]
candRef (((Int, CS) -> Bool) -> [(Int, CS)] -> [(Int, CS)]
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
        Solver -> [Int] -> IO ()
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
kInt -> Int -> Int
forall 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 <- [CS] -> IO (IORef [CS])
forall a. a -> IO (IORef a)
newIORef []
  let opt2 :: Options
opt2 =
        Options
opt
        { optOnMCSFound = \CS
mcs -> do
            IORef [CS] -> ([CS] -> [CS]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [CS]
ref (CS
mcsCS -> [CS] -> [CS]
forall a. a -> [a] -> [a]
:)
            Options -> CS -> IO ()
optOnMCSFound Options
opt CS
mcs
        }
  Solver -> [Int] -> Options -> IO ()
enumMCSAssumptions Solver
solver [Int]
sels Options
opt2
  IORef [CS] -> IO [CS]
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 (Set CS -> [CS]) -> Set CS -> [CS]
forall a b. (a -> b) -> a -> b
$ [CS] -> Set CS
forall a. Ord a => [a] -> Set a
Set.fromList [CS]
mcses
  (CS -> IO ()) -> [CS] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Options -> CS -> IO ()
optOnMUSFound Options
opt) [CS]
muses
  ([CS], [CS]) -> IO ([CS], [CS])
forall a. a -> IO a
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