ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996

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

Main functions

areDualDNFs

Arguments

:: Set IntSet

a monotone boolean function f given in DNF

-> Set IntSet

a monotone boolean function g given in DNF

-> Bool

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 = size f + size g.

checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet

Synonym for checkDualityB.

checkDualityA

Arguments

:: 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 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 = size f + size g.

checkDualityB

Arguments

:: Set IntSet

a monotone boolean function f given in DNF

-> Set IntSet

a monotone boolean function f given in DNF

-> Maybe IntSet

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 = size f + size 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.

isRedundant :: Set IntSet -> Bool

isRedundant F tests whether F contains redundant implicants.

deleteRedundancy :: Set IntSet -> Set IntSet

Removes redundant implicants from a given DNF.

Utilities for testing

isCounterExampleOf :: IntSet -> (Set IntSet, Set IntSet) -> Bool

occurFreq

Arguments

:: Fractional a

=> Int

a variable x

-> Set IntSet

a DNF F

-> a

occurFreq x F computes |{I∈F | x∈I}| / |F|

Internal functions exported only for testing purpose

condition_1_1 :: Set IntSet -> Set IntSet -> Bool

condition_1_2 :: Set IntSet -> Set IntSet -> Bool

condition_1_3 :: Set IntSet -> Set IntSet -> Bool

condition_2_1 :: Set IntSet -> Set IntSet -> Bool

condition_1_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet

condition_1_2_solve :: Set IntSet -> Set IntSet -> Maybe IntSet

Find xs such that xs isCounterExampleOf (f,g) unless condition_1_2 f g.

condition_1_3_solve :: Set IntSet -> Set IntSet -> Maybe IntSet

condition_2_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet