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:

- 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 ).

- Apply advanced methods like time-series analysis, techniques from risk-assessment or even option-theory (suitably generalised) to make informed decisions.
- 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 ).

- Develop a much more precise and useful theory of proof systems.
- Create maps of the universe of NP-problems and their translations.
- Develop a theory and framework of generalised satisfiability.
- Combine the theory of generalised satisfiability with the theories from commutative algebra and algebraic geometry.
- Develop a natural algorithm combining the three paradigms (local search, look-ahead, conflict-driven).
- Make graph/hypergraph methods successful and all the other poly-time methods.
- 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