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 2hard 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 unitclauses in phi * F, hence F is 2hard.

Note the translation of p being 2hard 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 (n2)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(n2)}; 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(n2) = 2n 4 equalitys y_1 <> x_3, y_2 <> x_3, ..., y_{2n5} <> x_n, y_{2n4} <> x_n in the CNF representation.

It appears that r_{n2} is needed to "break" all of these equalities (one level each).

Are there 1soft 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 experimentdirectories

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 Bashusage 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 randomgenerator then needs to be reconsidered.
 Todo:
 Write "analyse_all_permutations"
 Todo:
 Add milestones
Definition in file general.hpp.