Ten Challenges in Propositional Reasoning and Search

1 Introduction

Propositional reasoning is a core problem in many ar­ eas of artificial intelligence. In recent years this area has seen growing interest and activity, due to advances in our ability to solve large problem instances, including ones that encode real-world problems such as planning and diagnosis. Contributions to the area of propositional deduction and satisfiability testing have come from re­ search communities in artificial intelligence, operations research, and theoretical computer science. A set of key technical challenges have begun to emerge from interac­ tions within and among these research groups. We will describe some of these challenges and discuss why they are important for progress in the field.

For many years the problem of propositional reason­ ing received relatively little attention. It appeared that nothing could be done to improve upon the performance of the Davis-Putnam procedure (1960), which held its position as the most efficient satisfiability testing algo­ rithm for three decades. Furthermore, most researchers in artificial intelligence felt that the representational power of propositional logic was too limited, and turned their attention to first-order logic or even more powerful formalisms , such as various modal and non-monotonic logics. Several factors contributed to a renewed inter­ est in propositional reasoning. First, new algorithms were discovered, including ones based on stochastic local search as well as systematic search, that have better scal­ ing properties than the basic Davis-Putnam algorithm. Second, improvements in machine speed, memory size, and implementations extended the range of the algo­ rithms. Third, researchers began to develop and solve propositional encodings of interesting, real-world prob­ lems such as planning and diagnosis, with others on the horizon, such as natural language processing and ma­ chine learning. Such encodings were not even being con­ sidered a few years ago because they were thought to be far too large to be handled by any method. Between 1991 and 1996 the size of hard satisfiability problems that could be feasibly solved grew from ones involving less than 100 variables to ones involving over 10,000 vari­ ables.

Progress has been spurred by the interaction of re­ searchers in AI, operations research, and theory, in mak­ ing available benchmark problems (DIMACS, see Trick and Johnson 1996), holding joint workshops (Ginsberg 1995), and sharing algorithms and code. There is a grow­ ing consensus, however, that certain key technical chal­ lenges must be addressed in order to continue to increase the range of problems that can be practically solved. Work on propositional reasoning can be grouped in three core areas: systematic search; stochastic search; and problem encodings. For each area, we will discuss con­ crete challenges that have arisen. We stress that these challenges are not particularly our own invention, but rather summarize the issues that frequently arise in in­ formal discussions among researchers. Progress on any of these challenges would directly extend the usefulness of the propositional reasoning approach to problems in AI.

Because of the large number of references involved, we have not attempted to cite all related literature. However, a web page for these challenge problems has been constructed with a more complete bibliography, further details on the challenge problems, and point­ ers to existing satisfiability testing procedures. See http: j jwww .research.att.com;-selman/ challenge.

With each challenge, we give our best estimate of a time frame within which we think the challenge can be met. For the harder challenges, even partial solutions will constitute a significant contribution to the field.

2 Evaluation Criteria

The main evaluation criteria that has been adopted in the satisfiability testing (SAT) community is empirical performance on shared benchmark problems. We believe that this remains the best way to evaluate responses to any of the algorithmic challenges we will present. The alternative, evaluation by theoretical analysis, is prob­ lematic. Worst-case complexity results are all usually exponential. Furthermore, theoretical average case re­ sults are difficult to obtain, and can even be mislead­ ing because of the difficulty of formally characterizing problem distributions. Even when a sound theoretical analysis is devised, it may only characterize the asymp­ totic performance of the algorithm, and that asymptote may lie too far out (e.g., to problems containing trillions of variables) to be of practical consequence. Of course, theoretical analysis can be a very useful complement to empirical evaluation, and can help us gain insights into why an algorithm works well or poorly on a given prob­ lem distribution. (In fact, one of our non-algorithmic challenges , as we will see, is to develop a theoretical anal­ ysis that explains why local search works well on certain problem distributions.)

Reasonably good benchmark collections of satisfiabil­ ity problems, mainly in CNF form, are publically avail­ able from a number of sources. These include the DI­ MACS collection, which was used as a testbed for a large number of algorithms as reported in (Trick and Johnson 1996); a collection of circuit diagnosis problems encoded as SAT (Larrabee 1992); the planning problems Kautz and Selman (1996) devised for their SATPLAN system; hardware and software verification problems from the model checking community; and others. All these col­ lections have the property that published papers exist specifying the best known algorithms and running times for solving each of their instances.

