Abstract
A set of clauses constitutes a hitting formula if every truth assignment falsifies exactly one clause. This is a condition which can be checked efficiently. If every clause is a weakening of a clause in some CNF, then the CNF is unsatisfiable. This is the Hitting proof system.