Class Library for Boolean Function Manipulation

Mila Sukalinska, Ivo Damianov

South-West University, Department of Computer Sciences

This is a class library fo Boolean Functions Manipulation developed in C#. The library can be easily used with languages from .NET Framework family as education and research tool. This class library for symbolic manipulation of Boolean functions provides various internal representations:

• Truth Table
• Formula
• OBDD

Internal Implementations

The functionality is derived into 2 parts - representation dependency properties and other properties which do not depend on internal representation. Every different implementation accomplish properties like:

• Reduce - method which reduces the current representation if it is possible
• Apply - Obtain new function applying some operation $\bigtriangledown$ between existing two other functions $f=f_1 \bigtriangledown f_2$
• Restrict - Replace variable with a constant $ f|_{x_i=b} $
• Compose - Replace variable with a function $ f_1|_{x_i=f_2} $

Implementation Independent Functionality

Some of the most popular and importat properties for researching are representation independent:

• Shannon Expansion - Boolean functions can be decomposed by means of the identity: $f=x.f|_x+x'.f|_{x'}$ where $f$ is any function and $f|_x$ and $f|_{x'}$ are positive and negative Shannon cofactors of $f$.
• Positive Davio $(f = xf_{1} \oplus f_{2})$ and Negative Davio $(f= xf_{1}\oplus f_{1}\oplus f_{2}=\overline{x}f_{1} \oplus f_{2})$
• Is Linear – checks if Boolean function is linear
• Monotonous – checks if Boolean function is monotonous
• Preserves 0 and Preserves 1
• Is Essential – checks if variable is Essential
• Separable Graph – returns all ordered separable pairs of variables

Convertors

The library defines 4 methods which implement convertion between different representation:

• Formula to Truth Table
• Truth Table to DNF (Disjunctive normal form)
• Truth Table to CNF (Conjunctive normal form)
• Truth Table to ANF (Algebraic normal form)
• Truth Table to BDD - the library contains UI coponent which helps to visualize the diagram

Download Link