general.hpp File Reference

Plans regarding finding size-bounded hypergraph transversals. More...

Go to the source code of this file.

Detailed Description

Plans regarding finding size-bounded hypergraph transversals.

Translations to SAT
  • We need translations of the problem of finding a hypergraph transversal of size "=B" or "<=B" to CNF-SAT-instances plus cardinality constraints.
  • See "Representing cardinality constraints" in ComputerAlgebra/Satisfiability/Lisp/Generators/plans/CardinalityConstraints.hpp.
  • Then to this "mixed problem" one can apply a translation of cardinality constraints to CNF-SAT, to obtain a pure CNF-SAT problem.
  • Alternatively, one could translate it fully into a cardinality-constraint problem instance, while then for a CNF-translation of (pure) cardinality-constraint problems constraints ">= 1" (which just represent clauses) are handled directly?
  • But this is a loss of information! And we need to have mixed problem types anyway, so we should use the mixed presentation.
Using ILP
Exploiting known bounds
  • See "Exploiting self-similarity" in Experimentation/Investigations/RamseyTheory/VanderWaerdenProblems/Transversals/plans/general.hpp for motivation.
  • The aim is to improve transversals_bv, transversals_bvs by exploiting known bounds on localised transversal sizes.
  • Given are a hypergraph G and sets S <= V(G) together with numbers a, b fulfilling a <= |S cap T| <= b for every transversal fulfilling the given bound |T| <= B.
  • Then dynamically (changing with T) the intersection size s = |S cap T| and the number r = |S - T| of remaining vertices are updated.
  • As soon as s > b or s + r < a holds the current T is "inconsistent".
  • The algorithm invariants should avoid reaching this situation, and instead we should have forced assignments "one step before".
  • That is, if s = b is reached, then all vertices in S - T need to be removed.
  • While if s+r = a is reached, then all vertices in S - T need to be included.
  • When branching on vertex v the following updates are performed:
    1. For the branch where v is included: If v in S, then s:s+1 and r:r-1.
    2. For the branch where v is excluded: If v in S, then r:r-1 (this follows from the removal of v from S).
    3. In both cases, if v is not in S then nothing happens.
    4. The numbers a, b stay as they are.
    5. While S doesn't need to be updated (removal of v had no further (real) effect).
  • In the vdW-application S is a progression with s < n, which yields the lower bound, while also the complement of S is a progression, which yields a lower bound on the size of the complement, and thus an upper bound on the size of S.
  • A question is whether one needs to have T explicitely represented?
    1. The only places where S, T are needed is when all of S-T needs to be included resp. excluded.
    2. Perhaps one just keeps S-T up-to-date?
  • How are the sets S given?
    1. In the vdW-application it is quickly computable to which S the current vertex v belongs.
    2. So perhaps we actually model a kind of active clause-set here.
    3. Only inclusions resp. exclusions need to be taken care of (no undoing here).
    4. So a function S is supplied, which takes as input pairs [v,e], where e=0 for exclusion and e=1 for inclusion (DNF-interpretation).
    5. While the output is the list of inferred clauses (CNF-interpretation), the empty clause for a contradiction, and unit clauses for forced inclusions/exclusions.
    6. So inside S unit-clause propagation must take place.
    7. The concept of "literal" must be clarified here.
      • Boolean variables are natural, with 0 for exclusion and 1 for inclusion.
      • Since we want to continue working with the vertices as given, we work with monosigned literals, where variables have boolean domains.
      • A hyperedge, say {a,b,c}, stands for {a#0,b#0,c#0}, so we have non-boolean CNF-clause-sets (using negative monosigned literals) --- but the concept of literals here also allows, e.g., "a=0".
      • So literals are actually triples [v,e,s] (see "Notions for generalised literals" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/plans/NonBoolean.hpp), where e in {0,1} and s in {-1,+1}.
      • But perhaps it is more natural for the communication with the active clause S to consider the literals communicated as (just) positive (so no need for the sign here)? However for the output this is not natural, and they should be negative (monosigned), if one does not want to use signs.
      • Though for CNF-interpretation negative literals are more natural, perhaps here we just use positive literals? Then there would be no need for re-interpretations.
      • Hyperedge {a,b,c} would be interpreted as {a=1,b=1,c=1}, i.e., {[a,1],[b,1],[c,1]}, while the input to S is a (single) literal [v,e] as above, and the output is a list of clauses (of length at most 1), where, say, {[d,0]} would mean that d is to be exluded.
      • Seems natural.

Definition in file general.hpp.