OKlibrary  0.2.1.6
general.hpp File Reference

On investigations regarding boolean functions. More...

Go to the source code of this file.

## Detailed Description

On investigations regarding boolean functions.

Todo:
Fast computation of prime implicates/implicants
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.
• Implementations of ANFs are discussed in "Algebraic normal form" in ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/plans/Basics.hpp.
• Hardness of CNF representations of ANF formulas:
• An ANF formula represents the constant 0 function iff it is 0.
• So, given a formula in ANF, we can trivially decide if some partial assignment falsifies it (just evaluate and check "= 0?").
• This brings up the obvious relation to hardness, as discussed in "Hardness of boolean function representations" above.
• In general, what is the hardness of an ANF formula translated to CNF in the standard way?
• Translating the ANF formula p := x_1 * x_2 + x_1 * x_3 as standard:
```F := prime_imp(y_1 <-> x_1 * x_2) union prime_imp(y_2 <-> x_1*x_3) union prime_imp(xor(y_1,y_2,1))
```
yields a 2-hard representation, because the assignment phi = <x_2 -> 1, x_3 -> 1> applied to F gives
```phi * F = prime_imp(y_1 <-> x_1) union prime_imp(y_2 <-> x_1) union prime_imp(xor(y_1,y_2,1))
```
representing the (unnormalised) "ANF" formula x_1 + x_1 which normalised to ANF is 0. However, there are no unit-clauses in phi * F, hence F is 2-hard.
• Note the translation of p being 2-hard does not depend on the representations for the boolean functions y_i <-> X and XOR in the standard ANF to CNF translation.
• MG conjectures that for any number of variables n in NN, there exists an ANF formula for which the standard CNF translation is (n-2)-hard:
• Consider such an n, and the formula:
```x_3 * x_1 + x_3 * x_2 + ... + x_n * x_1 + x_n * x_2
```
which has the translation with new variables y_1, ..., y_{2(n-2)}; each new variable representing a product in the ANF formula.
• The assignment <x_1 -> 1, x_2 -> 1> falsifies this formula, and leaves us with 2(n-2) = 2n -4 equalitys y_1 <-> x_3, y_2 <-> x_3, ..., y_{2n-5} <-> x_n, y_{2n-4} <-> x_n in the CNF representation.
• It appears that r_{n-2} is needed to "break" all of these equalities (one level each).
• Are there 1-soft translations of all ANF formulas into CNF?
• We should implement the functions needed to deal with ANF formulas and their conversion to CNF and then investigate this empirically.
Todo:
Boolean function representations
• We need a list of all the representations we use for boolean functions.
Bug:
analyse_random_permutations does not create experiment-directories
• Every experiment takes places in its own directory.
• This standard has been explained and used many times.
• Perhaps MG would finally take notice of it.
• Also the weak Bash-usage has to be corrected.
• And the other scripts in this directory need also to be corrected.
• Every program and so on carries a proper name, and thus scripts use capital letters.
Todo:
All essential computations of analyse_random_permutations at C++ level
• The C++ simulation of the Maxima random-generator then needs to be reconsidered.
Todo:
Write "analyse_all_permutations"
Todo: