condition for a CNF formula to be a tautology 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.