![Meta-complexity_logo_hi-res](/sites/default/files/styles/workshop_banner_sm_1x/public/2023-02/Meta-complexity_hi-res.png.jpg?itok=oFqprXq1)
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.