Plans for local search SAT algorithms at the Maxima/Lisp level in general.
More...
Go to the source code of this file.
Detailed Description
Plans for local search SAT algorithms at the Maxima/Lisp level in general.
 Todo:
 Relations to other modules
 Todo:
 A general framework

See [Stochastic Local Search: Foundations and Applications; Hoos, Stuetzle, 2005].

We should be able to establish a generic framework.

This generic framework should allow us to use specialised algorithm for hypergraph colouring (see "Faster local search" in Experimentation/Investigations/plans/VanderWaerdenProblems.hpp).
 Todo:
 Examing search landscapes

See "Framework for the analysis of search space structures" in Satisfiability/Algorithms/LocalSearch/plans/general.hpp.

A good overview is given by chapter 5 ("Search space structure
and SLS performance") in [Hoos, Stuetzle; Stochastic Local Search]; we should strive to implement all methods there at least in their exact versions.

Perhaps we should first consider ordinary satisfiability (boolean, and in clausal form), while generalisations come later.

Generalisations which apply to arbitrary optimisation problems perhaps should not be considered in this module, but for example in a supermodule ComputerAlgebra/LocalSearch.

For signed clausesets we consider the hypercube of total assignments (edges between total assignments which differ in exactly one position), where the vertices are labelled with the number of falsified clauses.

One could then consider the directed graph with edges only to positions where the score is improved.

Additionally we should look into the literature on random problems and statistical physics (see also the work of Elitza Maneva et al).
 Todo:
 Theoretical random walk algorithms

The base cases are Papadimitriou's and Schoening's algorithms.

They should be easy instances of the generic framework.

What to do with these implementations:

They serve educational purposes.

Regarding their real efficiency, since they only use features which are analysable (to a certain extend), they should be inferior to "practical" schemes.

Perhaps one could also integrate their analysis into our system.

And worsecase instances are of interest.

As well as general evaluations of their runtime behaviour (which should be simpler, since "purer", than for practical schemes).
Definition in file general.hpp.