{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
-- Copyright   :  (c) Masahiro Sakai 2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- * [GurvichKhachiyan1999] Vladimir Gurvich and Leonid Khachiyan,
--   On generating the irredundant conjunctive and disjunctive normal forms of monotone Boolean functions,
--   Discrete Applied Mathematics, vol. 96-97, pp. 363-373, 1999.
--   <http://www.sciencedirect.com/science/article/pii/S0166218X99000992>
--
-----------------------------------------------------------------------------
module ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
  (
  -- * Problem definition
    module ToySolver.Combinatorial.HittingSet.InterestingSets

  -- * Main functionality
  , run

  -- * Applications: monotone boolean functions
  , findPrimeImplicateOrPrimeImplicant
  , generateCNFAndDNF

  -- * Applicaitons: minimal hitting sets
  , minimalHittingSets
  , enumMinimalHittingSets
  ) 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 qualified ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996 as FredmanKhachiyan1996
import ToySolver.Combinatorial.HittingSet.InterestingSets

-- -----------------------------------------------------------------

-- | Given a problem and an option, it computes maximal interesting sets and
-- minimal uninteresting sets.
run :: forall m prob. IsProblem prob m => prob -> Options m -> m (Set IntSet, Set IntSet)
run :: forall (m :: * -> *) prob.
IsProblem prob m =>
prob -> Options m -> m (Set IntSet, Set IntSet)
run prob
prob Options m
opt = Set IntSet -> Set IntSet -> m (Set IntSet, Set IntSet)
loop (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map IntSet -> IntSet
complement (forall (m :: * -> *). Options m -> Set IntSet
optMaximalInterestingSets Options m
opt)) (forall (m :: * -> *). Options m -> Set IntSet
optMinimalUninterestingSets Options m
opt)
  where
    univ :: IntSet
    univ :: IntSet
univ = 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 -> m (Set IntSet, Set IntSet)
    loop :: Set IntSet -> Set IntSet -> m (Set IntSet, Set IntSet)
loop Set IntSet
comp_pos Set IntSet
neg = do
      case Set IntSet -> Set IntSet -> Maybe IntSet
FredmanKhachiyan1996.checkDuality Set IntSet
neg Set IntSet
comp_pos of
        Maybe IntSet
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map IntSet -> IntSet
complement Set IntSet
comp_pos, Set IntSet
neg)
        Just IntSet
xs -> do
          InterestingOrUninterestingSet
ret <- forall prob (m :: * -> *).
IsProblem prob m =>
prob -> IntSet -> m InterestingOrUninterestingSet
minimalUninterestingSetOrMaximalInterestingSet prob
prob IntSet
xs
          case InterestingOrUninterestingSet
ret of
            UninterestingSet IntSet
ys -> do
              forall (m :: * -> *). Options m -> IntSet -> m ()
optOnMinimalUninterestingSetFound Options m
opt IntSet
ys
              Set IntSet -> Set IntSet -> m (Set IntSet, Set IntSet)
loop Set IntSet
comp_pos (forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
ys Set IntSet
neg)
            InterestingSet IntSet
ys -> do
              forall (m :: * -> *). Options m -> IntSet -> m ()
optOnMaximalInterestingSetFound Options m
opt IntSet
ys
              Set IntSet -> Set IntSet -> m (Set IntSet, Set IntSet)
loop (forall a. Ord a => a -> Set a -> Set a
Set.insert (IntSet -> IntSet
complement IntSet
ys) Set IntSet
comp_pos) Set IntSet
neg

-- -----------------------------------------------------------------

-- | Find a new prime implicant or implicate.
--
-- Let /f/ be a monotone boolean function over set of variables /S/.
-- Let ∧_{I∈C} ∨_{i∈I} x_i and ∨_{I∈D} ∧_{i∈I} x_i be the irredundant
-- CNF representation /f/ and DNF representation of /f/ respectively.
--
-- Given a subset /C' ⊆ C/ and /D' ⊆ D/, @'findPrimeImplicateOrPrimeImplicant' S f C' D'@ returns
--
-- * @Just (Left I)@ where I ∈ C \\ C',
--
-- * @Just (Right I)@ where J ∈ D \\ D', or
--
-- * @Nothing@ if /C'=C/ and /D'=D/.
--
findPrimeImplicateOrPrimeImplicant
  :: 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/
  -> Maybe ImplicateOrImplicant
findPrimeImplicateOrPrimeImplicant :: IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> Maybe ImplicateOrImplicant
findPrimeImplicateOrPrimeImplicant IntSet
vs IntSet -> Bool
f Set IntSet
cs Set IntSet
ds = do
  IntSet
xs <- Set IntSet -> Set IntSet -> Maybe IntSet
FredmanKhachiyan1996.checkDuality Set IntSet
ds Set IntSet
cs
  let prob :: SimpleProblem m
prob = forall (m :: * -> *). IntSet -> (IntSet -> Bool) -> SimpleProblem m
SimpleProblem IntSet
vs (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Bool
f)
  case forall a. Identity a -> a
runIdentity (forall prob (m :: * -> *).
IsProblem prob m =>
prob -> IntSet -> m InterestingOrUninterestingSet
minimalUninterestingSetOrMaximalInterestingSet forall {m :: * -> *}. SimpleProblem m
prob IntSet
xs) of
    UninterestingSet IntSet
ys -> forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> ImplicateOrImplicant
Implicant IntSet
ys)
    InterestingSet IntSet
ys -> forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> ImplicateOrImplicant
Implicate (IntSet
vs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
ys))