Progress on any of our challenges (when applicable) will be measured by showing that the proposed method outperforms "11 other known methods on at least one set of benchmark problems. Some of our challenges in the area of problem encodings involve finding better ways to represent a real-world problem as SAT. In these cases, the empirical evaluation should involve comparing per­ formance of the best SAT algorithms on the proposed encoding against the best published results for any algo­ rithm that can solve the original (i.e. , unencoded) prob­ lem instances. In such a comparison it is usually not pos­ sible to outperform the specialized algorithms (although it is sometimes possible, see for example (Kautz and Sel­ man 1996)), but one should provide evidence that solv­ ing the encoded problem with general purpose Boolean satisfiability procedures is at least competitive.

Whenever possible, comparisons should also be made to the difficulty of solving the problems when alternative encodings are used, such as may be found in some of the benchmark sets. In cases where alternative encodings are available, one should show that the new encoding yields problems that are easier to solve by at least one state-of-the-art SAT procedure. (For example, it would be counted as progress if one developed a new encoding of planning problems that was good for stochastic search procedures, even if the encoding did not help systematic search procedures.)

In order to keep the criteria for comparison as objec­ tive as possible, it is important that results include total miming time. This may be adjusted for machine speed, but it is not sufficient to only report certain character­ istics of the execution, such as "number of nodes ex­ panded" (Johnson 1996). There are many ways to shift the computational effort in search algorithms - for ex­ ample, to visit fewer nodes by doing more work at each node - and an objective evaluation must consider the entire picture. Comparisons should cite the best results from the Operations Research and computer science the­ ory literature, as well as the AI literature.

Tests should be done on a variety of problem sizes, up to the hardest available instances that the method can solve. It is important to show the limits of the proposed method, that is, where it becomes highly exponential or otherwise fails. Often methods that look good on small instances break down on larger ones (Johnson 1996).

3 Challenging SAT Problems

We shall begin the list of challenges by citing two spe­ cific open SAT problems. The first is to develop a way to prove that unsatisfiable 700 variable 3-CNF formu­ las, randomly generated in the "hard" region where the ratio of variables to clauses is 4.3, are in fact unsatisfi­ able (Mitchell et al. 1992; Crawford and Auton 1993) . Randomly-generated satisfiable formulas of this size are regularly solved by stochastic search algorithms such as GSAT, but they are unable to prove unsatisfiability; and no systematic algorithm has been able to solve hard ran­ dom formulas of this size. A generator for these hard random problem instances can be found at the DIMACS benchmark archive (Trick and Johnson 1996).

CHALLENGE 1: (1-2 yrs) Prove that a hard 700 variable random 3-SAT formula is unsatisfiable.

The second challenge problem is satisfiable. It is an encoding of a 32-bit parity problem, that appears in the DIMACS benchmark set . It appears to be too large for current systematic algorithms. It also defeats the hill­ climbing techniques used by current local search algo­ rithms.

CHALLENGE 2: (2-5 yrs) Develop an algorithm that finds a model for the DIMA CS 32-bit parity problem.

For the second challenge, of course, the algorithm should not be told in advance the known solution! Given the amount of effort that has been spent on these two instances, any algorithm solving one or both will have to do something significantly different from current meth­ ods.

4 Challenges for Systematic Search

In the previous section we described two challenging SAT problems. In this section, and the next one, we describe promising ideas whose utility has not yet been demon­ strated. In each case the challenge is to demonstrate the utility of a currently known, but as yet unproven, approach to solving SAT problems. In keeping with the discussion in section 2, to demonstrate the utility of an idea one must construct a procedure which uses that idea in an essential way in solving at least one class of prob­ lems more effectively than any other known approach.

Our next challenge is using proof systems stronger than resolution. All of the best systematic methods for propositional reasoning are based on creating a resolu­ tion proof tree. This includes depth-first search algo­ rithms such as the Davis-Putnam procedure, where the proof tree can be recovered from the trace of the algo­ rithm's execution, but is not explicitly represented in a data structure (the algorithm only maintains a single branch of the proof tree in memory at any one time) . Most work on systematic search concentrates on heuris­ tics for variable-ordering and value selection, all in order to the reduce size of the tree.

