A note on disjunctive form tautologies

Cook [1] and Karp [2] have shown that a large class of combinatorial decision problems can be solved in time bounded by a polynomial in the size of the problem iff there is a polynomial time procedure for deciding whether a disjunctive formula with at most three literals per disjunct in the propositional calculus is a tautology.