High-performance SAT solvers based on systematic search generally use either conflict driven clause learning (CDCL) or lookahead techniques to gain efficiency. Both styles of reasoning can gain from a preprocessing phase in which some form of deduction is used to simplify the problem. In this paper we undertake an empirical examination of the effects of several recently proposed preprocessors on both CDCL and lookahead-based SAT solvers. One finding is that the use of multiple preprocessors one after the other can be much more effective than using any one of them alone, but that the order in which they are applied is significant. We intend our results to be particularly useful to those implementing new preprocessors and solvers.
In the last decade, the propositional satisfiability (SAT) has become one of the most interesting research problems within artificial intelligence (AI). This tendency can be seen through the development of a number of powerful SAT solvers, based on either systematic search or stochastic local search (SLS), for solving various hard combinatorial search problems such as automatic deduction, hardware and software verification, planning, scheduling, and FPGA routing.
The power of contemporary systematic SAT solvers derives not only from the underlying Davis-Putnam-Logemann-Loveland (DPLL) algorithm but also from enhancements aimed at increasing the amount of unit propagation, improving the choices of variables for splitting or making backtracking more intelligent. Two of the most important such enhancements are conflict driven clause learning (CDCL), made practicable on a large scale by the watched literal technique, and one-step lookahead. These two tend to exclude each other: the most successful solvers generally incorporate one or the other but not both. The benefits they bring are rather different too, as is clear from the results of recent SAT competitions. For problems in the “industrial” category, CDCL, as implemented in MINISAT [ES03, SE05], siege [Rya04] and zChaff [MMZ+01, ZMMM01] is currently the method of choice. On random problems, however, lookahead-based solvers such as Dew Satz [AS05], Kcnfs [DD01] and March dl [HvM06] perform better.
Lookahead, of course, is expensive at every choice node, while clause learning is expensive only at backtrack points. Since half of the nodes (plus one) in any binary tree are leaves, this difference is significant for lookahead-based solvers which process nodes relatively slowly and gain, if at all, by reducing the search tree size. Looking ahead is an investment in at-node processing which can pay off only if it results in more informed choices with an impact on the total number of nodes visited. Where learnt clauses prune the tree at least as effectively as complex choice heuristics, CDCL must win. This seems to be the case in many classes of highly structured problems such as the “industrial” ones in the SAT competitions. We have no clearer definition than anyone else of “structure”, but are interested to find ways in which lookahead-based solvers might detect and exploit it as well as the clause learners do.
A noteworthy feature of many recent systems is a preprocessing phase, often using inference by some variant of resolution, to transform problems prior to the search. One suggestion we wish to make and explore is that such transformations may help lookahead-based solvers to discover useful structure. That is, much of the reasoning done by nogood inference might be done cheaply “up-front”, provided that the subsequent variable choice heuristics are good enough to exploit it. In what follows, we are therefore concerned mainly with the effects of preprocessing, including those of using multiple preprocessors in series, on the performance of a lookahead-based solver Dew Satz on problems where it does poorly in comparison with a clause learning solver (MINISAT). We also include some results and remarks on benefits to be gained in the opposite direction, where MINISAT is helped by preprocessing to attack problems to which Dew Satz is more suited.
In this paper we propose a multiple preprocessing technique to boost the performance of systematic SAT solvers. The motivation for applying multiple preprocessors prior to the systematic search process is clear: each preprocessor uses a different strategy in objective to simplify clause sets derived from real-world problems that exhibit a great deal structure such as symmetries, variable dependencies, clustering, and the like. Our initial observation showed that each strategy works well for simplifying the structure of some problems, at most of the time, from hard to easy. When a problem exhibits different kinds of structure, then a single preprocessor has difficulty to simplify the structures. In this case, we need to run multiple preprocessors one after the other.
We report performance statistics for the two solvers, Dew Satz and MINISAT, with and without combinations of five (and for one problem set, six) of the best contemporary SAT preprocessors when solving parity, planning, bounded model checking and FPGA routing benchmark problems from SATLIB and the recent SAT competitions. One finding is that the use of multiple preprocessors one after the other can be much more effective than using any one of them alone, but that the order in which they are applied is significant. We intend our results to be particularly useful to those implementing new preprocessors and solvers.
The rest of the paper is organized as follows: section 2 addresses the related work. In sections 3 and 4, we briefly describe the preprocessors and solvers examined in our study. The main part of the paper consists of experimental results, and we conclude with a few remarks and suggestions.
Resolution-based SAT preprocessors for CNF formula simplification have a dramatic impact on the performance of even the most efficient SAT solvers on many benchmark problems [LMS01]. The simplest preprocessor consists of just computing length-bounded resolvents and deleting duplicate and subsumed clauses, as well as tautologies and any duplicate literals in a clause.
There are two most directly related works. The first one is that of Anbulagan et al. [APSS06] which examined the integration of five resolution-based preprocessors alone or the combination of them with stochastic local search (SLS) solvers. Their experimental results show that SLS solvers benefit the present of resolution-based preprocessing and multiple preprocessing techniques. And the second one is that of Lynce and Marques-Silva [LMS01]. They only evaluated empirically the impact of some preprocessors developed before 2001 including 3-Resolution, without considering multiple preprocessing, on the performance of systematic SAT solvers. In recent years, many other preprocessors, which are sophisticated, have been applied to modern propositional reasoners. Among them are 2-SIMPLIFY [Bra01], the preprocessor in Lsat [OGMS02] for recovering and exploiting Boolean gates, HyPre [Bac02, BW04], Shatter [ASM03] for dealing with symmetry structure, NiVER [SP05] and SatELite [EB05]. We consider some of these preprocessors plus 3-Resolution in our study. 3
We describe briefly the six SAT preprocessors used in the experiments. The first five are all based on resolution and its variants such as hyper-resolution. Resolution [Qui55, DP60, Rob65] itself is widely used as a rule of inference in first order automated deduction, where the clauses tend to be few in number and contain few literals, and where the reasoning is primarily driven by unification. As a procedure for propositional reasoning, however, resolution is rarely used on its own because in practice it has not been found to lead to efficient algorithms. The sixth preprocessor is a special-purpose tool for symmetry detection, which is important for one problem class in the experiments. 3.1 k-Resolution is just saturation under resolution with the restriction that the parent clauses are of length at most k. The special cases of 2-Resolution and 3-Resolution are of most interest. 3-Resolution has been used in a number of SAT solvers, notably Satz [LA97] and the SLS solver R+AdaptNovelty+ [APSS05] which won the satisfiable random problem category in the SAT2005 competition. Since it is the preprocessor already used by Satz, we expect it to work well with Dew Satz. 3.2
2-SIMPLIFY 2-SIMPLIFY [Bra01] constructs an implication graph from all binary clauses in the problem. Where there is an implication chain from a literal X to X, X can be deduced as a unit which can be propagated. The method also collapses strongly connected components, propagates shared implications, or literals implied in the graph by every literal in a clause, and removes some redundant binary clauses. Experimental results [Bra01, Bra04] show that systematic search benefits markedly from 2-SIMPLIFY on a wide range of problems. 3.3
HyPre [BW04] also reasons with binary clauses, but incorporates full hyper-resolution, making it more powerful than 2-SIMPLIFY. In addition, unit reduction and equality reduction are incrementally applied to infer more binary clauses. It can be costly in terms of time, but since it is based explicitly on hyper-resolution it avoids the space explosion of computing a full transitive closure. HyPre has been used in the SAT solver, 2CLS+EQ [Bac02], and we consider it a very promising addition to many other solvers. It is generally useful for exploiting implicational structure in large problems. 3.4
Variable Elimination Resolution (VER) is an ancient inference method consisting of performing all resolutions on a chosen variable and then deleting all clauses in which that variable occurs, leaving just the resolvents. It is easy to see that this is a complete decision procedure for SAT problems, and almost as easy to see that it is not practicable because of exponential space complexity. Recently, Subbarayan and Pradhan [SP05] proposed NiVER (Non increasing VER) which restricts the variable elimination to the case in which there is no increase in the number of literals after elimination. This shows promise as a SAT preprocessor, improving the performance of a number of solvers [SP05]. 3.5
E´en and Biere [EB05] proposed the SatELite preprocessor, which extends NiVER with a rule of Variable Elimination by Substitution. Several additions including subsumption detection and improved data structures further improved performance in both space and time. SatELite was combined with MINISAT to form SatELiteGTI, the system which dominated the SAT2005 competition on the crafted and industrial problem categories. Since we use MINISAT for our experiments, it is obvious that SatELite should be one of the preprocessors we consider. 3.6
It is clear that eliminating symmetries is essential to solving realistic instances of many problems. None of the resolution-based preprocessors does this, so for problems that involve a high degree of symmetry we added Shatter [AMS03] which detects symmetries and adds symmetry-breaking clauses. These always increase the size of the clause set and for satisfiable problems they remove some of the solutions, but they typically make the problem easier by pruning away isomorphic copies of parts of the search space.
4.1
MINISAT As noted in Section 1, we concentrate on just two solvers: MINISAT, which relies on clause learning, and Dew Satz, which uses lookahead.
So¨rensson and E´en [ES03, SE05] released the MINISAT solver in 2005. Its design is based on Chaff, particularly in that it learns nogoods or “conflict clauses” and accesses them during the search by means of two watched literals in each clause. MINISAT is quite small (a few hundred lines of code) and easy to use either alone or as a module of a larger system. Its speed in comparison with similar solvers such as zChaff comes from a series of innovations of which the most important are an activity-decay schedule which proceeds by frequent small reductions rather than occasional large ones, and an inference rule for reducing the size of conflict clauses by introducing a restricted subsumption test. The cited paper contains a brief but informative description of these ideas. 4.2
The solver Dew Satz [AS05] is a recent version of the Satz solver [LA97]. Like its parent Satz, it gains efficiency by a restricted one-step lookahead scheme which rates some of the neighbouring variables every time a choice must be made for branching purposes. Its lookahead is more sophisticated than the original one of Satz, adding a DEW (dynamic equality weighting) heuristic to deal with equalities. This enables the variable selection process to avoid duplicating the work of weighting variables detected to be equivalent to those already examined. Thus, while the solver has no special inference mechanism for propositional equalities, it does deal tolerably well with problems containing them. 5
We present results on four benchmark problem sets chosen to present challenges for one or other or both of the SAT solvers. The experiments were conducted on a cluster of 16 AMD Athlon 64 processors running at 2 GHz with 2 GB of RAM. Ptime in the tables represents preprocessing time, while Stime represents solvers runtime without including Ptime. The timebound of Stime is 15,000 seconds per problem instance. It is worth noting that in our study the results of SatELiteGTI, the solver which dominated the SAT2005 competition on the crafted and industrial problem categories, are represented by the results of SatELite+MINISAT. 5.1
The 32-bit parity problem was listed by Selman et al. [SKM97] as one of ten challenges for research on satisfiability testing. The ten instances of the problem are satisfiable. The first response to this challenge was by Warners and van Maaren [WvM98] who solved the par32-*-c problem (5 instances) using a special-purpose preprocessor to deal with equivalency conditions. Two years later, Li [Li00] solved the ten par32* instances by enhancing Satz’s search process with equivalency reasoning. Ostrowski et par32-1 par32-2 par32-3 par32-4 par32-5 par32-1-c par32-2-c par32-3-c par32-4-c par32-5-c
Orig 3Res Hyp+3Res Niv+3Res 3Res+Hyp Sat+3Res Orig 3Res Hyp+3Res Niv+3Res Orig 3Res Hyp+3Res Niv+3Res Sat+3Res Orig 3Res Sat Hyp+3Res 3Res+Hyp Niv+3Res 3Res+Niv 3Res+Sat Sat+3Res Sat+2Sim Orig Niv Orig 3Res Hyp+3Res Orig 3Res Hyp+3Res Orig 3Res Hyp Hyp+3Res Niv+3Res Sat+3Res Orig 3Res Hyp+3Res Niv+3Res Sat+3Res Orig Niv+3Res al. [OGMS02], solved the problems with Lsat, which performs a preprocessing step to recover and exploit the logical gates of a given CNF formula and then applies DPLL with a Jeroslow-Wang branching rule. The challenge has now been met convincingly by Heule et al. [HvM04] with their March eq solver, which combines equivalency reasoning in a preprocessor with a lookahead-based DPLL and which solves all of the par32* instances in seconds. Dew Satz is one of the few solvers to have solved any instances of the 32-bit parity problem without special-purpose equivalency reasoning [AS05].
Table 1 shows the results of running the lookahead-based solver Dew Satz and the CDCL-based solver MINISAT on the ten par32 instances, with and without preprocessing. As preprocessors we used 3-Resolution, HyPre, NiVER and SatELite alone and followed by 3-Resolution for the last three. We eliminated 2-SIMPLIFY from this test as it aborted the resolution process of the first five par32* instances presented in the Table 1. We experimented also with all combination of two preprocessors for the problems par32-1 and par32-4. Where lines are omitted from the table (e.g. there is no line for HyPre on par32-1 and for SatELite+3-Resolution on par32-2), this is because no single solver produced a solution for those simplified instances.
It is evident from the table that these problems are seriously hard for both solvers. Even with preprocessing, MINISAT times out on all of them except for par32-2 and par32-5-c. Curiously, on par32-2 instance, preprocessing with 3-Resolution makes its performance degrade a little. This is not a uniform effect: Table 4 below shows examples in which MINISAT benefits markedly from 3-Resolution. Without preprocessing, Dew Satz times out on nine of ten par32 instances, but in every case except par32-5 and par32-5-c 3-Resolution suffices to help it find a solution, and running multiple preprocessors improves its performance.
In general, Table 1 shows that multiple preprocessing contributes significantly to enhance the performance of Dew Satz and the preprocessor 3-Resolution dominates the contribution through either single or multiple preprocessing. 5.2
The ferry planning benchmark problems, taken from SAT2005 competition, are all easy for MINISAT, which solves all of them in about one second without needing preprocessors. Dew Satz, however, is challenged by them. The problems are satisfiable. We show the Dew Satz and MINISAT results on the problems in Table 2. Clearly the original problems contain some structure that CDCL is able to exploit but which is uncovered by one-step lookahead. It is therefore interesting to see which kinds of reasoning carried out in a preprocessing phase are able to make that same structure available to Dew Satz. Most strikingly, reasoning with binary clauses in the manner of the 2-SIMPLIFY preprocessor reduces runtimes by upwards of four orders of magnitude in some cases. HyPre, NiVER and SatELite, especially HyPre, are also effective on these planning problems. In most cases the number of backtracks reduces from million to less than 100 or even zero for ferry8 v01a, ferry9 v01a, and ferry10 ks99a instances which means that the input formula is solved at the root node of the search tree. 1946/22336/45706 1930/22289/45621 1881/32855/66732 1543/21904/45243 1286/21601/50644 1279/56597/120318
Stime Another domain providing benchmark problem sets which appear to be easy for MINISAT but sometimes hard for Dew Satz is bounded model checking. In Table 3 we report results on five of eleven BMC-IBM problems, two BMC-galileo problems and two of four BMC-alpha problems. All other benchmark problems in the BMC-IBM class are easy for both solvers and so are omitted from the table. The other two BMC-alpha instances are harder than the two reported even for MINISAT before and after preprocessing. The problems presented in Table 3 are satisfiable.
Each of these bounded model checking problems is brought within the range of Dew Satz by some form of preprocessing. In general, HyPre and 3-Resolution are the best for this purpose, especially when used together, though on problem BMC-IBM-13 they are ineffective without the additional use of NiVER. The column showing the number of times Dew Satz backtracks is worthy of note. In many cases, preprocessing reduces the problem to one that can be solved without backtracking. Solving “without backtracking” has to be interpreted with care here, of course, since a nontrivial amount of lookahead may be required in a “backtrack-free” search. The results for BMC-galileo-9 furnish a good example of this: HyPre takes 407 seconds to refine the problem, following which Dew Satz spends 90 seconds on lookahead reasoning while constructing the first (heuristic) branch of its search tree, but then that branch leads directly to a solution. Adding 3-Resolution to the preprocessing step does not change the number of variables, and only slightly reduces the number of clauses, but it roughly halves the time subsequently spent on lookahead.
The instance BMC-alpha-4408 is hard for Dew Satz even after preprocessing. While MINISAT with multiple preprocessing solves the problem instance with an order of magnitude faster. We can also observe that HyPre brings more benefit than SatELite,
Table 4 shows results for both solvers on a related problem set consisting of formal verification problems taken from the SAT2005 competition. The IBM-FV-01 problems are satisfiable except for the problem IBM-FV-01-k10; the IBM-FV-26 problems are unsatisfiable. Most of these satisfiable problems are easy for MINISAT, but the unsatisfiable cases show that the SatELite preprocessor (with which MINISAT was paired in the competition) is by far the least effective of the four we consider for MINISAT on these problems. The preprocessor HyPre proved the unsatisfiability of IBM-FV-01-k10 in 1.27 seconds. 2-SIMPLIFY was not used to simplify the IBM-FV-26 problems, because it is limited for input formula with maximum 100,000 variables. Again there are cases in which Dew Satz is improved from a 15,000 second timeout to a one-branch proof of unsatisfiability. Note that the numbers of clauses in these cases are actually increased by the preprocessor 3-Resolution, confirming that the point of such reasoning is to expose structure rather than to reduce problem size. 5.4
FPGA routing problem is a higly symmetrical problem that model the routing of wires in the channels of field-programmable integrated circuits [AMS03]. The problem instances used in the experiment, which were artificially designed by Fadi Aloul, are taken from SAT2002 competition.
Without preprocessing to break symmetries, many of the FPGA routing problems are hard—harder for CDCL solvers than for lookahead-based ones. Not only do they have many symmetries, but the clause graphs are also disconnected. Lookahead techniques with neighbourhood variables ordering heuristic seem able to choose inferences within one graph component before moving to another, whereas MINISAT jumps frequently between components. Table 5 shows performances of both solvers on FPGA routing problem set. Of 21 selected satisfiable (bart) problems, MINISAT solves 8 in some 2 hours. It manages better with the unsatisfiable (homer) instances, solving 14 of 15 in a total time of around 6 hours. Dew Satz solves all of the bart problems in 17.5 seconds and the homer ones in 45 minutes.
The detailed results for two of the satisfiable problems and two unsatisfiable ones (Table 6) are interesting. The resolution-based preprocessors do not give any modification to the size of the input formula except when using SatELite. The Shatter preprocessor, which removes certain symmetries, is tried on its own and in combination with the five resolution-based preprocessors. It should be noted that the addition of symmetry-breaking clauses increases the sizes of the problems, but of course it greatly reduces the search spaces in most cases.
The performance of Dew Satz after preprocessing is often worse in terms of time than it was before, though there is always a decreases in the size of its search tree. This is because of the increase in the problem size which increases the amount of lookahead process. MINISAT, by contrast, sometimes speeds up by several orders of magnitude after preprocessing. Table 7 illustrates the difficulty of selecting the order in which to apply multiple preprocessors. It shows results on just two sample problems. The first is the bounded model checking problem BMC-IBM-12, which Dew Satz attempted with the three preprocessors HyPre, NiVER and 3-Resolution in different orders. Only one order, NiVER followed by HyPre followed by 3-Resolution, renders the problem feasible for Dew Satz. With the preprocessors in that order, it is solved in less than 2 minutes; with any other order it cannot be solved in more than four hours. The second problem, ferry10 ks99a, shows the range of different outcomes produced by varying the order of four preprocessors. If we get it right, we get a solution in 5 seconds, but we know of no simple rule for getting it right in such a case. Neither running NiVER first nor running 3-Resolution last is sufficient. Even with NiVER, HyPre and 3-Resolution in the right order, putting 2SIMPLIFY first rather than third changes the runtime from 5 seconds to several hours. The third experiment illustrates the efffect of alternating two preprocessors. Simplifying bart28 bart30 homer19 homer20
Orig Sat Sha Sha+3Res Sha+Hyp Sha+Niv Sha+Sat Sha+2Sim Orig Sat Sha Sha+3Res Sha+Hyp Sha+Niv Sha+Sat Sha+2Sim Orig Sat Sha Sha+3Res Sha+Hyp Sha+Niv Sha+Sat Sha+2Sim Orig Sat Sha Sha+3Res Sha+Hyp Sha+Niv Sha+Sat Sha+2Sim
n/a 6,066,241
290,871 8,216,100 with 2-SIMPLIFY followed by NiVER is insufficient to allow solution before the timeout. Simplifying again with 2-SIMPLIFY brings the runtime down to under an hour; adding NiVER again brings it down again to a couple of minutes; repeating 2-SIMPLIFY, far from improving matters, causes the time to blow out to two hours. 6
We performed an empirical study of the effects of several recently proposed SAT preprocessors on both CDCL and lookahead-based SAT solvers. We describe several outcomes from this study as follow.
1. High-performance SAT solvers, whether they depend on clause learning or on lookahead, benefit greatly from preprocessing. Improvements of four orders of magnitude in runtimes are not uncommon. 2. It is unlikely to equip a SAT solver with just one preprocessor of the kind considered in this paper. Very different preprocessing techniques are appropriate to different problem classes. 3. There are frequently benefits to be gained from running two or more preprocessors in series on the same problem instance. 4. Both clause learning and lookahead need to be enhanced with techniques specific to reasoning with binary clauses, in order to exploit dependency chains, and with techniques for equality reasoning. 5. Lookahead-based solvers also benefit greatly from resolution between longer clauses, as in the 3-Resolution preprocessor. This seems to capture ahead of the search some of the inferences which would be achieved during it by learning clauses. CDCL solvers can also benefit from 3-Resolution preprocessor—dramatically in certain instances—but the effects are far from uniform. 6.1
The following lines of research are open: 1. It would, of course, be easy if tedious to extend the experiments to more problem sets, more preprocessors and especially to more solvers. We shall probably look at some more DPLL solvers, but do not expect the results to add much more than detail to what is reported in the present paper. One of the more important additions to the class of solvers will be a non-clausal (Boolean circuit) reasoner. We have not yet experimented with such a solver. We have already investigated preprocessing for several state of the art SLS (stochastic local search) solvers, but that is such a different game that we regard it as a different experiment and do not report it here. 2. The more important line of research is to investigate methods for automatically choosing among the available preprocessors for a given problem instance, and [AMS03] for automaticallly choosing the order in which to apply successive preprocessors. Machine learning may help here, though it would be better, or at least more insightful, to be able to base decisions on a decent theory about the interaction of reasoning methods. 3. Another interesting project is to combine preprocessors not as a series of separate modules but as a single reasoner. For example, it would be possible to saturate under 3-Resolution and hyper-resolution together, in the manner found in resolution-based theorem provers. Whether this would be cost-effective in terms of time, and whether the results would differ in any worthwhile way from those obtained by ordering separate preprocessors, are unknown at this stage.
As SAT solvers are increasingly applied to real-world problems, we expect deductive reasoning by preprocessors to become increasingly important to them.
This work was funded by National ICT Australia (NICTA). National ICT Australia is funded through the Australian Government’s Backing Australia’s Ability initiative, in part through the Australian Research Council.
Fadi A. Aloul, Igor L. Markov, and Karem A. Sakallah. Shatter: Efficient symmetry-breaking for boolean satisfiability. In Design Automation Conference, pages 836–839. ACM/IEEE, 2003.
Anbulagan, Duc Nghia Pham, John Slaney, and Abdul Sattar. Old resolution meets modern SLS. In Proceedings of 20th AAAI, pages 354–359, 2005.
Anbulagan, Duc Nghia Pham, John Slaney, and Abdul Sattar. Boosting SLS performance by incorporating resolution-based preprocessor. In Proceedings of Third International Workshop on Local Search Techniques in Constraint Satisfaction (LSCS), in conjunction with CP-06, pages 43–57, 2006.
Anbulagan and John Slaney. Lookahead saturation with restriction for SAT. In Proceedings of 11th CP, pages 727–731, 2005.
Fadi A. Aloul, Karem A. Sakallah, and Igor L. Markov. Efficient symmetry breaking for boolean satisfiability. In Proceedings of 18th IJCAI, Mexico, 2003.
Fahiem Bacchus. Enhancing Davis Putnam with extended binary clause reasoning. In Proceedings of 18th AAAI, pages 613–619, Edmonton, Canada, August 2002. AAAI Press. [Bra01] [Bra04] [BW04] [DD01] [DP60] [EB05] [ES03] [HvM04] [HvM06] [LA97] [Li00] [LMS01]
Ronen I. Brafman. A simplifier for propositional formulas with many binary clauses. In Proceedings of 17th IJCAI, pages 515–522, 2001.
Ronen I. Brafman. A simplifier for propositional formulas with many binary clauses. IEEE Transactions on Systems, Man, and Cybernetics, Part B, 34(1):52–59, 2004.
Fahiem Bacchus and Jonathan Winter. Effective preprocessing with hyperresolution and equality reduction. In Revised Selected Papers of SAT 2003, LNCS 2919 Springer, pages 341–355, 2004.
Olivier Dubois and Gilles Dequen. A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In Proceedings of 17th IJCAI, pages 248– 253, Seattle, Washington, USA, 2001.
M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201–215, 1960.
Niklas E´en and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Proceedings of 8th SAT, LNCS Springer, 2005.
Niklas E´en and Niklas Sorensson. An extensible SAT-solver. In Proceedings of 6th SAT, 2003.
Marijn Heule and Hans van Maaren. Aligning CNF- and equivalencereasoning. In Proceedings of 7th SAT, Vancouver, Canada, 2004.
Marijn Heule and Hans van Maaren. March dl: Adding adaptive heuristics and a new branching strategy. Journal on Satisfiability, Boolean Modeling and Computation, (2):47–59, 2006.
Chu Min Li and Anbulagan. Look-ahead versus look-back for satisfiability problems. In Proceedings of 3rd CP, pages 341–355, Schloss Hagenberg, Austria, 1997.
Chu Min Li. Integrating equivalency reasoning into Davis-Putnam procedure. In Proceedings of 17th AAAI, pages 291–296, USA, 2000. AAAI Press.
I. Lynce and J. Marques-Silva. The interaction between simplification and search in propositional satisfiability. In Proceedings of CP’01 Workshop on Modeling and Problem Formulation, 2001. [MMZ+01] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of DAC, pages 530–535, 2001. [OGMS02] Richard Ostrowski, E´ric Gr´egoire, Bertrand Mazure, and Lakhdar Sais.
Recovering and exploiting structural knowledge from CNF formulas. In Proceedings of 8th CP, pages 185–199, 2002. [Rob65] [SE05] [SKM97] [SP05] [WvM98]