msakai / toysolver / 767

Committed 22 May 2025 12:57PM UTC coverage: 71.847% (-0.06%) from 71.906%

Build # 767

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f4d92f6d1 into c10d256d2

Run Details

11104 of 15455 relevant lines covered (71.85%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

76.54

/src/ToySolver/Combinatorial/HittingSet/FredmanKhachiyan1996.hs

{-# 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 n = iterate f m !! 30
  where
    m = logn / logBase 2 logn
      where
        logn = logBase 2 n
    f x = m * ((logx + logBase 2 logx) / logx)
      where
        logx = logBase 2 x

disjoint :: IntSet -> IntSet -> Bool
disjoint xs ys = IntSet.null $ xs `IntSet.intersection` ys

intersect :: IntSet -> IntSet -> Bool
intersect xs ys = not $ disjoint xs ys

isHittingSetOf :: IntSet -> Set IntSet -> Bool
isHittingSetOf xs yss = all (xs `intersect`) yss

isCounterExampleOf :: IntSet -> (Set IntSet, Set IntSet) -> Bool
isCounterExampleOf xs (f,g) = lhs == rhs
  where
    lhs = or [is `IntSet.isSubsetOf` xs | is <- Set.toList f]
    rhs = or [xs `disjoint` js | js <- Set.toList g]

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

condition_1_1 :: Set IntSet -> Set IntSet -> Bool
condition_1_1 f g = all (\is -> all (\js -> is `intersect` js) g) f

condition_1_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve f g = listToMaybe $ do
  is <- Set.toList f
  js <- Set.toList g
  guard $ is `disjoint` js
  return is

condition_1_2 :: Set IntSet -> Set IntSet -> Bool
condition_1_2 f g = h f == h g
  where
    h = IntSet.unions . 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 f g
  | Just (v1,_) <- IntSet.minView d1 = Just $ head [IntSet.delete v1 is | is <- Set.toList f, v1 `IntSet.member` is]
  | Just (v2,_) <- IntSet.minView d2 = Just $ head [(vs `IntSet.difference` (IntSet.delete v2 js)) | js <- Set.toList g, v2 `IntSet.member` js]
  | otherwise = Nothing
  where
    f_vs = IntSet.unions $ Set.toList f
    g_vs = IntSet.unions $ Set.toList g
    vs = f_vs `IntSet.union` g_vs
    d1 = f_vs `IntSet.difference` g_vs
    d2 = g_vs `IntSet.difference` f_vs

condition_1_3 :: Set IntSet -> Set IntSet -> Bool
condition_1_3 f g = maxSize f <= Set.size g && maxSize g <= Set.size f
  where
    maxSize xs = foldl' max 0 [IntSet.size i | i <- Set.toList xs]

condition_1_3_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve f g = listToMaybe $
  [head [is' | i <- IntSet.toList is, let is' = IntSet.delete i is, is' `isHittingSetOf` g] | is <- Set.toList f, IntSet.size is > g_size] ++
  [xs `IntSet.difference` head [js' | j <- IntSet.toList js, let js' = IntSet.delete j js, js' `isHittingSetOf` f] | js <- Set.toList g, IntSet.size js > f_size]
  where
    xs = IntSet.unions $ Set.toList $ Set.union f g
    f_size = Set.size f
    g_size = Set.size g

e :: Set IntSet -> Set IntSet -> Rational
e f g = sum [1 % (2 ^ IntSet.size i) | i <- Set.toList f] +
        sum [1 % (2 ^ IntSet.size j) | j <- Set.toList g]

condition_2_1 :: Set IntSet -> Set IntSet -> Bool
condition_2_1 f g = e f g >= 1

condition_2_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve f g =
  if condition_2_1 f g
  then Nothing
  else Just $ loop (IntSet.toList vs) f g IntSet.empty
  where
    vs = IntSet.unions $ Set.toList $ Set.union f g

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

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

isIrredundant :: Set IntSet -> Bool
isIrredundant = not . isRedundant

-- | Removes redundant implicants from a given DNF.
deleteRedundancy :: Set IntSet -> Set IntSet
deleteRedundancy = foldl' f Set.empty . sortOn IntSet.size . Set.toList
  where
    f :: Set IntSet -> IntSet -> Set IntSet
    f xss ys =
      if any (`IntSet.isSubsetOf` ys) xss
      then xss
      else Set.insert ys xss

-- | @occurFreq  x F@ computes /|{I∈F | x∈I}| \/ |F|/
occurFreq
  :: Fractional a
  => Int -- ^ a variable /x/
  -> Set IntSet -- ^ a DNF /F/
  -> a
occurFreq x f = fromIntegral (sum [1 | is <- Set.toList f, x `IntSet.member` is] :: Int) / fromIntegral (Set.size 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 f g = isNothing $ checkDualityB f g

-- | Synonym for 'checkDualityB'.
checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDuality = 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 f g
  | Just xs <- condition_1_1_solve f g = Just xs
  | otherwise = checkDualityA' (deleteRedundancy f) (deleteRedundancy g)

checkDualityA' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' f g
  | assert (isIrredundant f && isIrredundant g) False = undefined
  | Just s <- condition_1_2_solve f g = Just s
  | Just s <- condition_1_3_solve f g = Just s
  | Just s <- condition_2_1_solve f g = Just s
  | v <= 1 = solveSmall f g
  | otherwise = msum
      [ -- If x=0 then f(xs)=g(¬xs) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
        checkDualityA' f1 (deleteRedundancy (g0 `Set.union` g1))
      , -- If x=1 then f(xs)=g(¬xs) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs)
        liftM (IntSet.insert x) $ checkDualityA' (deleteRedundancy (f0 `Set.union` f1)) g1
      ]
  where
    size_f = Set.size f
    size_g = Set.size g
    n = size_f + size_g
    v = size_f * size_g
    xs = IntSet.unions $ Set.toList $ f `Set.union` g
    epsilon :: Double
    epsilon = 1 / logBase 2 (fromIntegral n)
    x = head [x | x <- IntSet.toList xs, occurFreq x f >= epsilon || occurFreq x g >= epsilon]
    -- f = x f0 ∨ f1
    (f0, f1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) f
    -- g = x g0 ∨ g1
    (g0, g1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) g

solveSmall :: Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall f g
  | assert (isIrredundant f && isIrredundant g) False = undefined
  | Set.null f && Set.null g = Just IntSet.empty
  | Set.null f = assert (not (Set.null g)) $
      if IntSet.empty `Set.member` g
      then Nothing
      else Just (IntSet.unions (Set.toList g))
  | Set.null g = assert (not (Set.null f)) $
      if IntSet.empty `Set.member` f
      then Nothing
      else Just IntSet.empty
  | size_f == 1 && size_g == 1 =
      let
        is = Set.findMin f
        js = Set.findMin g
        is_size = IntSet.size is
        js_size = IntSet.size js
      in if is_size == 1 then
           if js_size == 1 then
             Nothing
           else
             Just (js `IntSet.difference` is)
         else
           Just (is `IntSet.difference` js)
  | otherwise = error "should not happen"
  where
    size_f = Set.size f
    size_g = Set.size 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 f g
  | Just xs <- condition_1_1_solve f g = Just xs
  | otherwise = checkDualityB' (deleteRedundancy f) (deleteRedundancy g)

checkDualityB' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' f g
  | assert (isIrredundant f && isIrredundant g) False = undefined
  | Just s <- condition_1_2_solve f g = Just s
  | Just s <- condition_1_3_solve f g = Just s
  | Just s <- condition_2_1_solve f g = Just s
  | v <= 1 = solveSmall f g
--  | min size_f size_g <= 2 = undefined
  | otherwise =
      let x = head [x | x <- IntSet.toList xs, occurFreq x f > (0::Rational), occurFreq x g > (0::Rational)]
          -- f = x f0 ∨ f1
          (f0, f1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) f
          -- g = x g0 ∨ g1
          (g0, g1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) g
          epsilon_x_f :: Double
          epsilon_x_f = occurFreq x f
          epsilon_x_g :: Double
          epsilon_x_g = occurFreq x g
      in if epsilon_x_f <= epsilon_v then
           msum
           [ {- f(xs ∪ {x↦0})=g(¬xs ∪ {x↦1}) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs). -}
             checkDualityB' f1 (deleteRedundancy (g0 `Set.union` 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) -}
              -}
             msum $ do
               js <- Set.toList g0
               let f' = Set.filter (js `disjoint`) f0
                   g' = Set.map (`IntSet.difference` js) g1
               return $ do
                 ys <- checkDualityB' (deleteRedundancy g') (deleteRedundancy f')
                 let ys2 = IntSet.insert x $ xs `IntSet.difference` (js `IntSet.union` ys)
                 assert (ys2 `isCounterExampleOf` (f,g)) $ return ()
                 return ys2
           ]
         else if epsilon_x_g <= epsilon_v then
           msum
           [ {- f(xs ∪ {x↦1}) = g(¬xs ∪ {x↦0})) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs). -}
             liftM (IntSet.insert x) $ checkDualityB' (deleteRedundancy (f0 `Set.union` f1)) 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) -}
              -}
             msum $ do
               is <- Set.toList f0
               let f' = Set.map (`IntSet.difference` is) f1
                   g' = Set.filter (is `disjoint`) g0
               return $ do
                 ys <- checkDualityB' (deleteRedundancy f') (deleteRedundancy g')
                 let ys2 = is `IntSet.union` ys
                 assert (ys2 `isCounterExampleOf` (f,g)) $ return ()
                 return ys2
           ]
         else -- epsilon_v < min epsilon_x_f epsilon_x_g
           msum
           [ -- If x=0 then f(xs)=g(¬xs) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
             checkDualityB' f1 (deleteRedundancy (g0 `Set.union` g1))
           , -- If x=1 then f(xs)=g(¬xs) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs)
             liftM (IntSet.insert x) $ checkDualityB' (deleteRedundancy (f0 `Set.union` f1)) g1
           ]
  where
    size_f = Set.size f
    size_g = Set.size g
    v = size_f * size_g
    epsilon_v = 1 / xhi (fromIntegral v)
    xs = IntSet.unions $ Set.toList $ f `Set.union` 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.

1	{-# OPTIONS_GHC -Wall #-}
2	-----------------------------------------------------------------------------
3	-- \|
4	-- Module : ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
5	-- Copyright : (c) Masahiro Sakai 2015
6	-- License : BSD-style
7	--
8	-- Maintainer : masahiro.sakai@gmail.com
9	-- Stability : provisional
10	-- Portability : portable
11	--
12	-- This modules provides functions to check whether two monotone boolean
13	-- functions /f/ and /g/ given in DNFs are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,¬xn)).
14	--
15	-- References:
16	--
17	-- * [FredmanKhachiyan1996] Michael L. Fredman and Leonid Khachiyan,
18	-- On the Complexicy of Dualization of Monotone Disjunctifve Normal Forms,
19	-- Journal of Algorithms, vol. 21, pp. 618-628, 1996.
20	-- <http://www.sciencedirect.com/science/article/pii/S0196677496900620>
21	-- <http://www.cs.tau.ac.il/~fiat/dmsem03/On%20the%20complexity%20of%20Dualization%20of%20monotone%20Disjunctive%20Normal%20Forms%20-%201996.pdf>
22	--
23	-----------------------------------------------------------------------------
24	module ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
25	(
26	-- * Main functions
27	areDualDNFs
28	, checkDuality
29	, checkDualityA
30	, checkDualityB
31
32	-- * Redundancy
33	-- $Redundancy
34	, isRedundant
35	, deleteRedundancy
36
37	-- * Utilities for testing
38	, isCounterExampleOf
39	, occurFreq
40
41	-- * Internal functions exported only for testing purpose
42	, condition_1_1
43	, condition_1_2
44	, condition_1_3
45	, condition_2_1
46	, condition_1_1_solve
47	, condition_1_2_solve
48	, condition_1_3_solve
49	, condition_2_1_solve
50	) where
51
52	import Prelude hiding (all, any)
53	import Control.Arrow ((***))
54	import Control.Exception (assert)
55	import Control.Monad
56	import Data.Foldable (all, any)
57	import Data.IntSet (IntSet)
58	import qualified Data.IntSet as IntSet
59	import Data.List hiding (all, any, intersect)
60	import Data.Maybe
61	import Data.Ratio
62	import Data.Set (Set)
63	import qualified Data.Set as Set
64
65	-- \| xhi n ** xhi n == n
66	xhi :: Double -> Double
67	xhi n = iterate f m !! 30	1✔
68	where
69	m = logn / logBase 2 logn	1✔
70	where
71	logn = logBase 2 n	1✔
72	f x = m * ((logx + logBase 2 logx) / logx)	1✔
73	where
74	logx = logBase 2 x	1✔
75
76	disjoint :: IntSet -> IntSet -> Bool
77	disjoint xs ys = IntSet.null $ xs `IntSet.intersection` ys	1✔
78
79	intersect :: IntSet -> IntSet -> Bool
80	intersect xs ys = not $ disjoint xs ys	1✔
81
82	isHittingSetOf :: IntSet -> Set IntSet -> Bool
83	isHittingSetOf xs yss = all (xs `intersect`) yss	1✔
84
85	isCounterExampleOf :: IntSet -> (Set IntSet, Set IntSet) -> Bool
86	isCounterExampleOf xs (f,g) = lhs == rhs	1✔
87	where
88	lhs = or [is `IntSet.isSubsetOf` xs \| is <- Set.toList f]	1✔
89	rhs = or [xs `disjoint` js \| js <- Set.toList g]	1✔
90
91	_volume :: Set IntSet -> Set IntSet -> Int
92	_volume f g = Set.size f * Set.size g	×
93
94	condition_1_1 :: Set IntSet -> Set IntSet -> Bool
95	condition_1_1 f g = all (\is -> all (\js -> is `intersect` js) g) f	×
96
97	condition_1_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
98	condition_1_1_solve f g = listToMaybe $ do	1✔
99	is <- Set.toList f	1✔
100	js <- Set.toList g	1✔
101	guard $ is `disjoint` js	1✔
102	return is	1✔
103
104	condition_1_2 :: Set IntSet -> Set IntSet -> Bool
105	condition_1_2 f g = h f == h g	×
106	where
107	h = IntSet.unions . Set.toList	×
108
109	-- \| Find @xs@ such that @xs `isCounterExampleOf` (f,g)@ unless @'condition_1_2' f g@.
110	condition_1_2_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
111	condition_1_2_solve f g	1✔
112	\| Just (v1,_) <- IntSet.minView d1 = Just $ head [IntSet.delete v1 is \| is <- Set.toList f, v1 `IntSet.member` is]	1✔
113	\| Just (v2,_) <- IntSet.minView d2 = Just $ head [(vs `IntSet.difference` (IntSet.delete v2 js)) \| js <- Set.toList g, v2 `IntSet.member` js]	1✔
114	\| otherwise = Nothing	×
115	where
116	f_vs = IntSet.unions $ Set.toList f	1✔
117	g_vs = IntSet.unions $ Set.toList g	1✔
118	vs = f_vs `IntSet.union` g_vs	1✔
119	d1 = f_vs `IntSet.difference` g_vs	1✔
120	d2 = g_vs `IntSet.difference` f_vs	1✔
121
122	condition_1_3 :: Set IntSet -> Set IntSet -> Bool
123	condition_1_3 f g = maxSize f <= Set.size g && maxSize g <= Set.size f	×
124	where
125	maxSize xs = foldl' max 0 [IntSet.size i \| i <- Set.toList xs]	×
126
127	condition_1_3_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
128	condition_1_3_solve f g = listToMaybe $	1✔
129	[head [is' \| i <- IntSet.toList is, let is' = IntSet.delete i is, is' `isHittingSetOf` g] \| is <- Set.toList f, IntSet.size is > g_size] ++	1✔
130	[xs `IntSet.difference` head [js' \| j <- IntSet.toList js, let js' = IntSet.delete j js, js' `isHittingSetOf` f] \| js <- Set.toList g, IntSet.size js > f_size]	1✔
131	where
132	xs = IntSet.unions $ Set.toList $ Set.union f g	1✔
133	f_size = Set.size f	1✔
134	g_size = Set.size g	1✔
135
136	e :: Set IntSet -> Set IntSet -> Rational
137	e f g = sum [1 % (2 ^ IntSet.size i) \| i <- Set.toList f] +	1✔
138	sum [1 % (2 ^ IntSet.size j) \| j <- Set.toList g]	1✔
139
140	condition_2_1 :: Set IntSet -> Set IntSet -> Bool
141	condition_2_1 f g = e f g >= 1	1✔
142
143	condition_2_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
144	condition_2_1_solve f g =	1✔
145	if condition_2_1 f g	1✔
146	then Nothing	1✔
147	else Just $ loop (IntSet.toList vs) f g IntSet.empty	1✔
148	where
149	vs = IntSet.unions $ Set.toList $ Set.union f g	1✔
150
151	loop :: [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
152	loop [] _ _ ret = ret	1✔
153	loop (v:vs) f g ret =
154	if e f1 g1 <= e f2 g2	1✔
155	then loop vs f1 g1 (IntSet.insert v ret)	1✔
156	else loop vs f2 g2 ret	1✔
157	where
158	-- f = x f1 ∨ f2
159	-- g = x g2 ∨ g1
160	f1 = Set.map (IntSet.delete v) f	1✔
161	g1 = Set.filter (v `IntSet.notMember`) g	1✔
162	f2 = Set.filter (v `IntSet.notMember`) f	1✔
163	g2 = Set.map (IntSet.delete v) g	1✔
164
165	-- \| @'isRedundant' F@ tests whether /F/ contains redundant implicants.
166	isRedundant :: Set IntSet -> Bool
167	isRedundant = loop . sortOn IntSet.size . Set.toList	×
168	where
169	loop :: [IntSet] -> Bool
170	loop [] = False	×
171	loop (xs:yss) = or [xs `IntSet.isSubsetOf` ys \| ys <- yss] \|\| loop yss	×
172
173	isIrredundant :: Set IntSet -> Bool
174	isIrredundant = not . isRedundant	×
175
176	-- \| Removes redundant implicants from a given DNF.
177	deleteRedundancy :: Set IntSet -> Set IntSet
178	deleteRedundancy = foldl' f Set.empty . sortOn IntSet.size . Set.toList	1✔
179	where
180	f :: Set IntSet -> IntSet -> Set IntSet
181	f xss ys =	1✔
182	if any (`IntSet.isSubsetOf` ys) xss	1✔
183	then xss	1✔
184	else Set.insert ys xss	1✔
185
186	-- \| @occurFreq x F@ computes /\|{I∈F \| x∈I}\| \/ \|F\|/
187	occurFreq
188	:: Fractional a
189	=> Int -- ^ a variable /x/
190	-> Set IntSet -- ^ a DNF /F/
191	-> a
192	occurFreq x f = fromIntegral (sum [1 \| is <- Set.toList f, x `IntSet.member` is] :: Int) / fromIntegral (Set.size f)	1✔
193
194	-- \| @areDualDNFs f g@ checks whether two monotone boolean functions /f/
195	-- and /g/ are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,xn)).
196	--
197	-- Note that this function does not care about redundancy of DNFs.
198	--
199	-- Complexity: /O(n^o(log n))/ where @n = 'IntSet.size' f + 'IntSet.size' g@.
200	areDualDNFs
201	:: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
202	-> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
203	-> Bool
204	areDualDNFs f g = isNothing $ checkDualityB f g	×
205
206	-- \| Synonym for 'checkDualityB'.
207	checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet
208	checkDuality = checkDualityB	1✔
209
210	-- \| @checkDualityA f g@ checks whether two monotone boolean functions /f/
211	-- and /g/ are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,¬xn)) using
212	-- “Algorithm A” of [FredmanKhachiyan1996].
213	--
214	-- If they are indeed mutually dual it returns @Nothing@, otherwise
215	-- it returns @Just cs@ such that {xi ↦ (if xi∈cs then True else False) \| i∈{1…n}}
216	-- is a solution of f(x1,…,xn) = g(¬x1,…,¬xn)).
217	--
218	-- Note that this function does not care about redundancy of DNFs.
219	--
220	-- Complexity: /O(n^O(log^2 n))/ where @n = 'IntSet.size' f + 'IntSet.size' g@.
221	checkDualityA
222	:: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
223	-> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
224	-> Maybe IntSet
225	checkDualityA f g	1✔
226	\| Just xs <- condition_1_1_solve f g = Just xs	1✔
227	\| otherwise = checkDualityA' (deleteRedundancy f) (deleteRedundancy g)	×
228
229	checkDualityA' :: Set IntSet -> Set IntSet -> Maybe IntSet
230	checkDualityA' f g	1✔
231	\| assert (isIrredundant f && isIrredundant g) False = undefined	×
232	\| Just s <- condition_1_2_solve f g = Just s	1✔
233	\| Just s <- condition_1_3_solve f g = Just s	×
234	\| Just s <- condition_2_1_solve f g = Just s	×
235	\| v <= 1 = solveSmall f g	1✔
236	\| otherwise = msum	×
237	[ -- If x=0 then f(xs)=g(¬xs) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)	1✔
238	checkDualityA' f1 (deleteRedundancy (g0 `Set.union` g1))	1✔
239	, -- If x=1 then f(xs)=g(¬xs) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs)
240	liftM (IntSet.insert x) $ checkDualityA' (deleteRedundancy (f0 `Set.union` f1)) g1	×
241	]
242	where
243	size_f = Set.size f	1✔
244	size_g = Set.size g	1✔
245	n = size_f + size_g	1✔
246	v = size_f * size_g	1✔
247	xs = IntSet.unions $ Set.toList $ f `Set.union` g	1✔
248	epsilon :: Double
249	epsilon = 1 / logBase 2 (fromIntegral n)	1✔
250	x = head [x \| x <- IntSet.toList xs, occurFreq x f >= epsilon \|\| occurFreq x g >= epsilon]	1✔
251	-- f = x f0 ∨ f1
252	(f0, f1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) f	1✔
253	-- g = x g0 ∨ g1
254	(g0, g1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) g	1✔
255
256	solveSmall :: Set IntSet -> Set IntSet -> Maybe IntSet
257	solveSmall f g	1✔
258	\| assert (isIrredundant f && isIrredundant g) False = undefined	×
259	\| Set.null f && Set.null g = Just IntSet.empty	×
260	\| Set.null f = assert (not (Set.null g)) $	×
261	if IntSet.empty `Set.member` g	×
262	then Nothing	1✔
263	else Just (IntSet.unions (Set.toList g))	×
264	\| Set.null g = assert (not (Set.null f)) $	×
265	if IntSet.empty `Set.member` f	×
266	then Nothing	1✔
267	else Just IntSet.empty	×
268	\| size_f == 1 && size_g == 1 =	×
269	let	1✔
270	is = Set.findMin f	1✔
271	js = Set.findMin g	1✔
272	is_size = IntSet.size is	1✔
273	js_size = IntSet.size js	1✔
274	in if is_size == 1 then	×
275	if js_size == 1 then	×
276	Nothing	1✔
277	else
278	Just (js `IntSet.difference` is)	×
279	else
280	Just (is `IntSet.difference` js)	×
281	\| otherwise = error "should not happen"	×
282	where
283	size_f = Set.size f	1✔
284	size_g = Set.size g	1✔
285
286	-- \| @checkDualityB f g@ checks whether two monotone boolean functions /f/
287	-- and /g/ are mutually dual (i.e. f(x1,…,xn) = ¬g(¬x1,…,xn)) using
288	-- “Algorithm B” of [FredmanKhachiyan1996].
289	--
290	-- If they are indeed mutually dual it returns @Nothing@, otherwise
291	-- it returns @Just cs@ such that {xi ↦ (if xi∈cs then True else False) \| i∈{1…n}}
292	-- is a solution of f(x1,…,xn) = g(¬x1,…,xn)).
293	--
294	-- Note that this function does not care about redundancy of DNFs.
295	--
296	-- Complexity: /O(n^o(log n))/ where @n = 'Set.size' f + 'Set.size' g@.
297	checkDualityB
298	:: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
299	-> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
300	-> Maybe IntSet
301	checkDualityB f g	1✔
302	\| Just xs <- condition_1_1_solve f g = Just xs	1✔
303	\| otherwise = checkDualityB' (deleteRedundancy f) (deleteRedundancy g)	×
304
305	checkDualityB' :: Set IntSet -> Set IntSet -> Maybe IntSet
306	checkDualityB' f g	1✔
307	\| assert (isIrredundant f && isIrredundant g) False = undefined	×
308	\| Just s <- condition_1_2_solve f g = Just s	1✔
309	\| Just s <- condition_1_3_solve f g = Just s	1✔
310	\| Just s <- condition_2_1_solve f g = Just s	1✔
311	\| v <= 1 = solveSmall f g	1✔
312	-- \| min size_f size_g <= 2 = undefined
313	\| otherwise =	×
314	let x = head [x \| x <- IntSet.toList xs, occurFreq x f > (0::Rational), occurFreq x g > (0::Rational)]	×
315	-- f = x f0 ∨ f1
316	(f0, f1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) f	1✔
317	-- g = x g0 ∨ g1
318	(g0, g1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) g	1✔
319	epsilon_x_f :: Double
320	epsilon_x_f = occurFreq x f	1✔
321	epsilon_x_g :: Double
322	epsilon_x_g = occurFreq x g	1✔
323	in if epsilon_x_f <= epsilon_v then	1✔
324	msum	1✔
325	[ {- f(xs ∪ {x↦0})=g(¬xs ∪ {x↦1}) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs). -}	1✔
326	checkDualityB' f1 (deleteRedundancy (g0 `Set.union` g1))	1✔
327	, {- f(¬xs ∪ {x↦1}) = g(xs ∪ {x↦0})
328	⇔ f0(¬xs) ∨ f1(¬xs) = g1(xs)
329	⇔ f0(¬xs) ∨ (¬g0(xs)∧¬g1(xs)) = g1(xs) {- duality of f1 and g0∨g1 -}
330	⇔ f0(¬xs) = g1(xs) and g0(xs) = 1
331	{- g0(xs)=0 is impossible, because
332	it implies f0(¬xs)∨¬g1(xs)=g1(xs) and then
333	f0(¬xs)=g1(xs)=1 which contradicts condition (1.1) -}
334	-}
335	msum $ do	1✔
336	js <- Set.toList g0	1✔
337	let f' = Set.filter (js `disjoint`) f0	1✔
338	g' = Set.map (`IntSet.difference` js) g1	1✔
339	return $ do	1✔
340	ys <- checkDualityB' (deleteRedundancy g') (deleteRedundancy f')	1✔
341	let ys2 = IntSet.insert x $ xs `IntSet.difference` (js `IntSet.union` ys)	1✔
342	assert (ys2 `isCounterExampleOf` (f,g)) $ return ()	×
343	return ys2	1✔
344	]
345	else if epsilon_x_g <= epsilon_v then	1✔
346	msum	1✔
347	[ {- f(xs ∪ {x↦1}) = g(¬xs ∪ {x↦0})) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs). -}	1✔
348	liftM (IntSet.insert x) $ checkDualityB' (deleteRedundancy (f0 `Set.union` f1)) g1	1✔
349	, {- f(xs ∪ {x↦0}) = g(¬xs ∪ {x↦1})
350	⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
351	⇔ f1(xs) = g0(¬xs) ∨ (¬f0(xs)∧¬f1(xs)) {- duality of g1 and f0∨f1 -}
352	⇔ f1(xs) = g0(¬xs) and f0(xs) = 1
353	{- f0(xs)=0 is impossible, because
354	it implies f1(xs)=g0(¬xs)∨¬f1(xs) and then
355	f1(xs)=g0(¬xs)=1 which contradicts condition (1.1) -}
356	-}
357	msum $ do	1✔
358	is <- Set.toList f0	1✔
359	let f' = Set.map (`IntSet.difference` is) f1	1✔
360	g' = Set.filter (is `disjoint`) g0	1✔
361	return $ do	1✔
362	ys <- checkDualityB' (deleteRedundancy f') (deleteRedundancy g')	1✔
363	let ys2 = is `IntSet.union` ys	1✔
364	assert (ys2 `isCounterExampleOf` (f,g)) $ return ()	×
365	return ys2	1✔
366	]
367	else -- epsilon_v < min epsilon_x_f epsilon_x_g
368	msum	1✔
369	[ -- If x=0 then f(xs)=g(¬xs) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)	1✔
370	checkDualityB' f1 (deleteRedundancy (g0 `Set.union` g1))	1✔
371	, -- If x=1 then f(xs)=g(¬xs) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs)
372	liftM (IntSet.insert x) $ checkDualityB' (deleteRedundancy (f0 `Set.union` f1)) g1	1✔
373	]
374	where
375	size_f = Set.size f	1✔
376	size_g = Set.size g	1✔
377	v = size_f * size_g	1✔
378	epsilon_v = 1 / xhi (fromIntegral v)	1✔
379	xs = IntSet.unions $ Set.toList $ f `Set.union` g	1✔
380
381	-- $Redundancy
382	-- An implicant /I∈F/ of a DNF /F/ is redundant if /F/ contains proper subset of /I/.
383	-- A DNF /F/ is called redundant if it contains redundant implicants.
384	-- The main functions of this modules does not care about redundancy of DNFs.

msakai / toysolver / 767

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous