{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
-- Copyright   :  (c) Masahiro Sakai 2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This modules provides functions to check whether two monotone boolean
-- functions /f/ and /g/ given in DNFs are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,¬xn)).
--
-- References:
--
-- * [FredmanKhachiyan1996] Michael L. Fredman and Leonid Khachiyan,
--   On the Complexicy of Dualization of Monotone Disjunctifve Normal Forms,
--   Journal of Algorithms, vol. 21, pp. 618-628, 1996.
--   <http://www.sciencedirect.com/science/article/pii/S0196677496900620>
--   <http://www.cs.tau.ac.il/~fiat/dmsem03/On%20the%20complexity%20of%20Dualization%20of%20monotone%20Disjunctive%20Normal%20Forms%20-%201996.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
  (
  -- * Main functions
    areDualDNFs
  , checkDuality
  , checkDualityA
  , checkDualityB

  -- * Redundancy
  -- $Redundancy
  , isRedundant
  , deleteRedundancy

  -- * Utilities for testing
  , isCounterExampleOf
  , occurFreq

  -- * Internal functions exported only for testing purpose
  , condition_1_1
  , condition_1_2
  , condition_1_3
  , condition_2_1
  , condition_1_1_solve
  , condition_1_2_solve
  , condition_1_3_solve
  , condition_2_1_solve
  ) where

import Prelude hiding (all, any)
import Control.Arrow ((***))
import Control.Exception (assert)
import Control.Monad
import Data.Foldable (all, any)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List hiding (all, any, intersect)
import Data.Maybe
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as Set

-- | xhi n ** xhi n == n
xhi :: Double -> Double
xhi :: Double -> Double
xhi Double
n = forall a. (a -> a) -> a -> [a]
iterate Double -> Double
f Double
m forall a. [a] -> Int -> a
!! Int
30
  where
    m :: Double
m = Double
logn forall a. Fractional a => a -> a -> a
/ forall a. Floating a => a -> a -> a
logBase Double
2 Double
logn
      where
        logn :: Double
logn = forall a. Floating a => a -> a -> a
logBase Double
2 Double
n
    f :: Double -> Double
f Double
x = Double
m forall a. Num a => a -> a -> a
* ((Double
logx forall a. Num a => a -> a -> a
+ forall a. Floating a => a -> a -> a
logBase Double
2 Double
logx) forall a. Fractional a => a -> a -> a
/ Double
logx)
      where
        logx :: Double
logx = forall a. Floating a => a -> a -> a
logBase Double
2 Double
x

