general.hpp File Reference

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.

Update namespace
Write milestones
Travelling salesman problem
  • This seems to me the most widely explored topic of combinatorial optimisation, and thus we should connect to it.
    1. 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 non-geometric and exact TSP's.
    1. One could run first a "normal" TSP algorithm to obtain a good approximation, and then try to show that this is optimal (or not).
    2. Interesting to consider how to embed geometric information into SAT, but likely this is not so easy.
  • Methods for employing SAT:
    1. Of course, various direct translations need to be provided.
    2. And then active clauses and active clause-sets need to be explored.
  • Connect to the module Applications/Embeddings/HamiltonianPaths:
    1. See HamiltonianPaths/plans/general.hpp ("TSP").
    2. 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:
    1. The hypothesis (OK) is that SAT handles the "combinatorial heart", while TSP is for the "geometrical surface".
    2. So "typical SAT problems" translated into TSP-problems should be hard.
    3. As well as a SAT solver should have problems (starting with the problem size) in handling TSP-problems. However here active clause-sets could come to the rescue.
  • Organisation questions:
    1. Perhaps we better speak of "Travelling Salesperson Problem", as originally introduced? Does this have to do with "British English" vs. "US-american 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 namespace-alias "TrS". </li> <li> Here, in part "Applications", we only have SAT-applications; 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.
    2. See "Travelling salesman" in Satisfiability/Transformers/plans/general.hpp for translations into SAT.
    3. And see "Organisation" in Graphs/plans/general.hpp for translations from SAT to TSP.
    4. See "Travelling salesman" in Buildsystem/ExternalSources/SpecialBuilds/plans/SAT.hpp for installing external software.

Definition in file general.hpp.