-----------------------------------------------------------------------------
-- |
-- 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 -> [Lit] -> Options -> IO ()
enumMCSAssumptions Solver
solver [Lit]
sels Options
opt = do
  IORef [(Lit, CS)]
candRef <- [(Lit, CS)] -> IO (IORef [(Lit, CS)])
forall a. a -> IO (IORef a)
newIORef [(CS -> Lit
IS.size CS
cs, CS
cs) | CS
cs <- Options -> [CS]
optKnownCSes Options
opt]
  IORef [(Lit, CS)] -> Lit -> IO ()
loop IORef [(Lit, CS)]
candRef Lit
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 -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver (CS -> [Lit]
IS.toList CS
mcs)

    loop :: IORef [(Int, LitSet)] -> Int -> IO ()
    loop :: IORef [(Lit, CS)] -> Lit -> IO ()
loop IORef [(Lit, CS)]
candRef Lit
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]
++ Lit -> String
forall a. Show a => a -> String
show Lit
k
      [(Lit, CS)]
cand <- IORef [(Lit, CS)] -> IO [(Lit, CS)]
forall a. IORef a -> IO a
readIORef IORef [(Lit, CS)]
candRef

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

        Lit
vk <- 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
vk [(Integer
1,-Lit
sel) | Lit
sel <- [Lit]
sels] (Lit -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Lit
k)
        let loop2 :: IO ()
loop2 = do
              Bool
ret2 <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver [Lit
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 = [Lit] -> CS
IS.fromList [Lit
sel | Lit
sel <- [Lit]
sels, Bool -> Bool
not (Model -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
evalLit Model
m Lit
sel)]
                CS -> IO ()
mcsFound CS
mcs
                IORef [(Lit, CS)] -> ([(Lit, CS)] -> [(Lit, CS)]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [(Lit, CS)]
candRef (((Lit, CS) -> Bool) -> [(Lit, CS)] -> [(Lit, CS)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Lit
_,CS
cs) -> Bool -> Bool
not (CS
mcs CS -> CS -> Bool
`IS.isSubsetOf` CS
cs)))
                IO ()
loop2
        IO ()
loop2
        Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
vk]
        IORef [(Lit, CS)] -> Lit -> IO ()
loop IORef [(Lit, CS)]
candRef (Lit
kLit -> Lit -> Lit
forall a. Num a => a -> a -> a
+Lit
1)

allMCSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO [MCS]
allMCSAssumptions :: Solver -> [Lit] -> Options -> IO [CS]
allMCSAssumptions Solver
solver [Lit]
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 -> IO ()
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 -> [Lit] -> Options -> IO ()
enumMCSAssumptions Solver
solver [Lit]
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 -> [Lit] -> Options -> IO ([CS], [CS])
allMUSAssumptions Solver
solver [Lit]
sels Options
opt = do
  String -> IO ()
log String
"CAMUS: MCS enumeration begins"
  [CS]
mcses <- Solver -> [Lit] -> Options -> IO [CS]
allMCSAssumptions Solver
solver [Lit]
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 (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