disjoint :: IntSet -> IntSet -> Bool
disjoint :: IntSet -> IntSet -> Bool
disjoint IntSet
xs IntSet
ys = IntSet -> Bool
IntSet.null forall a b. (a -> b) -> a -> b
$ IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.intersection` IntSet
ys

intersect :: IntSet -> IntSet -> Bool
intersect :: IntSet -> IntSet -> Bool
intersect IntSet
xs IntSet
ys = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ IntSet -> IntSet -> Bool
disjoint IntSet
xs IntSet
ys

isHittingSetOf :: IntSet -> Set IntSet -> Bool
isHittingSetOf :: IntSet -> Set IntSet -> Bool
isHittingSetOf IntSet
xs Set IntSet
yss = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (IntSet
xs IntSet -> IntSet -> Bool
`intersect`) Set IntSet
yss

isCounterExampleOf :: IntSet -> (Set IntSet, Set IntSet) -> Bool
isCounterExampleOf :: IntSet -> (Set IntSet, Set IntSet) -> Bool
isCounterExampleOf IntSet
xs (Set IntSet
f,Set IntSet
g) = Bool
lhs forall a. Eq a => a -> a -> Bool
== Bool
rhs
  where
    lhs :: Bool
lhs = 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
f]
    rhs :: Bool
rhs = forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
xs IntSet -> IntSet -> Bool
`disjoint` IntSet
js | IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g]

_volume :: Set IntSet -> Set IntSet -> Int
_volume :: Set IntSet -> Set IntSet -> Int
_volume Set IntSet
f Set IntSet
g = forall a. Set a -> Int
Set.size Set IntSet
f forall a. Num a => a -> a -> a
* forall a. Set a -> Int
Set.size Set IntSet
g

condition_1_1 :: Set IntSet -> Set IntSet -> Bool
condition_1_1 :: Set IntSet -> Set IntSet -> Bool
condition_1_1 Set IntSet
f Set IntSet
g = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\IntSet
is -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\IntSet
js -> IntSet
is IntSet -> IntSet -> Bool
`intersect` IntSet
js) Set IntSet
g) Set IntSet
f

condition_1_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve Set IntSet
f Set IntSet
g = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ do
  IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f
  IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ IntSet
is IntSet -> IntSet -> Bool
`disjoint` IntSet
js
  forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
is

condition_1_2 :: Set IntSet -> Set IntSet -> Bool
condition_1_2 :: Set IntSet -> Set IntSet -> Bool
condition_1_2 Set IntSet
f Set IntSet
g = Set IntSet -> IntSet
h Set IntSet
f forall a. Eq a => a -> a -> Bool
== Set IntSet -> IntSet
h Set IntSet
g
  where
    h :: Set IntSet -> IntSet
h = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList

-- | Find @xs@ such that @xs `isCounterExampleOf` (f,g)@ unless @'condition_1_2' f g@.
condition_1_2_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_2_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_2_solve Set IntSet
f Set IntSet
g
  | Just (Int
v1,IntSet
_) <- IntSet -> Maybe (Int, IntSet)
IntSet.minView IntSet
d1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [Int -> IntSet -> IntSet
IntSet.delete Int
v1 IntSet
is | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f, Int
v1 Int -> IntSet -> Bool
`IntSet.member` IntSet
is]
  | Just (Int
v2,IntSet
_) <- IntSet -> Maybe (Int, IntSet)
IntSet.minView IntSet
d2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [(IntSet
vs IntSet -> IntSet -> IntSet
`IntSet.difference` (Int -> IntSet -> IntSet
IntSet.delete Int
v2 IntSet
js)) | IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g, Int
v2 Int -> IntSet -> Bool
`IntSet.member` IntSet
js]
  | Bool
otherwise = forall a. Maybe a
Nothing
  where
    f_vs :: IntSet
f_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
f
    g_vs :: IntSet
g_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
g
    vs :: IntSet
vs = IntSet
f_vs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
g_vs
    d1 :: IntSet
d1 = IntSet
f_vs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
g_vs
    d2 :: IntSet
d2 = IntSet
g_vs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
f_vs

condition_1_3 :: Set IntSet -> Set IntSet -> Bool
condition_1_3 :: Set IntSet -> Set IntSet -> Bool
condition_1_3 Set IntSet
f Set IntSet
g = Set IntSet -> Int
maxSize Set IntSet
f forall a. Ord a => a -> a -> Bool
<= forall a. Set a -> Int
Set.size Set IntSet
g Bool -> Bool -> Bool
&& Set IntSet -> Int
maxSize Set IntSet
g forall a. Ord a => a -> a -> Bool
<= forall a. Set a -> Int
Set.size Set IntSet
f
  where
    maxSize :: Set IntSet -> Int
maxSize Set IntSet
xs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Ord a => a -> a -> a
max Int
0 [IntSet -> Int
IntSet.size IntSet
i | IntSet
i <- forall a. Set a -> [a]
Set.toList Set IntSet
xs]

condition_1_3_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve Set IntSet
f Set IntSet
g = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$
  [forall a. [a] -> a
head [IntSet
is' | Int
i <- IntSet -> [Int]
IntSet.toList IntSet
is, let is' :: IntSet
is' = Int -> IntSet -> IntSet
IntSet.delete Int
i IntSet
is, IntSet
is' IntSet -> Set IntSet -> Bool
`isHittingSetOf` Set IntSet
g] | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f, IntSet -> Int
IntSet.size IntSet
is forall a. Ord a => a -> a -> Bool
> Int
g_size] forall a. [a] -> [a] -> [a]
++
  [IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` forall a. [a] -> a
head [IntSet
js' | Int
j <- IntSet -> [Int]
IntSet.toList IntSet
js, let js' :: IntSet
js' = Int -> IntSet -> IntSet
IntSet.delete Int
j IntSet
js, IntSet
js' IntSet -> Set IntSet -> Bool
`isHittingSetOf` Set IntSet
f] | IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g, IntSet -> Int
IntSet.size IntSet
js forall a. Ord a => a -> a -> Bool
> Int
f_size]
  where
    xs :: IntSet
