OKlibrary  0.2.1.6
Basics.hpp File Reference

Plans regarding the basics of boolean functions. More...

Go to the source code of this file.

Detailed Description

Plans regarding the basics of boolean functions.

Todo:
Notions of "finite functions"
• For a "finite function" f implicitly a domain D of values is given, with D = {0,1} for "boolean function", and furthermore we have an implicitly associated size-domain S <= NN_0, such that for every n in S f accepts lists of length n over D as inputs, and returns lists of length m_n (for some fixed m_n) over D as results.
• DONE (a finite function is just a function f, while n and m are not specified, but actually can be variable) A triple [n,m,f], where n is the number of inputs, m the number of outputs, and f the function, which accepts lists of length n, and returns lists of length m.
• Let's speak of a "n x m" finite function if we have n inputs and m outputs.
• DONE (0,1 is most common) The default is boolean values; shall this be "false, true", or "0, 1", or perhaps "-1, +1" ?
• DONE (n,m,D are only given implicitly) If a quadruple [n,m,f,D] is used, then for input and output the set of values is D.
• And if a quintuple [n,m,f,D,C] is used, then the values for the inputs are taken from D, while the values for the output are taken from C.
• Abbreviations: "bf" for "boolean function", "ff" for "finite function" (in general).
• Input and output conventions:
1. To make it more useful, perhaps instead of using standardised input and output names through natural numbers, we should use variables?!
2. Or should the renaming be done separately?
3. As above, inputs and outputs are lists of values; using variables, inputs and outputs would be total assignments w.r.t. the variables used.
4. Perhaps the basic functions are standardised boolean functions, operating on lists, while the various realisations of these functions use variables appropriately.
• An especially important case, realised for example by signed clause-sets, is that of a "finite relation", a map f: D^n -> {0,1}.
• Definitely we have the need for "formal boolean functions", which are associated with variables; see "Basic operations for boolean functions" in Satisfiability/Lisp/FiniteFunctions/plans/BDDs.hpp.
Todo:
Representing boolean functions by their truth tables
• The truth table is just a sequence of bits. So once the order is standardised (in such a way that adding variables doesn't change the order), truth tables can be represented by natural numbers (including zero), plus the information how many variables are there.
• Most natural seems here to use binary counting, with leading digit last (compare ComputerAlgebra/Combinatorics/Lisp/Enumeration/plans/general.hpp).
• Given such an encoding, the composition of boolean functions can be achieved by bitwise operations:
1. By package functs we have logor, logand and logxor; we have implemented these functions ourselves as and_ibo, or_ibo, xor_ibo.
2. We should also provide the other 13 basic functions (see ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/plans/BasicFunctions.hpp).
3. For negation one needs to know the number of bits.
• See "Using different algorithms for different parameter values" in Satisfiability/Heuristics/plans/general.hpp for some application of such algorithms (in general SAT solving).
Todo:
Algebraic normal form
• The algebraic normal form of an n x 1 boolean function f is as a sum of monomials in variables x_1, ..., x_n over the field (boolean ring) ZZ_2.
• One can also say that these are exactly the representations by polynomials in variables x_1, ..., x_n, since multiplication is idempotent, and thus only mononials need to be considered (using only powers 0 and 1).
• Every boolean function has exactly one such algebraic normal form, for which we should use the abbreviation "anf".
• How to represent anf's:
1. One could use Maxima terms together with ordinary addition and multiplication.
2. For evaluation values 0, 1 are substituted into the variables, and the sum is evaluated modulo 2.
3. However then we have the problem that for example natural numbers are not variables anymore, and renaming needs to happen.
4. So this shouldn't be the main form, but for the main form we just use hypergraphs, where the hyperedges represent the monomials.
5. Calling this "anf", while the sum of monomials in the Maxima-sense is called "manf".
6. A function "anf2manf" performs the translation, where we need various forms, like anf2manf_hg, if the input is a hypergraph, anf2manf_ohg, if the input is an ordered hypergraph.
7. For variables in the manf-form we use terms anf(v), where v is the original vertex.
8. eval_manf(t, S) evaluates such a term, where S is the list of substitutions in appropriate form.
• Direct computation of manf for n x 1 bf f:
1. The direct formula is as the sum over the vector v in f^-1(1) of products (x_1 + v_1 + 1) * ... * (x_n + v_n + 1), using variables x_i and arithmetic in ZZ_2.
2. This is true since each such product is exactly 1 iff x = v.
3. How can we evaluate these products more efficiently, taking idempotence of multiplication into account?
4. This argument shows existence of anf's, and uniqueness follows since there are only 2^(2^n) different anf's, and each thus must represent a different boolean function (of which there are exactly 2^(2^n)).
• Alternative computation:
1. The proof of uniqueness of anf for f: One has to show that an anf is zero iff its the empty hypergraph. Assume we have hyperedges. Choose a minimal hyperedge E (w.r.t. set-inclusion). Setting the variables in E to 1 and the other variables to 0, this hyperedge evaluates to 1, while the other hyperedges evaluate to 0. Thus E is a hyperedge in the anf of f.
2. So we get the following algorithm: For f compute its DNF hypergraph representation (for example by fulldnf2dnfhg_ofcs2ohg(FF)), collect the minimal hyperedge into the result-anf, subtract these hyperedges from f, in the algebraic interpretation over ZZ_2, and repeat with the new f.
3. The algorithmic problem is the subtraction: How to do this efficiently, without having to use the whole f ?
• Perhaps these functions go into a new file, AlgebraicNormalForm.mac. There will be further functions, like extracting the degree (the maximal size of a hyperedge).
• The standard translation of a formula p in ANF into CNF has:
• the variables of p;
• a new variable y_i for each product X_i in p;
• the primes clauses for y_i <-> X_i for each product X_i in p;
• clauses representing the sum (XOR) of all y_i (this could be prime clauses, or a splitting of the sum using new variables).
We should implement this translation, and provide references.
• Investigating algebraic normal forms and their translations is discussed in "Algebraic normal form" in Experimentation/Investigations/BooleanFunctions/plans/general.hpp.
Todo:
DONE (we just use full clause-sets) Boolean functions represented by sets of satisfied/falsified inputs
• An n-ary boolean function can be represented by a set of lists of length n, with elements 0,1.
• This as "dnf-representation" is the set of inputs mapped to 1, and as "cnf-representation" mapped to 0.
• How to call such representations? There is the notion of "minterms" and "maxterms", but I (OK) find this confusing. Let's just call it the "positive full representation" and the "negative full representation" ("full" as with "full clauses").
• Abbreviations "pfrbf" and "nfrbf".
• So for example the pfrbf of the binary and is {[1,1]}, while the nfrbf is {[0,0],[0,1],[1,0]}.
• Shall we make a distinction between sets and lists?
• These sets are just re-coding of the full DNF and the full CNF representations; so do we need this type of representation at all?
• Perhaps it is convenient (and intuitive) to have it.
• However as DNF-clause-sets the above is {{1,2}}, while as CNF-clause-set we have {{-1,-2},{-1,2},{1,-2}} (using the positions as variables).
• So we better avoid this doubling of entities.

Definition in file Basics.hpp.