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 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 lambda1n(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.

Descriptors :   *BOOLEAN ALGEBRA, *SEARCHING, *NONLINEAR PROGRAMMING, INPUT, VARIABLES, COMBINATORIAL ANALYSIS, PROBABILITY

Subject Categories : Operations Research

Distribution Statement : APPROVED FOR PUBLIC RELEASE