-- | 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 = (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 = forall (m :: * -> *). IntSet -> (IntSet -> Bool) -> SimpleProblem m
SimpleProblem IntSet
vs (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Bool
f)
    opt :: Options Identity
opt = forall a. Default a => a
def
      { optMaximalInterestingSets :: Set IntSet
optMaximalInterestingSets = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet
vs IntSet -> IntSet -> IntSet
`IntSet.difference`) Set IntSet
cs
      , optMinimalUninterestingSets :: Set IntSet
optMinimalUninterestingSets = Set IntSet
ds
      }
    (Set IntSet
pos,Set IntSet
neg) = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) prob.
IsProblem prob m =>
prob -> Options m -> m (Set IntSet, Set IntSet)
run forall {m :: * -> *}. SimpleProblem m
prob Options Identity
opt

minimalHittingSets :: Set IntSet -> Set IntSet
minimalHittingSets :: Set IntSet -> Set IntSet
minimalHittingSets = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IntSet -> [IntSet]
enumMinimalHittingSets

enumMinimalHittingSets :: Set IntSet -> [IntSet]
enumMinimalHittingSets :: Set IntSet -> [IntSet]
enumMinimalHittingSets Set IntSet
dnf = Set IntSet -> [IntSet]
loop forall a. Set a
Set.empty
  where
    vs :: IntSet
vs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set IntSet
dnf
    f :: IntSet -> Bool
f = Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
dnf

    loop :: Set IntSet -> [IntSet]
    loop :: Set IntSet -> [IntSet]
loop Set IntSet
cs =
      case IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> Maybe ImplicateOrImplicant
findPrimeImplicateOrPrimeImplicant IntSet
vs IntSet -> Bool
f Set IntSet
cs Set IntSet
dnf of
        Maybe ImplicateOrImplicant
Nothing -> []
        Just (Implicate IntSet
c)  -> IntSet
c forall a. a -> [a] -> [a]
: Set IntSet -> [IntSet]
loop (forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
c Set IntSet
cs)
        Just (Implicant IntSet
_) -> forall a. HasCallStack => [Char] -> a
error [Char]
"GurvichKhachiyan1999.enumMinimalHittingSets: should not happen"

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

_evalCNF :: Set IntSet -> IntSet -> Bool
_evalCNF :: Set IntSet -> IntSet -> Bool
_evalCNF Set IntSet
cnf IntSet
xs = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ IntSet -> Bool
IntSet.null forall a b. (a -> b) -> a -> b
$ IntSet
is IntSet -> IntSet -> IntSet
`IntSet.intersection` IntSet
xs | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
cnf]


_f, _g :: Set IntSet
_f :: Set IntSet
_f = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map [Key] -> IntSet
IntSet.fromList [[Key
2,Key
4,Key
7], [Key
7,Key
8], [Key
9]]
_g :: Set IntSet
_g = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map [Key] -> IntSet
IntSet.fromList [[Key
7,Key
9], [Key
4,Key
8,Key
9], [Key
2,Key
8,Key
9]]

_testA1, _testA2, _testA3, _testA4 :: Maybe ImplicateOrImplicant
_testA1 :: Maybe ImplicateOrImplicant
_testA1 = IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> Maybe ImplicateOrImplicant
findPrimeImplicateOrPrimeImplicant ([Key] -> IntSet
IntSet.fromList [Key
2,Key
4,Key
7,Key
8,Key
9]) (Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
_f) forall a. Set a
Set.empty Set IntSet
_f
_testA2 :: Maybe ImplicateOrImplicant
_testA2 = IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> Maybe ImplicateOrImplicant
findPrimeImplicateOrPrimeImplicant ([Key] -> IntSet
IntSet.fromList [Key
2,Key
4,Key
7,Key
8,Key
9]) (Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
_f) (forall a. a -> Set a
Set.singleton ([Key] -> IntSet
IntSet.fromList [Key
2,Key
8,Key
9])) Set IntSet
_f
_testA3 :: Maybe ImplicateOrImplicant
_testA3 = IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> Maybe ImplicateOrImplicant
findPrimeImplicateOrPrimeImplicant ([Key] -> IntSet
IntSet.fromList [Key
2,Key
4,Key
7,Key
8,Key
9]) (Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
_f) (forall a. Ord a => [a] -> Set a
Set.fromList [[Key] -> IntSet
IntSet.fromList [Key
2,Key
8,Key
9], [Key] -> IntSet
IntSet.fromList [Key
4,Key
8,Key
9]]) Set IntSet
_f
_testA4 :: Maybe ImplicateOrImplicant
_testA4 = IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> Maybe ImplicateOrImplicant
findPrimeImplicateOrPrimeImplicant ([Key] -> IntSet
IntSet.fromList [Key
2,Key
4,Key
7,Key
8,Key
9]) (Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
_f) (forall a. Ord a => [a] -> Set a
Set.fromList [[Key] -> IntSet
IntSet.fromList [Key
2,Key
8,Key
9], [Key] -> IntSet
IntSet.fromList [Key
4,Key
8,Key
9], [Key] -> IntSet
IntSet.fromList [Key
7,Key
9]]) Set IntSet
_f

_testB1 :: Maybe ImplicateOrImplicant
_testB1 :: Maybe ImplicateOrImplicant
_testB1 = IntSet
-> (IntSet -> Bool)
-> Set IntSet
-> Set IntSet
-> Maybe ImplicateOrImplicant
findPrimeImplicateOrPrimeImplicant ([Key] -> IntSet
IntSet.fromList [Key
2,Key
4,Key
7,Key
8,Key
9]) (Set IntSet -> IntSet -> Bool
evalDNF Set IntSet
_f) Set IntSet
_g forall a. Set a
Set.empty