{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Combinatorial.HittingSet.DAA
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- "Dualize and Advance" algorithm for enumerating maximal interesting sets
-- and minimal non-interesting sets.
--
-- * [GMKT1997]
--   D. Gunopulos, H. Mannila, R. Khardon, and H. Toivonen, Data mining,
--   hypergraph transversals, and machine learning (extended abstract),
--   in Proceedings of the Sixteenth ACM SIGACT-SIGMOD-SIGART Symposium
--   on Principles of Database Systems, ser. PODS '97. 1997, pp. 209-216.
--   <http://almaden.ibm.com/cs/projects/iis/hdb/Publications/papers/pods97_trans.pdf>
--
-- * [BaileyStuckey2015]
--   J. Bailey and P. Stuckey, Discovery of minimal unsatisfiable
--   subsets of constraints using hitting set dualization," in Practical
--   Aspects of Declarative Languages, pp. 174-186, 2005.
--   <http://ww2.cs.mu.oz.au/~pjs/papers/padl05.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.Combinatorial.HittingSet.DAA
  (
  -- * Problem definition
    module ToySolver.Combinatorial.HittingSet.InterestingSets

  -- * Main functionality
  , run

  -- * Applications: minimal hitting sets
  , generateCNFAndDNF
  ) where

import Control.Monad.Identity
import Data.Default.Class
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Set (Set)
import qualified Data.Set as Set
import ToySolver.Combinatorial.HittingSet.InterestingSets
import ToySolver.Combinatorial.HittingSet.Util (maintainNoSupersets)

-- | Given a problem and an option, it computes maximal interesting sets and
-- minimal uninteresting sets.
run :: forall prob m. IsProblem prob m => prob -> Options m -> m (Set IntSet, Set IntSet)
run :: forall prob (m :: * -> *).
IsProblem prob m =>
prob -> Options m -> m (Set IntSet, Set IntSet)
run prob
prob Options m
opt = do
  let comp_pos :: Set IntSet
comp_pos = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map IntSet -> IntSet
complement (Options m -> Set IntSet
forall (m :: * -> *). Options m -> Set IntSet
optMaximalInterestingSets Options m
opt)
  Set IntSet
hst_comp_pos <- Options m -> Set IntSet -> m (Set IntSet)
forall (m :: * -> *). Options m -> Set IntSet -> m (Set IntSet)
optMinimalHittingSets Options m
opt Set IntSet
comp_pos
  Set IntSet
-> Set IntSet -> Set IntSet -> m (Set IntSet, Set IntSet)
loop Set IntSet
comp_pos Set IntSet
hst_comp_pos (Options m -> Set IntSet
forall (m :: * -> *). Options m -> Set IntSet
optMinimalUninterestingSets Options m
opt)

  where
    univ :: IntSet
    univ :: IntSet
univ = prob -> IntSet
forall prob (m :: * -> *). IsProblem prob m => prob -> IntSet
universe prob
prob

    complement :: IntSet -> IntSet
    complement :: IntSet -> IntSet
complement = (IntSet
univ IntSet -> IntSet -> IntSet
`IntSet.difference`)

    loop :: Set IntSet -> Set IntSet -> Set IntSet -> m (Set IntSet, Set IntSet)
    loop :: Set IntSet
-> Set IntSet -> Set IntSet -> m (Set IntSet, Set IntSet)
loop Set IntSet
comp_pos Set IntSet
hst_comp_pos Set IntSet
neg = do
      let xss :: Set IntSet
xss = Set IntSet
hst_comp_pos Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set IntSet
neg
      if Set IntSet -> Bool
forall a. Set a -> Bool
Set.null Set IntSet
xss then
        (Set IntSet, Set IntSet) -> m (Set IntSet, Set IntSet)
forall a. a -> m 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 -> IntSet
complement Set IntSet
comp_pos, Set IntSet
neg)
      else do
        (Set IntSet
comp_pos', Set IntSet
hst_comp_pos', Set IntSet
neg') <- Set IntSet
-> Set IntSet
-> Set IntSet
-> [IntSet]
-> m (Set IntSet, Set IntSet, Set IntSet)
loop2 Set IntSet
comp_pos Set IntSet
hst_comp_pos Set IntSet
neg (Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
xss)
        Set IntSet
-> Set IntSet -> Set IntSet -> m (Set IntSet, Set IntSet)
loop Set IntSet
comp_pos' Set IntSet
hst_comp_pos' Set IntSet
neg'

    loop2 :: Set IntSet -> Set IntSet -> Set IntSet -> [IntSet] -> m (Set IntSet, Set IntSet, Set IntSet)
    loop2 :: Set IntSet
-> Set IntSet
-> Set IntSet
-> [IntSet]
-> m (Set IntSet, Set IntSet, Set IntSet)
loop2 Set IntSet
comp_pos Set IntSet
hst_comp_pos Set IntSet
neg [] = (Set IntSet, Set IntSet, Set IntSet)
-> m (Set IntSet, Set IntSet, Set IntSet)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set IntSet
comp_pos, Set IntSet
hst_comp_pos, Set IntSet
neg)
    loop2 Set IntSet
