×

Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. (English) Zbl 1081.68032

Summary: Capturing propositional logic, constraint satisfaction problems and systems of polynomial equations, we introduce the notion of systems with finite instantiation by partial assignments, fipa-systems for short, which are independent of special representations of problem instances, but which are based on an axiomatic approach with instantiation (or substitution) by partial assignments as the fundamental notion. Fipa-systems seem to constitute the most general framework allowing for a theory of resolution with nontrivial upper and lower bounds. For every fipa-system we generalise relativised hierarchies originating from generalised Horn formulas, and obtain hierarchies of problem instances with recognition and satisfiability decision in polynomial time and linear space, quasi-automatising relativised and generalised tree resolution and utilising a general “quasi-tight” lower bound for tree resolution. And generalising width-restricted resolution, for every fipa-system a (stronger) family of hierarchies of unsatisfiable instances with polynomial time recognition is introduced, weakly automatising relativised and generalised full resolution and utilising a general lower bound for full resolution.

MSC:

68Q25 Analysis of algorithms and problem complexity
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

SATO
PDFBibTeX XMLCite
Full Text: DOI