However, there are known fundamental limitations on the size of the shortest resolution proofs for certain prob­ lems (Haken 1985; Chvatal and Szemeredi 1988) . For example, "pigeon hole" problems (showing that n pi­ geons cannot fit in n - 1 holes) are intuitively easy, but shortest resolution refutation proofs are of exponen­ tial length. Shorter proofs do exist in more powerful proof systems. Examples of proof systems more pow­ erful than resolution include extended resolution, which allows one to introduce new defined variables, and reso­ lution with symmetry-detection, which uses symmetries to eliminate parts of the tree without search. Assum­ ing N P f. co - N P, even the most powerful propo­ sitional proof systems would require exponential long proofs worst case - nonetheless, such systems provably dominate resolution in terms of minimum proof size.

However, at this point in time, attempts to mecha­ nize these more powerful proof systems usually yield no computational savings, because it is harder to find the small proof tree in the new system, than to simply crank out a large resolution proof. In essence, the overhead in dealing with the more powerful rules of inference con­ sumes all the potential savings. There is promising work in this area (Crawford et al. 1996; de la Tour and Demri 1995), but not yet convincing empirical results on a va­ riety of benchmark problems; such evidence would meet our third challenge:

CHALLENGE 3: (2-5 yrs) Demonstrate that a propositional proof system more powerful than resolution can be made practical for satisfiability testing.

Our next challenge is the use of integer programming techniques in solving SAT problems. It is straightfor­ ward to translate SAT problems into 0-1 integer pro­ gramming problems (Hooker 1988), and thus it has been argued that integer programming techniques should be useful for propositional reasoning. In fact, however, this has not been shown to be the case. For example, one of the main techniques in integer programming is to com­ pute the linear relaxation of the problem, and then to use the (easily-found) solution of the relaxed problem to guide the selection of values in solving the integer prob­ lem. However, in most formulations the solution to the linear relaxation of any SAT problem simply sets all the variables to the value "1/2" (modulo unit propagation) , thus yielding no guidance at all. Therefore we offer a challenge to show that the well-developed body of tools and techniques from Operations Research does in fact have something new to offer for propositional reasoning.

CHALLENGE 4: (2-5 yrs) Demonstrate that inte­ ger programming can be made practical for satisfiability testing.

5 Challenges for Stochastic Search

Stochastic local search has been shown to be a powerful alternative to systematic search for finding models of sat­ isfiable CNF formulas. Stochastic algorithms are inher­ ently incomplete, because if they fail to find a model for a formula one cannot be certain that the formula is unsat­ isfiable. This has led to an asymmetry in our ability to solve satisfiable and unsatisfiable instances drawn from the same problem distribution. Stochastic algorithms can solve hard random satisfiable formulas containing thousands of variables, but we cannot solve unsatisfiable instances of the same size.

Can local search be made to work for proving unsat­ isfiability? This apparently would require searching in space of refutation proofs, rather than in space of truth assignments. Each state would be an incomplete proof tree, e.g., a proof tree that rules out some fraction of the truth assignments. The neighborhood of a state would be similar proof trees. The step in the local search would try to transform the proof into one that rules out a larger fraction of assignments .

CHALLENGE 5: (5-10 yrs) Design a practical stochastic local search procedure for proving unsatisfia­ bility.

Our next challenge is that of distinguishing "depen­ dent" from "independent" variables . SAT encodings of structured problems such as planning and diagnosis of­ ten contain large numbers of variables whose values are constrained to be a simple Boolean function of other variables. We call these dependent variables. Variables whose values can not be easily determined to be a simple function of other variables are called independent. For a given SAT problem there may be many different ways to classify the variables as dependent and independent. But for most SAT encodings of real-world problems there is a natural division between dependent and indepen­ dent variables. Since an assignment to the independent variables determines a truth value for each dependent variable, the number of assignments that need be con­ sidered in a systematic search is at most 2" where n is the number of independent variables .

We belief that it fairly easy to empirically demonstrate that identification of dependent variables improves the performance of systematic search. It appears to be more difficult to establish that identification of dependent vari­ ables improves stochastic search. The challenge, there­ fore, is to improve local search for problems with de­ pendent variables: the search should concentrate only (or mainly) on the independent variables, and some fast mechanism should then set the dependent variables.

CHALLENGE 6: (1-2 yrs) Improve stochastic lo­ cal search on structured problems by efficiently handling variable dependencies.

As we have noted, systematic and local search proce­ dures outperform each other on different problem classes. Even putting the issue of incompleteness aside , there ex­ ist classes of satisfiable problems for which one or the other approach is clearly the winner. This leads to the general question: Can we develop a procedure that lever­ ages the strengths of each? The obvious way, of course, is to simply run good implementations of each approach in parallel. But is there a more powerful way of combining the two? Recently there has been some intriguing work on using local search to implement the variable ordering heuristic for systematic search (Boufkhad 1996; Mazure et al. 1996). These methods and other ways of combin­ ing systematic and stochastic search need to be further developed and compared with previous approaches on a range of benchmark problems.

