general.hpp File Reference

Plans regarding boolean functions and generalisations. More...

Go to the source code of this file.

Detailed Description

Plans regarding boolean functions and generalisations.

Create milestones
Connections to other modules
General plans
  • An important motivation is the task of, given a finite function, find a representation of it by generalised CNF/DNF, propositional logic, CSPs, alliances of active clause-sets etc.
  • So from this point of view, finite functions are building blocks in representations of (generalised) satisfiability problem instances, and the task is to transform the whole representation into an alliance of active clause-sets.
  • But finite functions are also interesting in their own right. Constructing smallest circuits or smallest branching programs for example are interesting tasks (involving themselves satisfiability problems).
  • So various forms of general computational representations need to be supported, together with conversions to other forms.
  • Such "conversions" might involve satisfiability problems in various forms.
  • However, automata are not considered here, since we are studying here "combinatorial" (non-uniform) computations.
  • Perhaps we have a module ComputerAlgebra/Automata, where various forms of automata are provided, and there then, for a given input size, various forms of representations of this finite function (e.g., as a circuit), are also provided. See "Module ComputerAlgebra/Automata" in ComputerAlgebra/plans/general.hpp.
Quadratic functions
  • A boolean function is called "quadratic" if it is equivalent to a 2-DNF, and "dualy quadratic" if equivalent to a 2-CNF.
  • We need to implement the recognition of quadratic and dual quadratic functions.
  • We should have a dedicated file "Quadratic.mac".

    Horn functions
    • A boolean function is called "Horn" if it is equivalent to a Horn CNF.
    • We need to implement the recognition of Horn functions.
    • We should have a dedicated file "Horn.mac".
    Finite functions with full application of partial assignments
    • Compare to "Smurfs" in Satisfiability/Lisp/FiniteFunctions/plans/BDDs.hpp.
    • Consider a set D of values.
    • A "finite function with full application", for short "fffa", is either an element of D (for a constant function, without variables), or some object f, where the operations are
      1. var_fffa(f) for the set of variables of f on which f really depends,
      2. apply_pa_fffa(phi,f) for the application of a partial assignment phi to f, yielding again a fffa.
    • f is a constant iff var(f) = {} iff f is semantically a constant.
    • Variables v in phi with v notin var(f) have no influence on phi * f.
    • We have (psi * phi) * f = psi * (phi * f), where psi * phi is the composition of partial assignments.
    • For hitting CNF and hitting DNF we can implement models.
    • Even more efficient for permutations of {0,1}^n as boolean conditions {0,1}^2n -> {0,1}.
    And-inverter graphs (AIGs)
    • AIG's represent boolean functions; they are directed graphs with two types of nodes, terminal vertices, with outdegree zero and labelled by variables, and and-nodes, with out-degree one and arbitrary in-degree.
    • Additionally edges can be labelled as "negations".
    • So these are just general circuits, only using negation and binary conjunction.
    • The computation starts at the terminal nodes, and moves backwards.
    • How to represent such digraphs?
      1. One possibility is the straight-line format, that is, we do not use explicit digraphs, but just "node-lists".
      2. Or we use general digraphs, where the vertices are either variables or otherwise and-nodes, and where edges are either "positive" or "negative".
    • See http://en.wikipedia.org/wiki/And-inverter_graph for general information.
    • Regarding external sources, see (at least) "Aiger" and "ABC" in Buildsystem/ExternalSources/SpecialBuilds/plans/BooleanFunctions.hpp.
    File formats
    • Lexicographical listing of all values:
      1. The file format should be very close to the Dimacs-format, but there is no need for line-end-symbols.
      2. So we have an initial comment block (every line started with "c").
      3. Then the parameter line, for boolean functions "p bft n" ("boolean function table"), while for general finite functions with n inputs, 1 output, and value set D = {1, ..., p} we use "p fft n p".
      4. After this parameter-line we have (exactly) 2^n resp. p^n many entries separated by (at least one) space-symbol, each representing a value for inputs in lexicographical order (from left to right, using the natural order on integers).
      5. For boolean functions the values are 0,1, while the default for finite functions is 1, ..., p.
      6. Perhaps by "fftz" instead of "fft" we use zero-based values, i.e., D = {0, ..., p-1}. So fftz for p=2 is exactly the case bft.
    • For information on how to use Espresso and the file format involved see Buildsystem/ExternalSources/SpecialBuilds/docus/Espresso.hpp .

Definition in file general.hpp.