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 clauseset, 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 clauselength.

If F is renamable horn, then h(F) <= 1.

If F is a 2CNF clauseset, 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 Maximafunctions hardness_wpi_cs, hardness_cs, and hardness_u_cs for computing hardness.
 Todo:
 Propagation hardness of 2CNF

F in 2CLS 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 DNFclauseset F, the set of CNFprimeclauses is the transversal hypergraph of F, with elementwise negation.

One would guess that if F is far away from a variabledisjoint hitting clauseset, 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 CNFrepresentation of small hardness.

If F is a positive 2CLS, 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.

3CLS:
hardness_cs(dualts_cs({{1,2,3},{2,3,4}});
1
 Todo:
 Hardness of Sudoku problems

As discussed in "Finding hard instances for boxdimension 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 whardness!

Also the direct encoding is very natural here.

An article about this should be very attractive!

For this we need hardnesscomputation at C++ level.
Definition in file general.hpp.