Plans regarding finding sizebounded hypergraph transversals.
More...
Go to the source code of this file.
Detailed Description
Plans regarding finding sizebounded hypergraph transversals.
 Todo:
 Connections
 Todo:
 Translations to SAT

We need translations of the problem of finding a hypergraph transversal of size "=B" or "<=B" to CNFSATinstances 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 CNFSAT, to obtain a pure CNFSAT problem.

Alternatively, one could translate it fully into a cardinalityconstraint problem instance, while then for a CNFtranslation of (pure) cardinalityconstraint 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.
 Todo:
 Using ILP
 Todo:
 Exploiting known bounds

See "Exploiting selfsimilarity" 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:

For the branch where v is included: If v in S, then s:s+1 and r:r1.

For the branch where v is excluded: If v in S, then r:r1 (this follows from the removal of v from S).

In both cases, if v is not in S then nothing happens.

The numbers a, b stay as they are.

While S doesn't need to be updated (removal of v had no further (real) effect).

In the vdWapplication 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?

The only places where S, T are needed is when all of ST needs to be included resp. excluded.

Perhaps one just keeps ST uptodate?

How are the sets S given?

In the vdWapplication it is quickly computable to which S the current vertex v belongs.

So perhaps we actually model a kind of active clauseset here.

Only inclusions resp. exclusions need to be taken care of (no undoing here).

So a function S is supplied, which takes as input pairs [v,e], where e=0 for exclusion and e=1 for inclusion (DNFinterpretation).

While the output is the list of inferred clauses (CNFinterpretation), the empty clause for a contradiction, and unit clauses for forced inclusions/exclusions.

So inside S unitclause propagation must take place.

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 nonboolean CNFclausesets (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 CNFinterpretation negative literals are more natural, perhaps here we just use positive literals? Then there would be no need for reinterpretations.

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.