xs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.union Set IntSet
f Set IntSet
g
    f_size :: Int
f_size = forall a. Set a -> Int
Set.size Set IntSet
f
    g_size :: Int
g_size = forall a. Set a -> Int
Set.size Set IntSet
g

e :: Set IntSet -> Set IntSet -> Rational
e :: Set IntSet -> Set IntSet -> Rational
e Set IntSet
f Set IntSet
g = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
1 forall a. Integral a => a -> a -> Ratio a
% (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ IntSet -> Int
IntSet.size IntSet
i) | IntSet
i <- forall a. Set a -> [a]
Set.toList Set IntSet
f] forall a. Num a => a -> a -> a
+
        forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
1 forall a. Integral a => a -> a -> Ratio a
% (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ IntSet -> Int
IntSet.size IntSet
j) | IntSet
j <- forall a. Set a -> [a]
Set.toList Set IntSet
g]

condition_2_1 :: Set IntSet -> Set IntSet -> Bool
condition_2_1 :: Set IntSet -> Set IntSet -> Bool
condition_2_1 Set IntSet
f Set IntSet
g = Set IntSet -> Set IntSet -> Rational
e Set IntSet
f Set IntSet
g forall a. Ord a => a -> a -> Bool
>= Rational
1

condition_2_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve Set IntSet
f Set IntSet
g =
  if Set IntSet -> Set IntSet -> Bool
condition_2_1 Set IntSet
f Set IntSet
g
  then forall a. Maybe a
Nothing
  else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop (IntSet -> [Int]
IntSet.toList IntSet
vs) Set IntSet
f Set IntSet
g IntSet
IntSet.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 forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.union Set IntSet
f Set IntSet
g

    loop :: [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
    loop :: [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop [] Set IntSet
_ Set IntSet
_ IntSet
ret = IntSet
ret
    loop (Int
v:[Int]
vs) Set IntSet
f Set IntSet
g IntSet
ret =
      if Set IntSet -> Set IntSet -> Rational
e Set IntSet
f1 Set IntSet
g1 forall a. Ord a => a -> a -> Bool
<= Set IntSet -> Set IntSet -> Rational
e Set IntSet
f2 Set IntSet
g2
      then [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop [Int]
vs Set IntSet
f1 Set IntSet
g1 (Int -> IntSet -> IntSet
IntSet.insert Int
v IntSet
ret)
      else [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop [Int]
vs Set IntSet
f2 Set IntSet
g2 IntSet
ret
      where
        -- f = x f1 ∨ f2
        -- g = x g2 ∨ g1
        f1 :: Set IntSet
f1 = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
v) Set IntSet
f
        g1 :: Set IntSet
g1 = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Int
v Int -> IntSet -> Bool
`IntSet.notMember`) Set IntSet
g
        f2 :: Set IntSet
f2 = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Int
v Int -> IntSet -> Bool
`IntSet.notMember`) Set IntSet
f
        g2 :: Set IntSet
g2 = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
v) Set IntSet
g

-- | @'isRedundant' F@ tests whether /F/ contains redundant implicants.
isRedundant :: Set IntSet -> Bool
isRedundant :: Set IntSet -> Bool
isRedundant = [IntSet] -> Bool
loop forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn IntSet -> Int
IntSet.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList
  where
    loop :: [IntSet] -> Bool
    loop :: [IntSet] -> Bool
loop [] = Bool
False
    loop (IntSet
xs:[IntSet]
yss) = forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
xs IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
ys | IntSet
ys <- [IntSet]
yss] Bool -> Bool -> Bool
|| [IntSet] -> Bool
loop [IntSet]
yss

isIrredundant :: Set IntSet -> Bool
isIrredundant :: Set IntSet -> Bool
isIrredundant = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IntSet -> Bool
isRedundant

-- | Removes redundant implicants from a given DNF.
deleteRedundancy :: Set IntSet -> Set IntSet
deleteRedundancy :: Set IntSet -> Set IntSet
deleteRedundancy = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Set IntSet -> IntSet -> Set IntSet
f forall a. Set a
Set.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn IntSet -> Int
IntSet.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList
  where
    f :: Set IntSet -> IntSet -> Set IntSet
    f :: Set IntSet -> IntSet -> Set IntSet