CHALLENGE 7: (1-2yrs) Demonstrate the suc­ cesful combination of stochastic search and systematic search techniques, by the creation of a new algorithm that outperforms . the best previous examples of both ap-

6 Challenges for Problem Encodings

The value of research on propositional reasoning ulti­ mately depends on our ability to find suitable SAT en­ codings of real-world problems. As discussed in the in­ troduction, there has been significant recent progress along this front . Examples include classical constraint­ based planning (Blum and Furst 1995; Kautz and Sel­ man 1996) , problems in finite algebra (Fujita et al. 1993) , verification of hardware and software, scheduling (Craw­ ford and Baker 1994), circuit synthesis and diagnosis (Larrabee 1992), and many other domains. Experience has shown that different encodings of the same problem can have vastly different computational properties. For example, in planning, "causal" encodings appear to be harder to solve than "state-based" encodings.

A challenge, therefore, is to develop a general char­ acterization of encodings that can be efficiently solved. This characterization may involve, for example, under­ standing the relationship between the encoding and the shape of its search space. Note that the characterization cannot be as simple as stating that the search space has no local minima, because realistic problems will almost certainly have local minima. For example, the SAT en­ codings of blocks-world planning problems do have deep local minima, yet can be solved by local search. We need to understand why search can escape from local minima in some encodings but not in others. Perhaps one can find easily measurable statistical properties of the encoding that predict the behavior of various search algorithms on a given instance.

CHALLENGE 8: (5-10 yrs) Characterize the com­ putational properties of different encodings of a real­ world problem domain, and/or give general principles that hold over a range of domains.

Note that evaluation of progress on this last challenge cannot be purely empirical. There will be some sub­ jective judgement necessary in determining whether the characterization is useful and enlightening. Predictions of the theory can be put to an empirical test: in the best case, the general principles would suggest new encodings which can be solved more easily than previous ones.

One problem with all of the propositional encodings for real-world problems that have been suggested in the literature is that they are extremely "brittle". If we look at formulations where models that satisfy the encoding correspond to solutions to the original problem instance, we see little relationship between models that "almost" satisfy the encoded problem and candidate solutions that "almost" satisfy the original problem instance. For ex­ ample, Kautz and Selman (1992) noted that it was easy to find truth-assignments that satisfied all but a single clause of SAT encodings of blocks-world planning prob­ lems. These "near models" corresponded to making a series of random motions, and then, in the last state the blocks "magically" (violating physical constraints) arrange themselves in the correct position.

The robustness of encodings, and in particular, the robustness of local search algorithms applied to those encodings, could be improved by finding ways to more closely align the semantics of the SAT instance with the semantics of the source domain:

CHALLENGE 9: (1-2 yrs} Find encodings of real­ world domains which are robust in the sense that "near models" are actually "near solutions".

As we discussed earlier, benchmarks have been an im­ portant driving force behind work on propositional rea­ soning algorithms. Ideally one would have access to a very large number of real-world problem encodings, so that one could develop solid statistical evidence of the performance of various techniques. In practice the num­ ber of real problems that can be obtained is limited. It is extremely time-consuming and knowledge-intensive work to manually create such instances, and the largest and potentially most useful examples are often part of some proprietary project, and thus cannot be shared. Hard randomly-generated problems have proven to be a good alternative for testing - so far, the algorithms that are the best on randomly generated instances are also best on structured problems. However, there is the concern that we may be reaching a point where this is no longer the case, and that of the simple random dis­ tributions now used for testing may be driving us in the wrong direction in our research (Johnson 1996). There­ fore we present a final challenge, which if answered would provide vital tools for ensuring progress in this field .

CHALLENGE 10: (2-5 yrs) Develop a generator for problem instances that have computational properties that are more similar to real-world instances.

It is necessary to provide concrete evidence, empirical and/or theoretical, that the problem distribution so gen­ erated closely matches some set of real-world domains.

7 Conclusions

We have presented a series of technical challenge prob­ lems in the area of propositional reasoning and search. We believe that progress towards solving these problems will directly extend the usefulness of the propositional reasoning approach to problems in artificial intelligence, and computer science in general.