Plans regarding applications of (generalised) SAT to combinatorial optimisation.
More...
Go to the source code of this file.
Detailed Description
Plans regarding applications of (generalised) SAT to combinatorial optimisation.
 Todo:
 Update namespace
 Todo:
 Write milestones
 Todo:
 Travelling salesman problem

This seems to me the most widely explored topic of combinatorial optimisation, and thus we should connect to it.

It seems also that since 2000 or so there is stagnation in the field, at least w.r.t. algorithms and implementations, and perhaps something can be done here.

Under Combinatorics/Graphs we should consider generic algorithms (and/or links to respective software).

One would guess that SAT should be most likely to succeed on nongeometric and exact TSP's.

One could run first a "normal" TSP algorithm to obtain a good approximation, and then try to show that this is optimal (or not).

Interesting to consider how to embed geometric information into SAT, but likely this is not so easy.

Methods for employing SAT:

Of course, various direct translations need to be provided.

And then active clauses and active clausesets need to be explored.

Connect to the module Applications/Embeddings/HamiltonianPaths:

See HamiltonianPaths/plans/general.hpp ("TSP").

It might be that the "numerical treatment" via large weights is not optimal.

We should also explores the use of ordinal numbers in heuristics for the TSP as proposed by AB.

Interesting translations from/to SAT:

The hypothesis (OK) is that SAT handles the "combinatorial heart", while TSP is for the "geometrical surface".

So "typical SAT problems" translated into TSPproblems should be hard.

As well as a SAT solver should have problems (starting with the problem size) in handling TSPproblems. However here active clausesets could come to the rescue.

Organisation questions:

Perhaps we better speak of "Travelling Salesperson Problem", as originally introduced? Does this have to do with "British English" vs. "USamerican English" ? Or perhaps the "travelling salesperson
is political correctness, and the "salesman" is the original version?
Then, of course, we stick to the "salesman". </li>
<li> It should get its own module, "TravellingSalesperson" or
"TravellingSalesman", with namespacealias "TrS". </li>
<li> Here, in part "Applications", we only have SATapplications; however we need also a module devoted to the TSP (where direct approaches etc. are handled). Likely this should go to supermodule Combinatorics/Graphs. See "Organisation" in Graphs/plans/general.hpp.

See "Travelling salesman" in Satisfiability/Transformers/plans/general.hpp for translations into SAT.

And see "Organisation" in Graphs/plans/general.hpp for translations from SAT to TSP.

See "Travelling salesman" in Buildsystem/ExternalSources/SpecialBuilds/plans/SAT.hpp for installing external software.
Definition in file general.hpp.