Scientific Annals of Computer Science

"Alexandru Ioan Cuza" University of Iaşi

On the Complexity of Propositional Calculus Formulae.

Published in Volume X, 2001, p. 27-44, doi:

Authors: Stefan ANDREI, Gheorghe GRIGORAS, Manfred KUDLEK, Cristian MASALAGIU


In this paper we present some estimations for the number of resolvents and the number of steps of the classical Resolution Algorithm applied to a propositional formula $F$ over $n$ variables. This topic may be useful for generating PROLOG-like interpreters. The notations and definitions necessary in this paper are presented in the {sl first section}. Our variant of Resolution Algorithm (Algorithm 1) is essential for the results obtained in the next sections. The {sl second section} is dedicated to the computation of the maximal number of resolvents. The situations when this number is reached are also treated. The main result is Theorem ref{t.1.2.}. The {sl third} and {sl fourth} sections refer to Krom and Horn clauses, which represent two classes of clauses forming a {sl stable} part w.r.t. resolution. For each of these two classes we also compute the maximal number of resolvents which may be reached and study the {sl limit} cases. For the class of Krom clauses we obtain a polynomial algorithm (Proposition ref{p.2.3.}) for testing the (un)satisfiability of $F$ together with the computation of Res^(F). The computation of Res^(F) for a Horn formula leads to an exponential algorithm (Theorem ref{t.2.4.}).

We also indicate how some of our results may be improved.


© 2006-2019 FII | Contact: annals at