comp_pos Set IntSet
hst_comp_pos Set IntSet
neg (IntSet
xs : [IntSet]
xss) = do
      Maybe IntSet
ret <- prob -> IntSet -> m (Maybe IntSet)
forall prob (m :: * -> *).
IsProblem prob m =>
prob -> IntSet -> m (Maybe IntSet)
maximalInterestingSet prob
prob IntSet
xs
      case Maybe IntSet
ret of
        Maybe IntSet
Nothing -> do
          Options m -> IntSet -> m ()
forall (m :: * -> *). Options m -> IntSet -> m ()
optOnMinimalUninterestingSetFound Options m
opt IntSet
xs
          Set IntSet
-> Set IntSet
-> Set IntSet
-> [IntSet]
-> m (Set IntSet, Set IntSet, Set IntSet)
loop2 Set IntSet
comp_pos Set IntSet
hst_comp_pos (IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
xs Set IntSet
neg) [IntSet]
xss
        Just IntSet
ys -> do
          Options m -> IntSet -> m ()
forall (m :: * -> *). Options m -> IntSet -> m ()
optOnMaximalInterestingSetFound Options m
opt IntSet
ys
          let zs :: IntSet
zs = IntSet -> IntSet
complement IntSet
ys
              comp_pos' :: Set IntSet
comp_pos' = IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
zs Set IntSet
comp_pos
              -- "4.2 Incremental Hitting set Calculation" from [BaileyStuckey2015]
              hst_comp_pos' :: Set IntSet
hst_comp_pos' = [IntSet] -> Set IntSet
forall a. Ord a => [a] -> Set a
Set.fromList ([IntSet] -> Set IntSet) -> [IntSet] -> Set IntSet
forall a b. (a -> b) -> a -> b
$ [IntSet] -> [IntSet]
maintainNoSupersets ([IntSet] -> [IntSet]) -> [IntSet] -> [IntSet]
forall a b. (a -> b) -> a -> b
$
                [Key -> IntSet -> IntSet
IntSet.insert Key
w IntSet
ws | IntSet
ws <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
hst_comp_pos, Key
w <- IntSet -> [Key]
IntSet.toList IntSet
zs]
          -- hst_comp_pos' <- optMinimalHittingSets opt comp_pos'
          (Set IntSet, Set IntSet, Set IntSet)
-> m (Set IntSet, Set IntSet, Set IntSet)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set IntSet
comp_pos', Set IntSet
hst_comp_pos', Set 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 = ((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 Identity
opt = Options Identity
forall a. Default a => a
def
      { optMaximalInterestingSets = Set.map (vs `IntSet.difference`) cs
      , optMinimalUninterestingSets = ds
      }
    (Set IntSet
pos,Set IntSet
neg) = Identity (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet)
forall a. Identity a -> a
runIdentity (Identity (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet))
-> Identity (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet)
forall a b. (a -> b) -> a -> b
$ SimpleProblem Identity
-> Options Identity -> Identity (Set IntSet, Set IntSet)
forall prob (m :: * -> *).
IsProblem prob m =>
prob -> Options m -> m (Set IntSet, Set IntSet)
run SimpleProblem Identity
forall {m :: * -> *}. SimpleProblem m
prob Options Identity
opt