StraightLinePrograms.hpp File Reference

Plans regarding straight-line programs ("circuits") More...

Go to the source code of this file.

Detailed Description

Plans regarding straight-line programs ("circuits")

The notion of a "straight-line program"
  • An important construction of a finite function is from a "gate list", which is a list L consisting of pairs [I,f], where f is an n x m ff, while I is a list of length n specifying the inputs of n, which are either pairs [i,j] for the i-th function in L with output number j, or are numbers i for the i-th input.
  • These "general circuits" are normally called "straight-line programs".
  • For the output we need to specify a list with pairs [i,j] or i (as before).
  • Perhaps, when the function has only one output, then a singleton list [i] can be used.
  • When using an input [i,j], then i must be smaller than the index of the gate (for which this is an input); in other words, the gates are nodes of a dag (directed acyclic graph), and we have given (via the ordering of L) a topological sorting.
  • More precisely, the gates can only be properly understood as nodes if they have only one output. For m >= 2 outputs, perhaps the node is splitting into one "computational node", into which all the inputs go, and this node has m outgoing arcs to the "output nodes", where the respective single outputs can be obtained.
  • We don't need to admit constant inputs, since these can be simulated by source-gates.
The notion of a "boolean circuit"
  • Of interest is finding boolean circuits (w.r.t. different bases) for given boolean functions.
  • Boolean circuits are likely best modelled as boolean straight-line programs, where now best the gates come from a given set (for example the set B_2 of all binary boolean functions).
  • See the work of Alexander S. Kulikov for example.
  • Section 7.1.2 in [Knuth, The Art of Computer Programming: Introduction to Combinatorial Algorithms and Boolean Functions, 2008] contains a nice overview and concrete methods for computing optimal circuits (over the full base).
  • Perhaps Heribert Vollmer is interested in such investigations?
  • Another important topic, generalising the considerations under "Simplifications" in ComputerAlgebra/Satisfiability/Lisp/PropositionalLogic/plans/general.hpp, is simplification of boolean circuits.
Other translations (than the Tseitin translation)
  • See [Manolios, Vroon; SAT 2007].
    1. As types of circuits "Reduced Boolean Circuits" (RBCs), "And-Inverter Graphs" (AIGs) and "NICE dags" are mentioned.
    2. The basis for a nice-dag is given by negation, ite (if-then-else), conjunction (n-ary?) and equivalence (n-ary?). And then there are several restrictions similar to RBCs, to maximise "sharing".
    3. A quadratic-time algorithm to translate such nice-dags into CNF is presented, and implemented in their system "BAT" (see "BAT" in Buildsystem/ExternalSources/SpecialBuilds/plans/ModelChecking.hpp).
    4. The "Jackson-Sheridan" algorithm is mentioned, translating an RBC into CNF.
    5. And they also mention the "Brummayer-Biere" algorithm, from AIGs to CNF.
  • See [Een, Mishchenko, Soerensson; SAT 2007]
    1. AIGs are considered: gates are binary conjunction, negation and the constant true, where negation is handled by "signing" edges.
    2. First rewrite-rules on AIGs are systematically investigated.
    3. And then the CNF-translation happens via "technology mapping", some form of optimisation process.

Definition in file StraightLinePrograms.hpp.