general.hpp File Reference

On investigations regarding the hardness of representations of boolean functions. More...

Go to the source code of this file.

Detailed Description

On investigations regarding the hardness of representations of boolean functions.

Hardness of boolean function representations
  • The hardness h(F) of a CNF F is defined to be the minimum k such that for all implicates C of F, we have that r_k(phi_C * F) yields the empty clause.
  • We have that:
    • h(F) = 0 if F contains all its prime implicates.
    • h(F) <= h(F') where F' is the canonical (full) CNF representation of F.
    • If F is a full clause-set, i.e., only clauses of length n(F)), then h(F) = n(F) - m where m is the size of a prime implicate of F with the minimum clause-length.
    • If F is renamable horn, then h(F) <= 1.
    • If F is a 2-CNF clause-set, then h(F) <= 2.
  • For a boolean function f the "hardest" representation F, without new variables, is the canonical CNF representation of f. This follows from the fact that for every partial assignment phi, applying phi to F yields the canonical unsatisfiable CNF on the remaining variables, which is of maximum hardness.
  • How does this hardness notion relate to the performance of SAT solvers on existing problems?
  • Investigations into how representations with different hardness affect SAT solving is being investigated in:
  • The hardness of the following should be investigated:
  • Computing the hardness of small functions:
    • We do not, in general, compute the hardness of boolean function representations, but construct representations with low hardness.
    • However, for experimental evaluation and curiousities sake, we can and should measure the hardness of certain representations of small boolean functions.
    • For example, we should measure the hardness of the minimum representations of the DES and AES boxes. See AdvancedEncryptionStandard/plans/Representations/general.hpp.
    • We have the Maxima-functions hardness_wpi_cs, hardness_cs, and hardness_u_cs for computing hardness.
Propagation hardness of 2-CNF
  • F in 2-CLS should even have phardness(F) <= 2.
  • This should be investigated also experimentally (to strengthen our system).
Hardness of canonical translation of positive DNF
  • For a positive DNF-clause-set F, the set of CNF-prime-clauses is the transversal hypergraph of F, with element-wise negation.
  • One would guess that if F is far away from a variable-disjoint hitting clause-set, then the canonical translation dualts_cs(F) should have high hardness.
  • The boolean function of the DNF F could then also have the property of not having a small CNF-representation of small hardness.
  • If F is a positive 2-CLS, then we have hardness at most 1:
    test1(n) := hardness_cs(dualts_cs(powerset(setn(n),2)))$
    n <= 1 yield hardness 0, all other n yield hardness 1.
  • 3-CLS:
Hardness of Sudoku problems
  • As discussed in "Finding hard instances for box-dimension 3" in Investigations/LatinSquares/Sudoku/plans/general.hpp, the right approach for determining the "hardness" of Sudoku problems should be to determine their t-, p- and w-hardness!
  • Also the direct encoding is very natural here.
  • An article about this should be very attractive!
  • For this we need hardness-computation at C++ level.

Definition in file general.hpp.