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 quadratic-time 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 Davis-Putnam 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 N00014-94-1-0382.
zResearch partially supported by NSF grant CCR-93-09470.