Search Rearrangement Backtracking often Requires Exponential Time to Verify Unsatisfiability,
Abstract
It is shown that any form of Search Rearrangement Backtracking (SRB) requires exponential time to verify the unsatisfiability of nearly all of a wide class of CNF boolean expressions. This result is based on an input model which generates n independant k-literal clauses from set of r boolean variables. We assume that k is fixed and n and r tend to infinity. The result holds if the limit as n approaches infinity of n/r(n) = lambda, is fixed and lambda>1n(2)/(1-2 to the -K power). SRB requires superpolynomial time nearly always if lambda is replaced by lambda(n) = o(n to the l/ln ln (n) power and the limit as n approaches infinity of lambda (n) = infinity (so the superpolynomial time result holds, for example if lambda (n) = (ln(n)) to the beta power where beta is any positive constant) These results apply to any form of the Davis-Putnam Procedure.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 05, 1987
- Accession Number
- ADA186121
Entities
People
- John Franco
Organizations
- Indiana University Bloomington