
On Finding Solutions for Extended Horn Formulas
John S. Schlipf?y, Fred S. Annexsteinz, John V. Francoy, R. P. Swaminathanyz
Computer Science,
Department of Electrical and Computer Engineering & Computer Science
University of Cincinnati
Cincinnati, OH 45221{0008, USA.
Abstract
In this note we present a simple quadratictime algorithm for solving the satisfiability problem for a special class of boolean formulas. This class properly contains the class of extended Horn formulas [1] and balanced formulas [2, 4]. Previous algorithms for these classes require testing membership in the classes. However, the problem of recognizing balanced formulas is complex, and the problem of recognizing extended Horn formulas is not known to be solvable in polynomial time. Our algorithm requires no such test for membership.
Keywords: Algorithms, satisfiability, extended Horn formulas, balanced matrices, unit resolution
1 Introduction
Chandru and Hooker [1] introduced the class of extended Horn formulas and showed that unit resolution alone can determine whether or not a given extended Horn formula I has a satisfying truth assignment. By repeated variable assignments and unit resolutions one can obtain a satisfying truth assignment for I. The results of [1] cannot, however, be applied unless it is known that I is extended Horn. Unfortunately, the problem of recognizing extended Horn formulas is not known to be solved in polynomial time.
In this paper we extend the observations of Chandru and Hooker to show that extended Horn formulas can be solved in quadratic time without first having to recognize them. Our observation is based on two facts. The first follows from two results in [1]. The second fact follows immediately from the soundness of resolution.
In Section 2 we define a small modification of the conventional DavisPutnam search trees
on Conjunctive Normal Form formulas. Let T denote any such (rooted) tree for an arbitrary
formula I. Each node in T represents a set of clauses closed under unit clause resolution. The
leaves correspond to partial truth assignments for which satisfiability or unsatisfiability has been
determined. All edges of T are directed away from the root.
?Corresponding author
yResearch partially supported by ONR grant N000149410382.
zResearch partially supported by NSF grant CCR9309470.