Plans regarding (various) colouring problems for hypergraphs.
More...
Go to the source code of this file.
Detailed Description
Plans regarding (various) colouring problems for hypergraphs.
 Todo:
 Relations to other modules
 Todo:
 Organisation

Best to create a submodule Hypergraphs/Lisp/Colouring.
 Todo:
 Translations to SAT problems

The namecomponents "std" (as in gcol2sat_stdohg2stdnbfclud) are not very appropriate (they cover only a special case, namely that standardised hypergraphs yield standardised clausesets).

For translation to boolean SAT also the "nondiagonal" versions (using two hypergraphs) should be provided.

Strong colouring (in every hyperedge all colours are different) can be handled by first applying section_hg(G,2) and then tcol2sat_hg2fcs; should we provide a convenience function combining them?
 Todo:
 Colouring by transversals

One should work out the precise relation between kcolourings of a hypergraph and its independent kcovers.

For example are there other examples besides those with empty hyperedge set where a contraction of two maximal independent subsets forbids a colouring?
 Todo:
 Generalised colouring problems

For nondiagonal Ramseyproblems and vanderWaerdentype problems, we do not need to go directly to nonboolean clausesets, but we can use an intermediate form, with "layers of hyperedges", as discussed in the following.

The problem would be given as a triple [V,C,L], where V is a set (the vertices), C is a set (the colours), and each L is a pair [H,c], where H is a set of hyperedges on V (i.e., [V,H] is a hypergraph), while c is an element of C.

The problem is to find a map f: V > C such that for every [H,c] and every E in H there exists v in E with f(v) <> c.

A standard hypergraph colouring problem with colour set C for hypergraph [V,E] is translated in [V,C,L], where L consists of the pairs [E,c] for c in C.

Compared with nonboolean clausesets (clausesets, where the clauses contain literals [v,c]), in this way we express the information that the clauseset is organised in layers.

This is now handled by gcol2sat_ohg2nbfclud (and gcol2sat_stdohg2stdnbfclud), but in the somewhat different form of a pair [GG,C], where GG is a list of hypergraphs and C is a list of colours.
 Todo:
 Greedy colouring

Compare Combinatorics/Hypergraphs/Colourings/plans/GreedyColouring.hpp.

Greedy colouring, running through the vertices in some order, and giving the vertices the first available colour (not violating the colouring condition), can also be done for hypergraphs.

It should be that for strong colouring (all hyperedges are multicoloured) this strategy yields an optimal colouring, when using a suitable vertex ordering.

However it seems that for (ordinary, i.e., weak) colouring this is no longer the case (example?).

So perhaps we first consider only strong colourings, since this is the true generalisation of greedy colouring for graphs here.

For the implementation we need the adjacency relation between vertices, which as graph is realised by the 2section, but we need the squarehypergraph representation of this graph (providing for each vertex the set of adjacent vertices).
 Todo:
 Positional games

See "Generalising positional games to SAT" in ComputerAlgebra/Games/Lisp/plans/general.hpp for the SATgeneralisation.

The translation yields quantified satisfiability problems; see ComputerAlgebra/Satisfiability/Lisp/Quantification/plans/general.hpp.

Should this be a submodule of Hypergraphs/Colouring? Or perhaps directly of Hypergraphs? Or should be have ComputerAlgebra/CombinatorialGames?

Given a hypergraphs G, a "positional game" (generalising "tictactoe") is played by players A, B, which assign to the vertices labels A resp. B, and the winner is the first player who, after or before his move, can show a monochromatic hyperedge of his "colour".

So [{},{}] yields is a draw, while [{},{{}}] is a win for A.

The different goals:

It is to be decided whether A can force a win, or, equivalently (negated), whether B can force a draw.

Since the goal of B is to establish a proper colouring (whatever A does), it seems best to translate the problem, whether B can force a draw, into satisfiability problems.

Still easier to formulate, that B can force *at least* a draw; more precisely this is called a "strong draw", that is, over the whole length of the game A can be prevented from every creating a monochrome hyperedge.

The "strong draw" (and its negation, the "weak win") ignores who's first.

We should have all four possibilities: "A wins", "B draws", "A weakly
wins", "B strongly draws".

Let V(G) = 2m be even (one can enforce this by adding an uncovered vertex). The variables are Va = {A_1,...,A_m,B_1,...,B_m,} each with domain V(G), representing the moves of A and B, and the conditions for a strong draw are:

The bijectivitycondition, that a satisfying total assignment represents a bijection from Va to V(G).

More precisely, the whole formula is "RA > (RB and COL)" (with "R" like "Rule").

RA is the conjunction of the disequalityliterals that every Amove is different from all previous moves.

RB is the conjunction of all the disequalityliterals that every Bmove is different from all previous moves.

COL is the colouring condition (see below).

For each hyperedge H in E(G), the positively signed CNFclause of length m, with literals "B_i in H" for all i in {1,...,m}.

One could introduce auxiliary boolean variables c_v for each vertex v, which are true if vertex v is taken by B; then COL would be the conjunction of implications "B_i=v > c_v" and "A_i=v > not c_v" and for each hyperedge H the disjunction of c_v for v in H.

The quantifier prefix is [["fa",A_1],["ex",B_1], ..., ["fa",A_m,"ex",B_m]].

The natural translation of the problem using boolean variables is:

Each variable A_i resp. B_i is replaced by n = 2m boolean variables A_{i,v} resp. B_{i,v}, true iff the move i chooses v in V(G).

The ruleformulas RA, RB (see above) now also need to contain the AMO and ALO conditions.

For each hyperedge H we have now the clause of length m * H with literals B_i,v for i in {1,..,m} and v in H.

Or, using the c_v as above, we again have clauses of length H.

["fa",A_i] is replaced by ["fa",A_{i,v_1}],...,["fa",A_{i,v_n}], and ["ex",B_i] is replaced by ["ex",B_{i,v_1}],...,["ex",B_{i,v_n}].

This looks like attractive problems, where the literature on positional games yields a rich source of examples, where the outcome is known. See "Generators" in ComputerAlgebra/Satisfiability/Lisp/Quantification/plans/general.hpp.

But for the colouring module, the "generator" aspect should be subordinated under the "tool" aspect, where we actually use (generalised) SAT solving to experimentally explore open questions on positional games.

A nice testcase is tictactoe.
 Todo:
 Achievement and avoidance game

In [Partitions into sumfree sets, BHR 2006] the following other forms of 2player hypergraph games are considered:

In "Positional games" above, every plays has his colour, and proper colourings are to be constructed.

Now there are only two players, and every move consists in either only choosing a colour (from a fixed set of colours), while the vertices are run through in order, or both vertex and colour are chosen, while still proper colourings are to be constructed.

In the "achievement game", the last player who can move wins.

In the "avoidance game", the last player who can move loses.

If the hypergraph is infinite, than an order needs to be fixed.

Nonkcolourability of the whole hypergraph guarantees that the games end in a fixed number of steps.

If the hypergraph is finite, then both forms are possible, fixing a vertexorder, or allowing free choices.
Definition in file Colouring.hpp.