Extended Horn Sets in Propositional Logic

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 Chandresekaran that characterizes when an integer solution of a system of inequalities can be found by rounding a real solution in a certain way. A linear-time procedure is provided for identifying “hidden” extended Horn sets 1991 that correspond to a specified arborescence. Finally, a way to interpret extended Horn sets in applications is suggested. © 1991, ACM. All rights reserved.