OKlibrary  0.2.1.6
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.

Todo:
Connections
Todo:
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.
Todo:
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).
Todo:
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_cs(dualts_cs({{1,2,3},{2,3,4}});
1
```
Todo:
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.