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.
 Todo:
 Update namespace.
 Todo:
 Create milestones.
 Todo:
 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:

OKsolver2002 in all variations

The march solvers

Ubcsat solvers (rsaps seems best)

Minisat

Parameters to investigate:

Number of solutions, number of essentially different solutions (at least for the maximal score)

Treeresolution hardness

Structure of autarky monoid
 Todo:
 Alternative formulations

Quantified Boolean Formulas ?

Obviously we can use nonboolean variables; also more powerful types of clauses?

While the primary variables are naturally boolean, for the auxiliary variables we can use domainsize k (for every field an auxiliary variable).

That all numbers are used is then captured by the surjectivity condition (all auxiliary variables together must capture all k numbers).

Firstorder logic ?

Is there an alternative propositional translation? Using different auxiliary variables?

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.

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

Each instance should now be simpler (since we have to solve more of them to establish the score).

It appears, that now also all basic symmetries are broken?
Such generators shall go to module Satisfiability/Transformers/Generators.

Active clauses and active clausesets?
 Todo:
 Special algorithms

The bruteforce search through all 2^(d^2) colourings should be implemented:

Input a graph.

Run through all 01assignments to the vertices, eliminate all edges having different colours, and determine the number of connected components.

Report for each score how often it has been achieved.
 Todo:
 Generalisation for arbitrary graphs

Instead of the chessboardgraphs G_d we can allow arbitrary graphs as inputs.

The decision problem, now with two inputs G and k, should be NPcomplete.

One can study the complexity of parameterised problems:

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.

So we have score(G) = max_{A <= V} ncc(G[A]) + ncc(G[VA]).

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.

We have score_2(G) = score(G).

Instead of boolean primary variables now naturally mvalued variables can be used.
Definition in file general.hpp.