@Article{VanGelder88,
 Author="Van Gelder, Allen",
 Title="{A Satisfiability Tester for Non-Clausal Propositional Calculus}",
 Journal="Information and Computation",
 VOLUME=79,
 NUMBER=1,
 YEAR=1988,
 MONTH=oct,
 PAGES="1--21",
 ANNOTE="{
 An algorithm for satisfiability testing in the propositional calculus
 with a worst case running time that grows at a rate less than
 $2^{(0.25+\epsilon)L}$ is described, where $L$ is the length of the 
 input expression.  This represents a new upper bound on the complexity
 of non-clausal satisfiability testing.  The performance is achieved by 
 using lemmas concerning assignment and pruning that preserve
 satisfiability, together with choosing a "good" variable upon which
 to recur. For expressions in CNF, it is shown that an upper 
 bound is $2^{0.128L}$.
 }"
}