Examples.hpp File Reference

Applying preprocessing to specific instance classes. More...

Go to the source code of this file.

Detailed Description

Applying preprocessing to specific instance classes.

Preprocessing by local dualisation should be applied to examples of small and/or well known problems, to test the idea, and to gain insights.

Pigeonhole formulas:
  • As an example, if one takes the weak PHP principle with m pigeons and n holes, one can represent pigeon i occupying a single hole by n DNF-clauses, each encoding that pigeon i sits in a particular hole as its sole occupier.
  • The weak PHP problem can then be represented by considering the conjunction of these DNF's, which can be represented as a CNF by translating each of these DNF's into CNF via the canonical translation.
  • This can be done using the following code:
    weak_php_ts_fcl(m,n) := 
        dualtsext_fcl(cl2fcl(pigeon_in_hole_dnf_cl(i,m,n)), i)[2],
        i, 1, m)))$
    pigeon_in_hole_dnf_cl(i,m,n) :=
      create_list(setify(create_list(if i2 = i then php_var(i2,j) else -php_var(i2,j), i2, 1, m)), j, 1, n)$
    output_weak_php_ts(m,n,filename) := block([FF : standardise_fcl(weak_php_ts_fcl(m,n))],
        sconcat("Weak PHP with ", m, " pigeons and ", n, " holes in dual Tseitin representation."), 
        FF[1], filename, FF[2]))$
    output_weak_php_ts_stdname(m,n) := output_weak_php_ts(m,n,
  • MG should present experimental data on this; for this (of course!) the above code has to become "official" (with tests and documentation).
  • Understanding this example:
    1. Now we want to understand what this "preprocessing" of weak_php_fcs(m,n) means.
    2. The clause-set is covered by m clause-set F_i, each given by the "long" clause C_i expressing that pigeon i sits in one hole, plus all clauses which can be resolved with C_i.
    3. F_i expresses exactly that pigeon i sits in at least one hole, and no hole occupied by pigeon i is also occupied by another pigeon.
    4. The unique DNF of F_i is given by pigeon_in_hole_dnf_cl(i,m,n).
    5. So weak_php_ts_fcl(m,n) is an example of what could be obtained from weak_php_fcs(m,n) by preprocessing by local dualisation.
    6. Now consider the prime clause-set P_i of F_i (all prime implicates, since F_i is a CNF here).
    7. P_i is exponentially large, however it contains no interesting elements, since all elements of P_i can be obtained from F_i by input resolution.
    8. So F_i has already the property, that every inconsistency and also every forced assignment can be detected by unit-resolution, while only total satisfying assignments exist.
    9. This can easily be seen by flipping the sign of all variables phi(i,j) (for all j), where now F_i becomes a Horn clause-set.
    10. Thus very likely F_i is the best representation possible here, and preprocessing can only make things worse.
    11. MG should implement the underlying functions, validate all statements experimentally, and then should prove all of this.
    12. A necessary condition for making the general preprocessing-by-local-compilation approach work seems to be that for the F_i constituting the cover there must exist some prime clauses which are hard to derive at least by tree resolution.

Definition in file Examples.hpp.