
Accession Number : ADA186121
Title : Search Rearrangement Backtracking often Requires Exponential Time to Verify Unsatisfiability,
Corporate Author : INDIANA UNIV AT BLOOMINGTON DEPT OF COMPUTER SCIENCE
Personal Author(s) : Franco, John
PDF Url : ADA186121
Report Date : 05 Jul 1987
Pagination or Media Count : 29
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 kliteral 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 lambda1n(2)/(12 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 DavisPutnam Procedure.
Descriptors : *BOOLEAN ALGEBRA, *SEARCHING, *NONLINEAR PROGRAMMING, INPUT, VARIABLES, COMBINATORIAL ANALYSIS, PROBABILITY
Subject Categories : Operations Research
Distribution Statement : APPROVED FOR PUBLIC RELEASE