This paper has begun the task of formally analyzing the power of clause learning from a proof complexity perspective. Understanding where clause learning stands in relation to well studied proof systems should lead to better insights on why it works well on certain domains and fails on others. For instance, pebbling problems are an example of a domain where our results say that learning is necessary and sufficient, given a good branching order, to obtain sub-exponential solutions using DPLL based methods. On the other hand, the connection with resolution also implies that any problem that contains as a sub-problem a formula that is inherently hard even for RES, such as the pigeonhole principle (Haken, 1985), must be hard for any variant of clause learning. For such domains, theoretical results suggest practical extensions such as symmetry breaking and counting techniques for obtaining efficient solutions.
The complexity results in this paper are about proofs of unsatisfiability, and hence apply directly only to the unsatisfiable version of the pebbling formulas. Despite this, the experiments show a clear speed-up on satisfiable versions as well. This, as mentioned in Section 1, can be explained by the idea of Achlioptas et al. (2001): any DPLL based algorithm run on a satisfiable problem instance will take a long time to run precisely when the algorithm encounters an unsatisfiable sub-problem of the original problem on which it must take a long time. This lets one translate hardness results from unsatisfiable formulas to their satisfiable counterparts.
This paper inspires but leaves open several interesting questions of proof complexity. We showed that there are formulas on which CL is much more efficient than any proper natural refinement of RES. In general, can every short refutation in any such refinement be converted into a short CL proof? Or are these refinements and CL incomparable? We have shown that with arbitrary restarts, a slight variant of CL is as powerful as RES. However, judging when to restart and deciding what branching sequence to use after restarting adds more nondeterminism to the process, making it harder for practical implementations. Can CL with limited restarts also simulate RES efficiently?
In practice, a solver must employ good branching heuristics as well as implement a powerful proof system. Our results that pebbling formulas have short CL proofs depends critically upon the solver choosing a branching sequence that solves the formula in a ``bottom-up'' fashion, so that the learned clauses have maximal reuse. Nevertheless, we were able to automatically generate such sequences for grid and randomized pebbling formulas. Although somewhat artificial and capturing the narrow domain of task precedence, pebbling graphs are structurally similar to the layered graphs induced naturally by problems involving unwinding of state space over time, such as STRIPS planning (Kautz and Selman, 1992) and bounded model checking (Biere et al., 1999b). Pebbling problems also provide hard instances for some of the best existing SAT solvers like zChaff. This bolsters our belief that high level structure can be recovered and exploited to make clause learning more efficient.
The form in which we extract and use problem structure is a branching sequence. Although capable of capturing more information than a static variable order and avoiding the overhead of dynamic branching schemes, the exactness and detail branching sequences seem to require for pebbling formulas might pose problems when we move to harder domains where a polynomial size sequence is unlikely to exist. We may still be able to obtain substantial (but not exponential) improvements as long as an incomplete or approximate branching sequence made correct decisions most of the time, especially near the top of the underlying DPLL tree. The performance gains reported for GTn formulas indicate that even a very simple and partial branching sequence can make a big difference in practice. Along these lines, variable orders in general have been studied in other scenarios, such as for algorithms based on BDDs (see e.g.,Aziz et al., 1994, Harlow and Brglez, 1998). There has been work on using BDD variable orders for DPLL algorithms without learning (Reda et al., 2002). The ideas here can potentially provide new ways of capturing structural information.
Finally, our approach of exploiting high level problem description to generate auxiliary information for SAT solvers requires the knowledge of this high level description. The standard CNF benchmarks, unfortunately, do not come with such a description. Of course, there is no reason for this information to not be available since CNF formulas for practically all real-world problems are created from a more abstract specification.