@inproceedings{VanGelderTsuji93,
 Author = "Van Gelder, Allen and Tsuji, Yumi K.",
 Title = "Incomplete Thoughts about Incomplete Satisfiability Procedures",
 Year = 1993,
 Month = "October",
 BOOKTitle = "Second DIMACS Challenge Workshop:
             Cliques, Coloring and Satisfiability",
 ANNOTE = "{Abstract: 
 Recent successes with incomplete satisfiability procedures raise numerous
 issues about their uses and evaluation.  Most such procedures search
 for "yes" answers, and give up if they do not find one.  The need for 
 "no" answers as well is addressed.  It is shown that a recent 
 approximation algorithm of Yannakakis can produce "no" answers only in 
 somewhat trivial cases.  The possibility of salvaging information from
 a "yes" program that is giving up, and using it to find a "no" answer
 is discussed.
 Two incomplete procedures were studied experimentally.
 One (based on "easy" resolutions) produces "no" answers.
 The other (based on Johnson's maximum satisfiability approximation
 algorithm) produces "yes" answers.  Both are deterministic, polynomial time
 algorithms, quadratic with careful implementation.  Combined, they
 solved 83\% of the formulas generated from a circuit-based applications,
 ranging from 400 to over 10000 variables.
 }"
}