A simplified NP-complete satisfiability problem (Q790612)

A well known NP-complete is the satisfiability problem (SAT) for sets of clauses in propositional logic; it is frequently used to show the NP- completeness of other problems by polynomial reduction. Therefore it is of practical interest to refine SAT without losing NP-completeness; one such refinement consists in the restriction to sets of clauses with exactly three literals per clause [\textit{S. A. Cook}, Proc. 3rd Ann. ACM Symp. Theory of Computing, 151-158 (1971; Zbl 0253.68020)]. Let m, n-SAT be the satisfiability-problem with exactly m literals per clause and at most n occurrences per atom. The author shows that 3,4-SAT is still NP- complete; furthermore he proves, that this is the strongest possible refinement, because the instance of 3,3-SAT are always satisfiable (so 3,3-SAT is trivial). Moreover the author presents a simple (deterministic) polynomial-time decision algorithm for the m, 2-SAT problem.