f Set IntSet
xss IntSet
ys =
      if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
ys) Set IntSet
xss
      then Set IntSet
xss
      else forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
ys Set IntSet
xss

-- | @occurFreq  x F@ computes /|{I∈F | x∈I}| \/ |F|/
occurFreq
  :: Fractional a
  => Int -- ^ a variable /x/
  -> Set IntSet -- ^ a DNF /F/
  -> a
occurFreq :: forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int
1 | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f, Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
is] :: Int) forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Set a -> Int
Set.size Set IntSet
f)

-- | @areDualDNFs f g@ checks whether two monotone boolean functions /f/
-- and /g/ are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,xn)).
--
-- Note that this function does not care about redundancy of DNFs.
--
-- Complexity: /O(n^o(log n))/ where @n = 'IntSet.size' f + 'IntSet.size' g@.
areDualDNFs
  :: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
  -> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
  -> Bool
areDualDNFs :: Set IntSet -> Set IntSet -> Bool
areDualDNFs Set IntSet
f Set IntSet
g = forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB Set IntSet
f Set IntSet
g

-- | Synonym for 'checkDualityB'.
checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDuality = Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB

-- | @checkDualityA f g@ checks whether two monotone boolean functions /f/
-- and /g/ are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,¬xn)) using
-- “Algorithm A” of [FredmanKhachiyan1996].
--
-- If they are indeed mutually dual it returns @Nothing@, otherwise
-- it returns @Just cs@ such that {xi ↦ (if xi∈cs then True else False) | i∈{1…n}}
-- is a solution of f(x1,…,xn) = g(¬x1,…,¬xn)).
--
-- Note that this function does not care about redundancy of DNFs.
--
-- Complexity: /O(n^O(log^2 n))/ where @n = 'IntSet.size' f + 'IntSet.size' g@.
checkDualityA
  :: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
  -> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
  -> Maybe IntSet
checkDualityA :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA Set IntSet
f Set IntSet
g
  | Just IntSet
xs <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
xs
  | Bool
otherwise = Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
f) (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
g)

checkDualityA' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' Set IntSet
f Set IntSet
g
  | forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Set IntSet -> Bool
isIrredundant Set IntSet
f Bool -> Bool -> Bool
&& Set IntSet -> Bool
isIrredundant Set IntSet
g) Bool
False = forall a. (?callStack::CallStack) => a
undefined
  | Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_2_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
  | Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
  | Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
  | Int
v forall a. Ord a => a -> a -> Bool
<= Int
1 = Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall Set IntSet
f Set IntSet
g
  | Bool
otherwise = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
      [ -- If x=0 then f(xs)=g(¬xs) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
        Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
      , -- If x=1 then f(xs)=g(¬xs) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs)
        forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
      ]
  where
    size_f :: Int
size_f = forall a. Set a -> Int
Set.size Set IntSet
f
    size_g :: Int
size_g = forall a. Set a -> Int
Set.size Set IntSet
g
    n :: Int
n = Int
size_f forall a. Num a => a -> a -> a
+ Int
size_g
    v :: Int
v = Int
size_f forall a. Num a => a -> a -> a
* Int
size_g
    xs :: IntSet
xs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set IntSet
f forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g
    epsilon :: Double
    epsilon :: Double
epsilon = Double
1 forall a. Fractional a => a -> a -> a
/ forall a. Floating a => a -> a -> a
logBase Double
2 (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)
    x :: Int
x = forall a. [a] -> a
head [Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs, forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f forall a. Ord a => a -> a -> Bool
>= Double
epsilon Bool -> Bool -> Bool
|| forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g forall a. Ord a => a -> a -> Bool
>= Double
epsilon]
    -- f = x f0 ∨ f1
    (Set IntSet
f0, Set IntSet
f1) = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
f
    -- g = x g0 ∨ g1
    (Set IntSet
g0, Set IntSet
g1) = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
g

solveSmall :: Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall :: Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall Set IntSet
f Set IntSet
g
  | forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Set IntSet -> Bool
isIrredundant Set IntSet
f Bool -> Bool -> Bool
&& Set IntSet -> Bool
isIrredundant Set IntSet
g) Bool
False = forall a. (?callStack::CallStack) => a
undefined
  | forall a. Set a -> Bool
