Average Time for the Full Pure Literal Rule

The simplified pure literal algorithm solves satisfiability problems by choosing variables in a fixed order and then generating subproblems for various values of the chosen variable. If some value satisfies every relation that depends on the chosen variable, then only the subproblem for that preferred value is generated. Otherwise, a subproblem is generated for every value of the variable. The full pure literal algorithm chooses variables that have a preferred value before choosing those that do not. A recurrence equation is found for the average time used by the full pure literal rule algorithm when solving random conjunctive normal form satisfiability problems. The random problems are characterized by the number of variables (v), the number of clauses (t), and the probability that a literal is in a clause (p). An asymptotic lower bound analysis shows that running time is more than polynomial in v when t increases more rapidly than (ln v) 2 (when p is set to maximize the running ..