Recognition of q-Horn formulae in linear time

The class of q-Horn Boolean expressions, generalizing the important classes of quadratic, Horn, and disguised Horn formulae, has been introduced in Boros et al.(1990). It has been shown there that the satisfiability problem corresponding to a disjunctive normal form φ is solvable in time, linear in the size of φ, if φ is known to be q-Horn. However, the recognition of such formulae was based on the solution of a linear programming problem, and had therefore a much higher (although still polynomial) complexity. In this paper a linear-time combinatorial algorithm is presented for recognizing q-Horn formulae, and reducing in this way the overall complexity of the corresponding satisfiability problem to a linear one.