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:
Add milestones

Definition in file general.hpp.