Copyright	(c) Masahiro Sakai 2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996

Contents

Main functions
Redundancy
Utilities for testing

Description

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

Synopsis

Main functions

areDualDNFs Source

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 Source

Synonym for checkDualityB.

checkDualityA Source

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 Source

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 Source

isRedundant F tests whether F contains redundant implicants.

deleteRedundancy :: Set IntSet -> Set IntSet Source

Removes redundant implicants from a given DNF.

Utilities for testing

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

occurFreq Source

Arguments

:: Fractional a
=> Int	a variable x
-> Set IntSet	a DNF F
-> a

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