{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Combinatorial.HittingSet.MARCO
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- * M. Liffiton and A. Malik, "Enumerating infeasibility: Finding multiple
--   MUSes quickly," in Integration of AI and OR Techniques in Constraint
--   Programming for Combinatorial Optimization Problems, C. Gomes and
--   M. Sellmann, Eds. pp. 160-175.
--   <http://sun.iwu.edu/~mliffito/publications/cpaior13_liffiton_MARCO.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.Combinatorial.HittingSet.MARCO
  (
  -- * Problem definition
    module ToySolver.Combinatorial.HittingSet.InterestingSets

  -- * Main functionality
  , run

  -- * Applications: monotone boolean functions
  , generateCNFAndDNF

  -- * Applicaitons: minimal hitting sets
  , minimalHittingSets
  ) where

import Control.Monad
import Data.Default.Class
import Data.IntMap ((!))
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.IORef
import Data.Set (Set)
import qualified Data.Set as Set
import System.IO.Unsafe
import ToySolver.Combinatorial.HittingSet.InterestingSets
import qualified ToySolver.SAT as SAT

-- | Given a problem and an option, it computes maximal interesting sets and
-- minimal uninteresting sets.
run :: forall prob. IsProblem prob IO => prob -> Options IO -> IO (Set IntSet, Set IntSet)
run :: forall prob.
IsProblem prob IO =>
prob -> Options IO -> IO (Set IntSet, Set IntSet)
run prob
prob Options IO
opt = do
  Solver
solver <- IO Solver
SAT.newSolver
  IntMap Var
item2var <- ([(Var, Var)] -> IntMap Var) -> IO [(Var, Var)] -> IO (IntMap Var)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Var, Var)] -> IntMap Var
forall a. [(Var, a)] -> IntMap a
IntMap.fromList (IO [(Var, Var)] -> IO (IntMap Var))
-> IO [(Var, Var)] -> IO (IntMap Var)
forall a b. (a -> b) -> a -> b
$ [Var] -> (Var -> IO (Var, Var)) -> IO [(Var, Var)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (IntSet -> [Var]
IntSet.toList (prob -> IntSet
forall prob (m :: * -> *). IsProblem prob m => prob -> IntSet
universe prob
prob)) ((Var -> IO (Var, Var)) -> IO [(Var, Var)])
-> (Var -> IO (Var, Var)) -> IO [(Var, Var)]
forall a b. (a -> b) -> a -> b
$ \Var
item -> do
    Var
v <- Solver -> IO Var
forall (m :: * -> *) a. NewVar m a => a -> m Var
SAT.newVar Solver
solver
    (Var, Var) -> IO (Var, Var)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
item,Var
v)
  let blockUp :: IntSet -> IO ()
blockUp IntSet
xs = Solver -> [Var] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Solver
solver [-(IntMap Var
item2var IntMap Var -> Var -> Var
forall a. IntMap a -> Var -> a
! Var
x) | Var
x <- IntSet -> [Var]
IntSet.toList IntSet
xs]
      blockDown :: IntSet -> IO ()
blockDown IntSet
xs = Solver -> [Var] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Solver
solver [IntMap Var
item2var IntMap Var -> Var -> Var
forall a. IntMap a -> Var -> a
! Var
x | Var
x <- IntSet -> [Var]
IntSet.toList (prob -> IntSet
forall prob (m :: * -> *). IsProblem prob m => prob -> IntSet
universe prob
prob IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
xs)]
  IORef [IntSet]
posRef <- [IntSet] -> IO (IORef [IntSet])
forall a. a -> IO (IORef a)
newIORef ([IntSet] -> IO (IORef [IntSet]))
-> [IntSet] -> IO (IORef [IntSet])
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Options IO -> Set IntSet
forall (m :: * -> *). Options m -> Set IntSet
optMaximalInterestingSets Options IO
opt
  IORef [IntSet]
negRef <- [IntSet] -> IO (IORef [IntSet])
forall a. a -> IO (IORef a)
newIORef ([IntSet] -> IO (IORef [IntSet]))
-> [IntSet] -> IO (IORef [IntSet])
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Options IO -> Set IntSet
forall (m :: * -> *). Options m -> Set IntSet
optMinimalUninterestingSets Options IO
opt
  (IntSet -> IO ()) -> [IntSet] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ IntSet -> IO ()
blockUp ([IntSet] -> IO ()) -> [IntSet] -> IO ()
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Options IO -> Set IntSet
forall (m :: * -> *). Options m -> Set IntSet
optMinimalUninterestingSets Options IO
opt
  (IntSet -> IO ()) -> [IntSet] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ IntSet -> IO ()
blockDown ([IntSet] -> IO ()) -> [IntSet] -> IO ()
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Options IO -> Set IntSet
forall (m :: * -> *). Options m -> Set IntSet
optMaximalInterestingSets Options IO
opt
  let loop :: IO ()
loop = do
        Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
        if Bool -> Bool
not Bool
ret then
          () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else do
          Model
model <- Solver -> IO Model
SAT.getModel Solver
solver
          let xs :: IntSet
xs = IntMap Var -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet (IntMap Var -> IntSet) -> IntMap Var -> IntSet
forall a b. (a -> b) -> a -> b
$ (Var -> Bool) -> IntMap Var -> IntMap Var
forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (Model -> Var -> Bool
forall m. IModel m => m -> Var -> Bool
SAT.evalLit Model
model) IntMap Var
item2var
          InterestingOrUninterestingSet
ret2 <- prob -> IntSet -> IO InterestingOrUninterestingSet
forall prob (m :: * -> *).
IsProblem prob m =>
prob -> IntSet -> m InterestingOrUninterestingSet
minimalUninterestingSetOrMaximalInterestingSet prob
prob IntSet
xs
          case InterestingOrUninterestingSet
ret2 of
            UninterestingSet IntSet
ys -> do
              IntSet -> IO ()
blockUp IntSet
ys
              IORef [IntSet] -> ([IntSet] -> [IntSet]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [IntSet]
negRef (IntSet
ys IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
:)
              Options IO -> IntSet -> IO ()
forall (m :: * -> *). Options m -> IntSet -> m ()
optOnMinimalUninterestingSetFound Options IO
opt IntSet
ys
            InterestingSet IntSet
ys -> do
              IntSet -> IO ()
blockDown IntSet
ys
              IORef [IntSet] -> ([IntSet] -> [IntSet]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [IntSet]
posRef (IntSet
ys IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
:)
              Options IO -> IntSet -> IO ()
forall (m :: * -> *). Options m -> IntSet -> m ()
optOnMaximalInterestingSetFound Options IO
opt IntSet
ys
          IO ()
loop
  IO ()
loop
  [IntSet]
pos <- IORef [IntSet] -> IO [IntSet]
forall a. IORef a -> IO a
readIORef IORef [IntSet]
posRef
  [IntSet]
neg <- IORef [IntSet] -> IO [IntSet]
forall a. IORef a -> IO a
readIORef IORef [IntSet]
negRef
  (Set IntSet, Set IntSet) -> IO (Set IntSet, Set IntSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([IntSet] -> Set IntSet
forall a. Ord a => [a] -> Set a
Set.fromList [IntSet]
pos, [IntSet] -> Set IntSet
forall a. Ord a => [a] -> Set a
Set.fromList [IntSet]
neg)

-- | Compute the irredundant CNF representation and DNF representation.
--
-- Let /f/ be a monotone boolean function over set of variables /S/.
-- This function returns /C/ and /D/ where ∧_{I∈C} ∨_{i∈I} x_i and
-- ∨_{I∈D} ∧_{i∈I} x_i are the irredundant CNF representation /f/ and
-- DNF representation of /f/ respectively.
generateCNFAndDNF
  :: IntSet -- ^ Set of variables /V/
  -> (IntSet -> Bool) -- ^ A monotone boolean function /f/ from /{0,1}^|V| ≅ P(V)/ to @Bool@
  -> Set IntSet -- ^ Subset /C'/ of prime implicates /C/ of /f/
  -> Set IntSet -- ^ Subset /D'/ of prime implicants /D/ of /f/
  -> (Set IntSet, Set IntSet)
generateCNFAndDNF :: IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> (Set IntSet, Set IntSet)
generateCNFAndDNF IntSet
vs IntSet -> Bool
f Set IntSet
cs Set IntSet
ds = IO (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet)
forall a. IO a -> a
unsafeDupablePerformIO (IO (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet))
-> IO (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet)
forall a b. (a -> b) -> a -> b
$ do
  (Set IntSet
pos,Set IntSet
neg) <- SimpleProblem IO -> Options IO -> IO (Set IntSet, Set IntSet)
forall prob.
IsProblem prob IO =>
prob -> Options IO -> IO (Set IntSet, Set IntSet)
run SimpleProblem IO
forall {m :: * -> *}. SimpleProblem m
prob Options IO
opt
  (Set IntSet, Set IntSet) -> IO (Set IntSet, Set IntSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet
vs IntSet -> IntSet -> IntSet
`IntSet.difference`) Set IntSet
pos, Set IntSet
neg)
  where
    prob :: SimpleProblem m
prob = IntSet -> (IntSet -> Bool) -> SimpleProblem m
forall (m :: * -> *). IntSet -> (IntSet -> Bool) -> SimpleProblem m
SimpleProblem IntSet
vs (Bool -> Bool
not (Bool -> Bool) -> (IntSet -> Bool) -> IntSet -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Bool
f)
    opt :: Options IO
opt = Options IO
forall a. Default a => a
def
      { optMaximalInterestingSets = Set.map (vs `IntSet.difference`) cs
      , optMinimalUninterestingSets = ds
      }

minimalHittingSets :: Set IntSet -> Set IntSet
minimalHittingSets :: Set IntSet -> Set IntSet
minimalHittingSets Set IntSet
xss =
  case IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> (Set IntSet, Set IntSet)
generateCNFAndDNF ([IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
xss) (Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
xss) Set IntSet
forall a. Set a
Set.empty Set IntSet
xss of
    (Set IntSet
yss, Set IntSet
_) -> Set IntSet
yss

evalDNF :: Set IntSet -> IntSet -> Bool
evalDNF :: Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
dnf IntSet
xs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
is IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
xs | IntSet
is <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
dnf]