Introducing w-Horn and z-Horn: A generalization of Horn and q-Horn formulae

In this paper we generalize the well-known notions of Horn and q-Horn formulae. A Horn clause, by definition, contains at most one positive literal. A Horn formula contains only Horn clauses. We generalize these notions as follows. A clause is a w-Horn clause if and only if it contains at least one negative literal or it is a unit or it is the empty clause. A formula is a w-Horn formula if it contains only w-Horn clauses after exhaustive unit propagation, i.e., after a Boolean Constraint Propagation (BCP) step. We show that the set of w-Horn formulae properly includes the set of Horn formulae. A function beta(x) is a valuation function if beta (x) + beta(-x) = 1 and beta(x) is an element of {0, 0.5, 1}, where x is a Boolean variable. A formula F is a q-Horn formula if and only if there is a valuation function beta(x) such that for each clause C in F we have that Sigma(x is an element of C) beta(x) <= 1. In this case we call beta(x) a q-feasible valuation for F. In other words, a formula is q-Horn if and only if each clause in it contains at most one "positive" literal (where beta(x) = 1) or at most two half ones (where beta(x) = 0.5). We generalize these notions as follows. A formula F is a z-Horn formula if and only if F '= BCP(F) and either F ' is trivially satisfiable or trivially unsatisfiable or there is a valuation function gamma(x)such that for each clause C in F ' we have that Sigma(x is an element of C boolean AND gamma(x)not equal 0.5)gamma(Gamma x) >= 1 or Sigma(x is an element of C boolean AND gamma(x)not equal 0.5)gamma((x)=0.5) gamma(x) = 1. In this case we call gamma(x) to be a z-feasible valuation for F '. In other words, a formula is z-Horn if and only if each clause in it after a BCP step contains at least one "negative" literal (where gamma(x) = 0) or exactly two half ones (where gamma(x) = 0.5). We show that the set of z-Horn formulae properly includes the set of q-Horn formulae. We also show that the w-Horn SAT problem can be decided in polynomial time. We also show that each satisfiable formula is z-Horn.