We formalize the idea that a set of propositional clauses that is not Horn-renamable can still be partially so. We show that for any finite set of clauses S defined on a set of variables V, there exists a largest subset U of V, with regard to inclusion, such that S is Horn-renamable with respect to U; we call it the Horn basis of S. If the Horn basis is not empty and S contains no unit clause, then deciding whether S is satisfiable reduces to deciding whether a proper subset of S is satisfable. We show that the Horn basis can be computed in linear time. © Elsevier Science Inc., 1998 <1
1. Introduction
Let p be a variable occurring in a propositional formula; we say that we rename p if we replace every occurrence of p by ~ p and every occurrence of -7 p by p. A set of clauses is said to be Horn-renamable if it can be transformed into a Horn set by renaming some variables [12][13][14]. The relevance of this transformation comes from the fact that renaming preserves satisfiability, and that one can decide in lin.ear time whether a Horn set is satisfiable [8,10]. Various linear algorithms for deciding whether a set of clauses is Horn-renamable have been proposed [1,5,11]. In this paper, we formalize the idea that a set of clauses that is not Horn-renamable can still be partially so.
Let V be a set of variables, S a set of clauses defined on V, and U _ V. We say that S is a U-Horn set if every clause of S containing a positive literal on U is a Horn clause and only contains literals defined on U. Note that our definition allows a clause of S to contain negative literals on U together with literals on V\ U, provided that it does not contain any positive literal on U. Obviously, S is a Horn set iff S is a V-Horn set. S is said to be a U-Horn-renamable set if it can be transformed into a U-Horn set by renaming some variables. We show that there