Ten Challenges for SAT Solving

At the occasion of the symposium Assessing the Progress (Baltimore, USA, March 2008), OK proposed 10 challenges for SAT solving he considers fundamental:

The slogans for the ten challenges (together with some related material) are as follows:

  1. Improve the quantitative understanding of heuristics (for DPLL-like algorithms).
  2. Apply advanced methods like time-series analysis, techniques from risk-assessment or even option-theory (suitably generalised) to make informed decisions.
  3. Generalise methods from combinatorics, reveal their "SAT-core".
  4. Develop a much more precise and useful theory of proof systems.
  5. Create maps of the universe of NP-problems and their translations.
  6. Develop a theory and framework of generalised satisfiability.
  7. Combine the theory of generalised satisfiability with the theories from commutative algebra and algebraic geometry.
  8. Develop a natural algorithm combining the three paradigms (local search, look-ahead, conflict-driven).
  9. Make graph/hypergraph methods successful and all the other poly-time methods.
  10. Develop sound software development practice and software usage practice, together with powerful tools.

Oliver Kullmann

Last modified: Thu Nov 17 18:29:27 GMT 2011