BooleanFunctions.hpp File Reference

Plans regarding building packages related to boolean functions. More...

Go to the source code of this file.

Detailed Description

Plans regarding building packages related to boolean functions.

See OKlib/Satisfiability/FiniteFunctions/plans/general.hpp for the central module regarding boolean functions (and generalisations).

Translations to SAT
Boolean functions
  • DONE (now automatically installed) There is an R-package with Quine/McCluskey etc.
    1. Installation (from CRAN)
      > oklib --R
      # Within R environment
      > install.packages("QCA")
      This draws the package from external CRAN sources. The lpSolve package dependency seems to be already installed for R in oklib.
    2. Installation (from source tarball)
      ExternalSources/Installations/R> oklib --R
      # Within R environment (with  QCA_0.5-0.tar.gz in the current directory)
      > install.packages("QCA_0.5-0.tar.gz", repos=NULL)
      Setting the "repos" parameter to null seems to force it to treat the package arguments as file paths to tar.gz packages.
  • http://www.dei.isep.ipp.pt/~ACC/bfunc/ seems not to be open source.
  • http://www.tcs.hut.fi/~tjunttil/circuits/index.html has translators and generators for boolean circuits.
Logic synthesis
  • http://vlsicad.eecs.umich.edu/BK/Slots/slots/LogicSynthesis.html
  • Scherzo
    1. Developed by Olivier Coudert (http://www.ocoudert.com/).
    2. Uses implicit BDD representation for primes and reduction techniques to avoid blow up in size of problem due to large numbers of prime implicates.
    3. Coudert has provided the code to MG, although it is not clear whether he would be willing to make it open-source.
    4. The source builds with some minor Makefile changes but segfaults. This seems likely to be an issue with how MG is building it and the difference in architectures (Scherzo seems to have been developed for systems other than standard x86 / x86_64).
    5. MG needs to e-mail Coudert again to check whether he would be willing to open-source the application.
  • BOOM
    1. Developed by Petr Fiser (http://service.felk.cvut.cz/vlsi/prj/BOOM/).
    2. Non-exact boolean minimisation, but allows iterative minimisation.
    3. According to experimental results on the project site, the software is highly competitive.
    4. License requires authors reference particular papers if one uses the software, and one must provide details to download the software (MG hasn't done this).
  • Using genetic programming:
    1. There are quite a few papes on finding (digital) circuits via genetic programming, but apparently no software.
  • Grigory Yaroslavtsev and Alexander Kulikov have written some software to find short circuits (over the full binary base for example).
  • egntott http://code.google.com/p/eqntott/
Improve documentation for Espresso
  • We should improve the source-code, so that the option "--version" is recognised.
  • At the ExternalSources page we need an index-page for the various pieces of documentation we have.
  • We need to investigate what is in espresso-book-examples.tar.gz:
    • This tarball contains a variety of different PLA files, which don't have any documentation along with them.
    • There is a book "Logic Minimization Algorithms for VLSI Synthesis" by Robert Brayton (the author of Espresso).
    • Given the name of the tarball, "Logic Minimization Algorithms for VLSI Synthesis" seems a likely candidate for the "book" the filename refers to (MG has ordered a copy).
  • The PLA format:
    • The "PLA format" is documented at ExternalSources/sources/Boolean/Espresso/espresso.5.html with additional information in ExternalSources/sources/Boolean/Espresso/man_octtools_espresso.html.
    • Finite functions with boolean variables:
      • A PLA represents a partial finite function, f : {0,1}^n -> {0,1}^m, by encoding the DNF of the relational viewpoint of f.
      • By the relational viewpoint, we mean representing the boolean function which takes both input and output bits and returns true iff f maps the given input to the given output. More precisely, representing f' : {0,1}^(n+m) -> {0,1} such that f'((I,O)) = 1 if f(I) = O.
      • The "header" of the PLA file:
        • The number of input and output variables are specified first with lines of the form:
          .i n
          .o m
          where n and m are the positive integer number of input and output variables.
        • Additional lines such as ".type" (discussed below), and others discussed in the documentation, may also be specified in the "header" of the file.
      • The "clauses":
        • Each line after the header is:
          1. a sequence of characters I in {1,0,-} of size n; followed by
          2. a space; followed by
          3. a sequence of characters O in {1,0,-} of size m.
          • Each line encodes a DNF clause which is part of a DNF representation for the partial finite function using the relational viewpoint.
          • That is, each line encodes that f(I') = O', where I' and O' are the boolean vectors corresponding to the strings I and O for that line.
          • A "-" in I indicates that f(I') = O' for both values of the corresponding variable.
          • A "-" in O indicates that f(I') = O' but the output value, for the variable the "-" corresponds to, is undefined.
      • Additional options:
        • ".type X": specifies how to interpret total assignments left unspecified, where X is one of the following:
          • "f": unspecified and assignments with undefined ouputs are assumed to be false (0).
          • "r": unspecified and assignments with undefined outputs are assumed to be true (1).
          • "fd": unspecified assignments are assumed to be false (the default for espresso).
          • "fr": unspecified assignments are considered to be "don't care" values.
          • "fdr": there should be no unspecified values.
        • The PLA standard also allows one to provide names for variables, as well as other options which give Espresso information on how to minimise the finite function provided. These options are discussed in
      • Lines in a PLA file starting with the "#" symbol are comments.
      • Note here that there is a difference between "undefined" and "unspecified".
      • One can use "-" for an output bit to explicitly *specify* that the partial finite function defined by the PLA is undefined for the corresponding input bits. A total assignment is unspecified if there is no espresso line which specifies its value.
      • Examples:
        • The DNF {{1,2,3},{-1,4,-5}} becomes
          .i 5
          .o 1
          111-- 1
          0--10 1
        • The two bit adder (from the espresso documentation):
          # 2-bit by 2-bit binary adder (with no carry input)
          .i 4
          .o 3
          0000  000
          0001  001
          0010  010
          0011  011
          0100  001
          0101  010
          0110  011
          0111  100
          1000  010
          1001  011
          1010  100
          1011  101
          1100  011
          1101  100
          1110  101
          1111  110
      • At the maxima level:
    • Finite functions with multi-valued variables:
      • The PLA format allows one to specify that certain boolean variables should be considered together as a single multi-valued variable.
      • Rather than using ".i" and ".o" to specify the number of input and output variables, one specifies:
        .mi n nb d1 ... dm
        where n is the total number of variables, nb is the number of boolean variables (always given first in the variable ordering), and di is the number of bits used to represent the i'th multi-valued variable.
      • The function is then specified as before, but the bits in multi-valued variables are separated by "|" and the last multi-valued variable is the output value (no space-separation).
      • For example (from the manual):
        .mv 8 5 2 3 4
      • We need to better understand multi-valued PLAs and relate it to our own considerations of non-boolean clause-sets etc.
    • All remaining options allowed in a PLA file should be documented here and then this later moved to docus.
  • We need to fully specify (in our system, using our language) what "PLAs" are, and create documentation for that. Perhaps we also need that at Maxima-level.
DONE (added additional entries to the configuration specific to the source directories) False build for Espresso
  • The directory names do not follow our standards.
  • In particular, espresso has the package name "espresso-ab-1.0-2.3.tar.gz" and directory names "espresso-ab-1.0", and yet it's executable name is "espresso2.3", all of which are very different.
  • This initial decision was made so as not to change the version information too much from the original (keeping with the authors original version information (1.0)) but adding more reasonable version information at the same time (the version number as printed by the executable).
  • To bring things inline with other packages, espresso should simply be repackaged to "espresso-2.3.tar.bz2" with "espresso-2.3" as the directory name and "espresso2.3" as the executable name.

Definition in file BooleanFunctions.hpp.