Plans regarding straightline programs ("circuits")
More...
Go to the source code of this file.
Detailed Description
Plans regarding straightline programs ("circuits")
 Todo:
 The notion of a "straightline 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 ith function in L with output number j, or are numbers i for the ith input.

These "general circuits" are normally called "straightline
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 sourcegates.
 Todo:
 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 straightline 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.
 Todo:
 Other translations (than the Tseitin translation)

See [Manolios, Vroon; SAT 2007].

As types of circuits "Reduced Boolean Circuits" (RBCs), "AndInverter Graphs" (AIGs) and "NICE dags" are mentioned.

The basis for a nicedag is given by negation, ite (ifthenelse), conjunction (nary?) and equivalence (nary?). And then there are several restrictions similar to RBCs, to maximise "sharing".

A quadratictime algorithm to translate such nicedags into CNF is presented, and implemented in their system "BAT" (see "BAT" in Buildsystem/ExternalSources/SpecialBuilds/plans/ModelChecking.hpp).

The "JacksonSheridan" algorithm is mentioned, translating an RBC into CNF.

And they also mention the "BrummayerBiere" algorithm, from AIGs to CNF.

See [Een, Mishchenko, Soerensson; SAT 2007]

AIGs are considered: gates are binary conjunction, negation and the constant true, where negation is handled by "signing" edges.

First rewriterules on AIGs are systematically investigated.

And then the CNFtranslation happens via "technology mapping", some form of optimisation process.
Definition in file StraightLinePrograms.hpp.