Chapter 12, Section 12.2.1, k-CNF definition

[ann-hup]

In the 2SAT section, the first sentence has a small typo in defining a k-CNF formula - it's just missing the word "if". I think the definition could also explicitly define what a "literal" is.

Current sentence: We say that a formula is a k-CNF it is an AND of ORs where each OR involves exactly k literals: Proposed sentence: We say that a formula is a k-CNF if it is an AND of ORS, where each OR has exactly k literals (variables or their negations)