Is there an easy condition (for example based on clauses) that implies that a formula in CNF is a tautology? Or is this as hard as for general formulas (not in CNF)?
I first thought of $F$ is a tautology iff every clause of $F$ is a tautology. But this is not true, only the direction from left to right works.
No, you are right.
A Conjunctive Normal Form is a statement which is a conjunction of a series of clauses where each clause is itself a disjunction of a series of literals (permissably including negations).
Such a statement is a tautology if and only if each and every clause is a tautology. A clause is a tautology if and only if either (1) one of the literals is a true valued constant or (2) the clause contains both a literal and its own negation.
Thank you very much.
– user136457 Feb 23 '15 at 16:26