general.hpp File Reference

Plans for Maxima-generators for clause-sets. More...

Go to the source code of this file.

Detailed Description

Plans for Maxima-generators for clause-sets.

Add tests for parity generators
Update milestones
  • Some general development strategies are to be developed.
  • Perhaps we should have a sub-module "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 re-thought and completely updated.
  • DONE ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/plans/HindmanProblems.hpp is not integrated at all.
Accompanying statistics
Write basic docus
  • We need basic docus for all generators.
  • 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 clause-set FF, how to create *new* variables?
    1. The need arises in constructions.
    2. Perhaps for each construction a new type of variable is introduced, like "php" for the pigeonhole formulas.
    3. Transformers which use a given clause-set 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.
    4. 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?
  • Motivated by a talk at BCTCS 2010 (Markus Jalsenius).
  • Their Internet resource is http://floodit.cs.bris.ac.uk .
  • Rules:
    1. The parameters are n (the dimension of the board) and c (the number of colours).
    2. Additionally we use k for the maximal number of moves.
    3. 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).
    4. Furthermore we have a map f_0: V -> {1, ..., c}.
    5. The moves will construct further maps f_1, ..., f_k: V -> {1,...,c}.
    6. 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.
    7. 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(r-1) being changed to i, that is, a transition f_{r-1} -> f_r is performed.
    8. 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 non-boolean SAT, encoding the round when a vertex has been reached:
    1. Using variable m_1, ..., m_k, each of domain {1,...,c}, for the moves.
    2. 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)).
    3. 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 r-1 and the initial colouring f_0(v) is equal to the value of m_r.
    4. (1,1) and neighbours of (1,1) are best handled separately.
    5. And likely one should explicitely state that once a node has been reached, it stays reached; this needs new variables (see the b-variables below).
    6. The domain of the condition C(v,r) is {m_r,a_v} plus a_w for the neighbours w of v.
    7. 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 r-1.
    8. This is not yet complete, since "reached stays reached" is not expressed. One could handle that by relaxing the condition "has value r-1" to "has value at most r-1". But this seems inefficient, since we should keep the domain of C(v,r) small.
    9. 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.
SMUSAT(1) and tree hitting clause-sets
Hard clause-sets (for resolution and refinements)
  • Tseitin's formulas
  • IMP and IMP' [Buresh-Oppenheim, Pitassi; 2007]
  • GT and GT' [Buresh-Oppenheim, Pitassi; 2007]
    1. We have ordergt_ofcs for the GT-formulas as used in [Kullmann, ECCC, 1999].
    2. We need to compare it with the "order principle" as used by Jan Johannsen.
    3. And we need to look into [Buresh-Oppenheim, Pitassi; 2007].
  • SP and SP' [Buresh-Oppenheim, Pitassi; 2007]
Operations (new clause-sets from old ones)
Hiding small unsatisfiable clause-sets
DONE Split Generators/Generators.mac
  • DONE Pigeonhole formulas and everything related to "Pigeonhole.mac"
    1. The spelling "pigeonhole" is to be used.
    2. Of course, all related plans go to "Pigeonhole.hpp".
  • DONE Ramsey problems
  • Special minimally unsatisfiable clause-sets
    1. 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.
    1. Perhaps to modules related to the problems they solve (by reduction).
    2. Or as kind of transformer-generators to the module where the transformed problem is solved.
    3. In any case, links should be provided.
  • Sudoku-problems : DONE

Definition in file general.hpp.