A revolution?

Furthermore, a completely new approach to solve SAT appeared last year, resulting from the existence of huge SAT instances encoding some specific problems, such as planning [KS92,KS96,EMW97] or more recently Bounded Model Checking [BCC$^+$99,ABE00,VB01]. While most of the underlying techniques are not new (DPLL with intelligent backtracking, learning and a rapid restart strategy), one of the main idea was to focus on a carefully engineered solver: when dealing with a huge instance, choosing the right algorithm or data structure is as important as choosing the right heuristic to reduce the search space. Chaff [MMZ$^+$01,ZMMM01] was designed from the begining to handle large formulas (more than 100000 variables) from a very specific area (mostly Bounded Model Checking) using ``lazy'' data structures. Since there is no heuristic shown to be efficient on EDA instances, Chaff also integrated a new form of learning, taking advantage of the overall lazy data structures used: Chaff makes mistakes, but learns quickly! Chaff outperformed existing SAT solvers on Bounded Model Checking instances, and a large set of ``structured'' (as opposed to random) instances [SC01]. It looked interesting to establish a new overall picture of SAT kingdom after that ``revolution''.

Such a competition allows to obtain both new solvers and new benchmarks. It was proved to stimulate the community (more than just by providing awards to it). Many breakthroughs in the last years were due to empirical evaluation of algorithms, leading to a better knowledge of algorithms behaviors and of benchmarks hardness. This knowledge allow to propose (and test) new answers. Such a competition can thus be viewed as one of the fundamental part of the research around the topic.