The intent of this research paper is to broaden the class of propositional formulas for which a linear-time decision procedure can be demonstrated. The authors define a new class of clause sets that has properties similar to sets of Horn clauses and present a linear-time decision procedure. The procedure relies on reducing the satisfiability problem to a relaxation of a corresponding integer-inequality problem. Short but useful reviews of the necessary background from logic and linear equation theory appear in Sections 2 and 3. The definition of “extended Horn clause” is based on a concept called “arborescence,” a special kind of connection graph that is formally defined but not well illustrated or motivated. From such a graph the authors derive a system of integer inequalities based on a concept of “flow.” I did not find this very helpful, however, and did not get much motivation from Figure 2 on page 211 or its discussion on page 210. Several interesting applications are given in Section 9, although the reference to Prolog and knowledge bases seems not quite appropriate because useful knowledge bases and Prolog programs are virtually never propositional. The lines x₂=1 and x₁−2x₂=2 are drawn incorrectly in Figure 1, and the point (1,1) is not the intersection of these two lines.