Plans for Maximagenerators for clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans for Maximagenerators for clausesets.
 Todo:
 Add tests for parity generators
 Todo:
 Update milestones

Some general development strategies are to be developed.

Perhaps we should have a submodule "LatinSquares" (including Sudoku).

What happened to ComputerAlgebra/Satisfiability/Lisp/Generators/plans/LinearInequality.hpp (mentioned in milestone 0.1.4) ?

DONE Generators/plans/RamseyProblems.hpp needs to be rethought and completely updated.

DONE ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/plans/HindmanProblems.hpp is not integrated at all.
 Todo:
 Accompanying statistics
 Todo:
 Write basic docus

We need basic docus for all generators.
 Todo:
 Variables

Compare "Global variables" in ComputerAlgebra/plans/Maxima.hpp.

Is the new scheme (using in functions "php_var(i,j)" instead of "php(i,j)", where php_var(i,j) := nounify(php)(i,j), now right? Why didn't the old scheme work?? (It kept a memory for the created symbols about their place of creation!!) Why is nounify(php) needed, where php is already a "noun" ??

Given a formal clauseset FF, how to create *new* variables?

The need arises in constructions.

Perhaps for each construction a new type of variable is introduced, like "php" for the pigeonhole formulas.

Transformers which use a given clauseset F should at least check that F doesn't contain the dedicated "new" variables  otherwise perhaps the computation is just aborted with an error message.

This test can be performed with e.g.
freeof(php,F)
.

DONE It seems that "declare(php, noun)" cannot be used twice, and thus we cannot reload a file containing such a declaration?? Is just to kill "php" before the solution?
 Todo:
 Floodit

Motivated by a talk at BCTCS 2010 (Markus Jalsenius).

Their Internet resource is http://floodit.cs.bris.ac.uk .

Rules:

The parameters are n (the dimension of the board) and c (the number of colours).

Additionally we use k for the maximal number of moves.

We have the graph G_{n,n}, the nxn grid, with vertex set {1,...,n}^2, and with the horizontal and vertical links (so the degree of a corner vertex is 2, of a border vertex is 3, and of an inner vertex is 4).

Furthermore we have a map f_0: V > {1, ..., c}.

The moves will construct further maps f_1, ..., f_k: V > {1,...,c}.

For round 0 <= r <= k let C(r) be the connected component of (1,1), where all vertices w with f_r(w) # f_r((1,1)) have been removed.

A move in round r in {1,...,k} now consists in choosing a colour i in {1,...,c}, which results in the colour of all vertices in C(r1) being changed to i, that is, a transition f_{r1} > f_r is performed.

The aim is to have all vertices having the same colour, that is, f_k is a constant function, which is equivalent to C(k) = V.

Translation to nonboolean SAT, encoding the round when a vertex has been reached:

Using variable m_1, ..., m_k, each of domain {1,...,c}, for the moves.

And variables a_v for v in V, each of domain {0,...,k}, for the round at which a_v has been "reached" (that is, the minimal r such that v in C(r)).

The whole problem is given by the set of conditions C(v,r) for vertices v in V and rounds r in {1,...,k}, where C(v,r) is true iff at least one neighbour of v has been reached at round r1 and the initial colouring f_0(v) is equal to the value of m_r.

(1,1) and neighbours of (1,1) are best handled separately.

And likely one should explicitely state that once a node has been reached, it stays reached; this needs new variables (see the bvariables below).

The domain of the condition C(v,r) is {m_r,a_v} plus a_w for the neighbours w of v.

C(v,r) is a conjunction of c implications, each having as premiss that m_r = i for i in {1,...,c}, and having as conclusion that a_v has value r iff at least one of its neighbours of colour i (initially) has value r1.

This is not yet complete, since "reached stays reached" is not expressed. One could handle that by relaxing the condition "has value
r1" to "has value at most r1". But this seems inefficient, since we should keep the domain of C(v,r) small.

One could introduce new boolean variables b_{v,r} with the meaning that v has been reached in one of the rounds 1, ..., r, that is, v is equivalent to the conjunction of a_v=i for i in {1,...,r}.

MG had the idea to express the problem via an iterated condition system.
 Todo:
 SMUSAT(1) and tree hitting clausesets
 Todo:
 Hard clausesets (for resolution and refinements)

Tseitin's formulas

IMP and IMP' [BureshOppenheim, Pitassi; 2007]

GT and GT' [BureshOppenheim, Pitassi; 2007]

We have ordergt_ofcs for the GTformulas as used in [Kullmann, ECCC, 1999].

We need to compare it with the "order principle" as used by Jan Johannsen.

And we need to look into [BureshOppenheim, Pitassi; 2007].

SP and SP' [BureshOppenheim, Pitassi; 2007]
 Todo:
 Operations (new clausesets from old ones)
 Todo:
 Hiding small unsatisfiable clausesets
 Todo:
 DONE Split Generators/Generators.mac

DONE Pigeonhole formulas and everything related to "Pigeonhole.mac"

The spelling "pigeonhole" is to be used.

Of course, all related plans go to "Pigeonhole.hpp".

DONE Ramsey problems

Special minimally unsatisfiable clausesets

The documentation should mention random_splitting_mus in ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/SplittingAnalysis.mac
DONE (moved to Satisfiability/Lisp/MinimalUnsatisfiability)

The translations are not generators, and should go somewhere else.

Perhaps to modules related to the problems they solve (by reduction).

Or as kind of transformergenerators to the module where the transformed problem is solved.

In any case, links should be provided.

Sudokuproblems : DONE
Definition in file general.hpp.