Extended Horn Sets in Propositional Logic
V. CHANDRU
PzLrdl~eGtziverslt~, West Lafuyettej Indiana
AND
J. N. HOOKER
Camegle Mellon Lrnlversltj,, PrltsblirtqJl, Penrrsylvanla
Abstract. The class of Horn clause sets in propositional logic is extended to a larger class for which the
satisfiability problem can still be solved by unit resolution in linear time. It is shown that to every
arborescence there corresponds a family of extended Horn sets, where ordinary Horn sets correspond
to stars with a root at the center. These results derive from a theorem of Chandrasekaran that
characterizes when an integer solution of a system of inequalities can be found by rounding a real
solution ma certain way, A linear-time procedure isprovided foridentifying’’hidden’’ extended Horn
sets (extended Horn but for complementation of variables) that correspond to a specified arborescence.
Finally, a way to interpret extended Horn sets in applications N suggested.
Categories and SubJect Descrlptors:F.4.l [Mathematical Logic and Formal Languages] : Mathematical
Logic—comp~~tatzo}tal logic, mechanical theorem prowng: G, 1.6 [Numerical Analysis]: Optimization—
~}ttegerpro.gra~n~~l~;z$; H.2. I [Database Management]: Logical design: 1.2.3 [Artificial Intelligence]:
Deduction and Theorem Proving—deduction, resolution
General Terms: Algorithms. Theory
Additional Key Words and Phrases: Horn clauses, propositional logic
1. Introdllctlon
Horn clauses are widely used in logical programming languages and knowledge-
based systems because inference is easy for them but generally quite hard for larger
classes of formulas. Unit resolution solves the inference (or satisfiability) problem
for Horn clauses in propositional logic in time that is linear in the number of
literals [12, 18], whereas the general satisfiability problem for propositional logic is
NP-complete [9].
The research of V. Chandru was supported in part by OffIce of Naval Research grant NOOO14-86-K-
0689 and by National Science Foundation grant DMC 88-07550.
The research of J. H. Hooker was supported in part by U.S. Air Force Oftice of Scientific Research
grant AFOSR-87-0292.
Authors’ addresses: V. Chandru, School of Industrial Engineering. Purdue Umverslty, West Lafayette,
IN 47907: J. N. Hooker. Graduate School of Industrial Administration, Carnegie Mellon University,
Pittsburgh, PA 15213,
Permission to copy without fee all or part of this material is granted provided that the copies are not
made or distributed for direct commercial advantage. the ACM copyright notice and the title of the
publication and its date appear. and notice is given that copying is by permission of the Association for
Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.
O 1991 ACM 0004-541 1/91/0100-0205 $01.50
Journal of the AssocMlon for Computmg Machlnwy, Vol 38.No 1,Janua~1Y91,pp 205-2!1

206 ~. CHANDRU AND J. N. HOOKER
It would obviously be desirable to extend Horn clauses to a larger class of
propositions for which the inference problem remains easy. Yamasaki and Doshita
[21 ] identified one such class, for which the inference problem can be solved in
cubic time; Arvind and Biswas [3] later found a quadratic time algorithm for the
class. Whereas Horn clauses have at most one positive literal, Yamasaki and
Doshita [21] consider sets of clauses that may have more than one positive literal,
provided the positive literals are “nested” in a certain way. Gallo and Scutella [13]
generalized the nested positives idea to obtain a recursively-defined hierarchy of
problems r(,, r, ,. ... where r. is the class of Horn problems, and rl the class
defined by Yamasaki and Doshita. The problems in 17~are soluble in O (Ln ~) time,
where L is the number of literals and n the number of atomic propositions. It is
unclear, however, how these classes of propositions might be more useful in practice
than ordinary Horn clauses.
We show below that there is another generalization of Horn clauses for which
inference is not only as easy as for Horn clauses but can be accomplished in the
same way—by a linear-time unit resolution algorithm. We call sets of such clauses
“extended Horn. ” A set of clauses is extended Horn if its atomic propositions
correspond to the arcs of some rooted arborescence (i.e., rooted directed tree in
which all arcs are directed away from the root) in such a way that each clause in
the set describes an “extended star-chain” flow pattern on the arborescence. That
is, if a positive (negative) literal indicates a forward (backward) unit flow on the
corresponding arc. then the resulting flow pattern consists of chains each of which
carries a unidirectional unit flow into the root, plus at most one such chain that is
unconnected to the root. Ordinary Horn sets correspond to arborescences that are
stars (i.e., all arcs incident to a central root), so that extended Horn sets represent
a substantial generalization of ordinary Horn sets. We also show that the inference
problem for “hidden” extended Horn sets, which are sets that become extended
Horn when one or more atomic propositions are replaced by their negations, can
likewise be solved by unit resolution, thus further enlarging the class of easy
inference problems. Finally, we characterize extended Horn sets of rules and suggest
one way that they might be interpreted and used in applications for which ordinary
Horn sets are inadequate.
We were led to a discovery of extended Horn sets by a theorem of Chandrase-
karan [6]. The theorem characterizes sets of linear inequalities for which a O-1
solution can always be found (if one exists) by rounding a real solution. which can
in turn be found by linear programming. We show that a set of inequalities with
coefficients in {O. 1, – I \ that corresponds to an arboresence (or any rooted, directed
tree) in the way noted above satisfies the conditions of Chandrasekaran’s theorem.
In this way, we give a network characterization of a family of 0-1 problems that
can be solved by linear programming and rounding. Extended Horn sets (explicit
or hidden) are those that, when expressed as a system of linear inequalities, belong
to this family of O– 1 problems. It follows that linear programming solves the
satisfiability problem for (explicit or hidden) extended Horn sets.
We also expose a remarkable parallel between unit resolution and the rounding
process dictated by Chandrasekaran’s theorem. This parallel sheds light on why
unit resolution solves extended Horn satisfiability problems.
Thus, the ease of solving Horn and extended Horn inference problems is directly
related to the fact that they pose O– 1 problems that can be solved by linear
programming and rounding. This adds to the collection of interesting mathematical
properties of Horn clauses that have recently been demonstrated by Blair et al [5],
Jeroslow and Wang [17], and Hooker [16]. See [8] and [15] for surveys.