Set.null Set IntSet
f Bool -> Bool -> Bool
&& forall a. Set a -> Bool
Set.null Set IntSet
g = forall a. a -> Maybe a
Just IntSet
IntSet.empty
  | forall a. Set a -> Bool
Set.null Set IntSet
f = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not (forall a. Set a -> Bool
Set.null Set IntSet
g)) forall a b. (a -> b) -> a -> b
$
      if IntSet
IntSet.empty forall a. Ord a => a -> Set a -> Bool
`Set.member` Set IntSet
g
      then forall a. Maybe a
Nothing
      else forall a. a -> Maybe a
Just (forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions (forall a. Set a -> [a]
Set.toList Set IntSet
g))
  | forall a. Set a -> Bool
Set.null Set IntSet
g = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not (forall a. Set a -> Bool
Set.null Set IntSet
f)) forall a b. (a -> b) -> a -> b
$
      if IntSet
IntSet.empty forall a. Ord a => a -> Set a -> Bool
`Set.member` Set IntSet
f
      then forall a. Maybe a
Nothing
      else forall a. a -> Maybe a
Just IntSet
IntSet.empty
  | Int
size_f forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Int
size_g forall a. Eq a => a -> a -> Bool
== Int
1 =
      let
        is :: IntSet
is = forall a. Set a -> a
Set.findMin Set IntSet
f
        js :: IntSet
js = forall a. Set a -> a
Set.findMin Set IntSet
g
        is_size :: Int
is_size = IntSet -> Int
IntSet.size IntSet
is
        js_size :: Int
js_size = IntSet -> Int
IntSet.size IntSet
js
      in if Int
is_size forall a. Eq a => a -> a -> Bool
== Int
1 then
           if Int
js_size forall a. Eq a => a -> a -> Bool
== Int
1 then
             forall a. Maybe a
Nothing
           else
             forall a. a -> Maybe a
Just (IntSet
js IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
is)
         else
           forall a. a -> Maybe a
Just (IntSet
is IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
js)
  | Bool
otherwise = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"should not happen"
  where
    size_f :: Int
size_f = forall a. Set a -> Int
Set.size Set IntSet
f
    size_g :: Int
size_g = forall a. Set a -> Int
Set.size Set IntSet
g

-- | @checkDualityB f g@ checks whether two monotone boolean functions /f/
-- and /g/ are mutually dual (i.e. f(x1,…,xn) = ¬g(¬x1,…,xn)) using
-- “Algorithm B” of [FredmanKhachiyan1996].
--
-- If they are indeed mutually dual it returns @Nothing@, otherwise
-- it returns @Just cs@ such that {xi ↦ (if xi∈cs then True else False) | i∈{1…n}}
-- is a solution of f(x1,…,xn) = g(¬x1,…,xn)).
--
-- Note that this function does not care about redundancy of DNFs.
--
-- Complexity: /O(n^o(log n))/ where @n = 'Set.size' f + 'Set.size' g@.
checkDualityB
  :: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
  -> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
  -> Maybe IntSet
checkDualityB :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB Set IntSet
f Set IntSet
g
  | Just IntSet
xs <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
xs
  | Bool
otherwise = Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
f) (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
g)

checkDualityB' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' Set IntSet
f Set IntSet
g
  | forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Set IntSet -> Bool
isIrredundant Set IntSet
f Bool -> Bool -> Bool
&& Set IntSet -> Bool
isIrredundant Set IntSet
g) Bool
False = forall a. (?callStack::CallStack) => a
undefined
  | Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_2_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
  | Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
  | Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
  | Int
v forall a. Ord a => a -> a -> Bool
<= Int
1 = Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall Set IntSet
f Set IntSet
g
--  | min size_f size_g <= 2 = undefined
  | Bool
otherwise =
      let x :: Int
x = forall a. [a] -> a
head [Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs, forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f forall a. Ord a => a -> a -> Bool
> (Rational
0::Rational), forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g forall a. Ord a => a -> a -> Bool
> (Rational
0::Rational)]
          -- f = x f0 ∨ f1
          (Set IntSet
f0, Set IntSet
f1) = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
f
          -- g = x g0 ∨ g1
          (Set IntSet
g0, Set IntSet
g1) = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
g
          epsilon_x_f :: Double
          epsilon_x_f :: Double
epsilon_x_f = forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f
          epsilon_x_g :: Double
          epsilon_x_g :: Double
