## 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

#### ABSTRACT

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.