OKlibrary  0.2.1.6
BDDs.hpp File Reference

Plans regarding BDDs and variations. More...

Go to the source code of this file.


Detailed Description

Plans regarding BDDs and variations.

Todo:
Connections
Todo:
Basic operations for boolean functions
  • We need the notion of a boolean function as a simple term (which can be put into a set).
  • We actually need "formal boolean functions", which depend on a set of (named) variables; or perhaps just natural numbers are enough to represent variables.
  • We need application of partial assignments to formal boolean functions.
  • We need elimination of variables on which the formal boolean function does not depend.
  • We need computation of forced assignments.
Todo:
OBDDs
  • The semantical representation:
    1. Consider a formal boolean function f.
    2. Also consider a linear order L of the variables of f.
    3. The OBDD of f w.r.t. L should exactly correspond to the set of formal boolean functions
      1. which are obtained from f by application of partial assignments whose domains are initial segments of L,
      2. and which depend on all their variables.
  • We need to compute the semantical representation according to this description. It seems best to first get in the way the nodes of the ordinary OBDD, while we leave out the edges and their labels (which can be added later).
Todo:
Smurfs
  • http://www.cs.uc.edu/~weaversa/SBSAT.html is the homepage of SBSAT, which is based on "smurfs", a strong representation of boolean functions.
  • The user manual is http://gauss.ececs.uc.edu/sbsat_user_manual/ .
  • The semantical representation:
    1. Consider a formal boolean function f.
    2. The smurf of f should exactly correspond to the set of formal boolean functions
      1. which are obtained from f by application of (artitrary) partial assignments,
      2. and which depend on all their variables and have no forced assignments.
  • We need to compute the semantical representation according to this description. It seems best to first get in the way the nodes of the smurf, while we leave out the edges and their labels (which can be added later).
  • Another similar model is "Finite functions with full application of partial assignments" in Satisfiability/Lisp/FiniteFunctions/plans/general.hpp.

Definition in file BDDs.hpp.