epsilon_x_g = forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g
      in if Double
epsilon_x_f forall a. Ord a => a -> a -> Bool
<= Double
epsilon_v then
           forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
           [ {- f(xs ∪ {x↦0})=g(¬xs ∪ {x↦1}) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs). -}
             Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
           , {- f(¬xs ∪ {x↦1}) = g(xs ∪ {x↦0})
                ⇔ f0(¬xs) ∨ f1(¬xs) = g1(xs)
                ⇔ f0(¬xs) ∨ (¬g0(xs)∧¬g1(xs)) = g1(xs) {- duality of f1 and g0∨g1 -}
                ⇔ f0(¬xs) = g1(xs) and g0(xs) = 1
                   {- g0(xs)=0 is impossible, because
                      it implies f0(¬xs)∨¬g1(xs)=g1(xs) and then
                      f0(¬xs)=g1(xs)=1 which contradicts condition (1.1) -}
              -}
             forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall a b. (a -> b) -> a -> b
$ do
               IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g0
               let f' :: Set IntSet
f' = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (IntSet
js IntSet -> IntSet -> Bool
`disjoint`) Set IntSet
f0
                   g' :: Set IntSet
g' = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
js) Set IntSet
g1
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
                 IntSet
ys <- Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
g') (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
f')
                 let ys2 :: IntSet
ys2 = Int -> IntSet -> IntSet
IntSet.insert Int
x forall a b. (a -> b) -> a -> b
$ IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` (IntSet
js IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
ys)
                 forall a. (?callStack::CallStack) => Bool -> a -> a
assert (IntSet
ys2 IntSet -> (Set IntSet, Set IntSet) -> Bool
`isCounterExampleOf` (Set IntSet
f,Set IntSet
g)) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
ys2
           ]
         else if Double
epsilon_x_g forall a. Ord a => a -> a -> Bool
<= Double
epsilon_v then
           forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
           [ {- f(xs ∪ {x↦1}) = g(¬xs ∪ {x↦0})) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs). -}
             forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
           , {- f(xs ∪ {x↦0}) = g(¬xs ∪ {x↦1})
                ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
                ⇔ f1(xs) = g0(¬xs) ∨ (¬f0(xs)∧¬f1(xs))  {- duality of g1 and f0∨f1 -}
                ⇔ f1(xs) = g0(¬xs) and f0(xs) = 1
                   {- f0(xs)=0 is impossible, because
                      it implies f1(xs)=g0(¬xs)∨¬f1(xs) and then
                      f1(xs)=g0(¬xs)=1 which contradicts condition (1.1) -}
              -}
             forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall a b. (a -> b) -> a -> b
$ do
               IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f0
               let f' :: Set IntSet
f' = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
is) Set IntSet
f1
                   g' :: Set IntSet
g' = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (IntSet
is IntSet -> IntSet -> Bool
`disjoint`) Set IntSet
g0
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
                 IntSet
ys <- Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
f') (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
g')
                 let ys2 :: IntSet
ys2 = IntSet
is IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
ys
                 forall a. (?callStack::CallStack) => Bool -> a -> a
assert (IntSet
ys2 IntSet -> (Set IntSet, Set IntSet) -> Bool
`isCounterExampleOf` (Set IntSet
f,Set IntSet
g)) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
ys2
           ]
         else -- epsilon_v < min epsilon_x_f epsilon_x_g
           forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
           [ -- If x=0 then f(xs)=g(¬xs) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
             Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
           , -- If x=1 then f(xs)=g(¬xs) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs)
             forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
           ]
  where
    size_f :: Int
size_f = forall a. Set a -> Int
Set.size Set IntSet
f
    size_g :: Int
size_g = forall a. Set a -> Int
Set.size Set IntSet
g
    v :: Int
v = Int
size_f forall a. Num a => a -> a -> a
* Int
size_g
    epsilon_v :: Double
epsilon_v = Double
1 forall a. Fractional a => a -> a -> a
/ Double -> Double
xhi (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
v)
    xs :: IntSet
xs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set IntSet
f forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g

-- $Redundancy
-- An implicant /I∈F/ of a DNF /F/ is redundant if /F/ contains proper subset of /I/.
-- A DNF /F/ is called redundant if it contains redundant implicants.
-- The main functions of this modules does not care about redundancy of DNFs.