@inproceedings{VanGelderTsuji96,
 Author = "Van Gelder, Allen and Tsuji, Yumi K.",
 Title = "Satisfiability Testing with More Reasoning and Less Guessing",
 Year = 1996,
 Editor = "Johnson, D. S. and Trick, M.",
 Publisher = "American Mathematical Society",
 Series = "DIMACS Series in Discrete Mathematics and Theoretical Computer
        Science", 
 BookTitle = "Cliques, Coloring, and Satisfiability: 
       Second DIMACS Implementation Challenge.", 
 NOTE = "(Appendix has Tutorial on Statistics in Satisfiability Research)",
 ANNOTE ="{Abstract: 
 A new algorithm for testing satisfiability of propositional formulas in 
 conjunctive normal form (CNF) is described.  It applies reasoning in the 
 form of certain resolution operations, and identification of equivalent 
 literals.  Resolution produces growth in the size of the formula, but within 
 a global quadratic bound; most previous methods avoid operations that 
 produce any growth, and generally do not identify equivalent literals.
 Computational experience so far suggests that the method does substantially
 less "guessing" than previously reported algorithms, while keeping a 
 polynomial time bound on the work done between guesses.  However, the
 time trade-off between reasoning and guessing is not yet clear.
 }",
 ANNOTE2="{
 We present experimental data comparing six branching strategies of the 
 proposed algorithm on a variety of problems, including several Dimacs
 benchmarks.  These branching strategies were shown to be different with 
 statistical significance and a new scheme based on Johnson's maximum 
 satisfiability approximation algorithm was the best on random 3-CNF formulas.
 In addition to the choice of a branching strategy, we found that 
 {\it variable reordering} can significantly impact the performance for many
 classes of problems in the Dimacs benchmark.  We have also tested both 
 satisfiable and unsatisfiable random 3-CNF formulas with 50-283 variables
 and 4.27 ratio of clauses to variables;  this class is generally acknowledged 
 to be relatively "hard" and required extensive backtracking by other 
 algorithms.  The new algorithm has solved them with surprisingly little 
 backtracking: for 200 variables at this ratio, the average number of guesses
 was 2,955 and the average CPU time was 119 seconds on SunSS10/41.  
 }",
 ANNOTE3="{
 For 283 variables, the average number of guesses was 57,503 with the
 values ranging from 105 to 182,006 in a set of 100 random formulas.
 We have also observed that unsatisfiable random problems do not follow the
 easy-hard-easy pattern.
 Our results indicate an exponential growth rate of
 $2^{.004L}$ for random formulas,
 where $L$ is the number of \emph{occurrences} of
 literals in the formula.
 Larger unsatisfiable formulas from circuit-fault analysis, with 500--10400
 variables were solved with \emph{no} backtracking in some cases.
 }"
}