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 slides from the Baltimore-talk contain the basic discussion.
• Here is the directory containing plans and other material for each of the challenges.

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).
   • See the chapter Fundaments of Branching Heuristics in the Handbook of Satisfiability (the pdf-file is available here ).
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".
   • See the chapter Minimal Unsatisfiability and Autarkies in the Handbook of Satisfiability (the pdf-file is available here ).
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.

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