general.hpp File Reference

Plans on the "Enigma1277" ("Faron's Puzzle") and generalisations. More...

Go to the source code of this file.

Detailed Description

Plans on the "Enigma1277" ("Faron's Puzzle") and generalisations.

Update namespace.
Create milestones.
Empirical study
  • Under Experimentation/ExperimentSystem we need a program which allows to run a collection of solvers of a collection on benchmarks, storing the results in some appropriate directory structure.
  • Solvers to investigate:
    1. OKsolver2002 in all variations
    2. The march solvers
    3. Ubcsat solvers (rsaps seems best)
    4. Minisat
  • Parameters to investigate:
    1. Number of solutions, number of essentially different solutions (at least for the maximal score)
    2. Tree-resolution hardness
    3. Structure of autarky monoid
Alternative formulations
  • Quantified Boolean Formulas ?
  • Obviously we can use non-boolean variables; also more powerful types of clauses?
    1. While the primary variables are naturally boolean, for the auxiliary variables we can use domain-size k (for every field an auxiliary variable).
    2. That all numbers are used is then captured by the surjectivity condition (all auxiliary variables together must capture all k numbers).
  • First-order logic ?
  • Is there an alternative propositional translation? Using different auxiliary variables?
    1. Instead of a total score k one can subdivide it into k = k_0 + k_1, that is, we have two parameters k_0, k_1, and k_e is the minimal number of components with vertices assigned value e.
    2. The primary variables stay as before, but instead of one type of auxiliary variables c_{i,j,p}, with k instances per field, we now have two types of auxiliary variables, with k_0 resp. k_1 instances per field:
      • c^e_{i,j,p} for 1 <= p <= k_e and e in {0,1}
      • b_{i,j} -> not c^0{i,j,p} for all 1 <= p <= k_0
      • not b_{i,j} -> not c^1{i,j,p} for all 1 <= p <= k_1
    3. Each instance should now be simpler (since we have to solve more of them to establish the score).
    4. It appears, that now also all basic symmetries are broken?
    Such generators shall go to module Satisfiability/Transformers/Generators.
  • Active clauses and active clause-sets?
Special algorithms
  • The brute-force search through all 2^(d^2) colourings should be implemented:
    1. Input a graph.
    2. Run through all 0-1-assignments to the vertices, eliminate all edges having different colours, and determine the number of connected components.
    3. Report for each score how often it has been achieved.
Generalisation for arbitrary graphs
  • Instead of the chessboard-graphs G_d we can allow arbitrary graphs as inputs.
  • The decision problem, now with two inputs G and k, should be NP-complete.
  • One can study the complexity of parameterised problems:
    1. For fixed k and arbitrary G? Not even clear this is in P?
  • For a graph G and a vertex set A let G[A] denote the induced subgraph, and let ncc(G) denote the number of connected components of G.
    1. So we have score(G) = max_{A <= V} ncc(G[A]) + ncc(G[V-A]).
    2. Now for m >= 2 we can define score_m(G) as the maximum of sum_{A in P} ncc(G[A]) over all partitions P of V with |P| <= m.
    3. We have score_2(G) = score(G).
    4. Instead of boolean primary variables now naturally m-valued variables can be used.

Definition in file general.hpp.