Hitting formulas have been studied in many different contexts at least since [Iwama,89]. A hitting formula is a set of Boolean clauses such that any two of them cannot be simultaneously falsified. [Peitl,Szeider,05] conjectured that hitting formulas should contain the hardest formulas for resolution. They supported their conjecture with experimental findings. Using the fact that hitting formulas are easy to check for satisfiability we use them to build a static proof system Hitting: a refutation of a CNF in Hitting is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. We show that tree-like resolution and Hitting are quasi-polynomially separated. We prove that Hitting is quasi-polynomially simulated by tree-like resolution, thus hitting formulas cannot be exponentially hard for resolution, so Peitl-Szeider's conjecture is partially refuted. Nevertheless Hitting is surprisingly difficult to polynomially simulate. Using the ideas of PIT for noncommutative circuits [Raz-Shpilka,05] we show that Hitting is simulated by Extended Frege. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in a deterministic polynomial time. We consider multiple extensions of Hitting. Hitting(+) formulas are conjunctions of clauses containing affine equations instead of just literals, and every assignment falsifies at most one clause. The resulting system is related to Res(+) proof system for which no superpolynomial lower bounds are known: Hitting(+) simulates the tree-like version of Res(+) and is at least quasi-polynomially stronger. We show an exponential lower bound for Hitting(+).

翻译：自[Iwama, 89]以来，命中公式已在多种不同背景下得到研究。命中公式是一组布尔子句，其中任意两个子句不能同时被证伪。[Peitl, Szeider, 05]猜想，命中公式应包含对归结而言最难的公式，并通过实验发现支持该猜想。利用命中公式易于检验可满足性的特点，我们构建了一个静态证明系统Hitting：在Hitting系统中，对一个CNF的驳斥是一个不可满足的命中公式，其每个子句均为被驳斥CNF中某个子句的弱化。将该系统与归结及其他证明系统进行比较，等价于研究命中公式的难度。我们证明树状归结与Hitting之间呈拟多项式分离。我们证明了Hitting可被树状归结拟多项式模拟，因此命中公式不能对归结产生指数级难度，从而部分反驳了Peitl-Szeider猜想。然而，Hitting的多项式模拟异常困难。借助非交换电路的PIT思想[Raz-Shpilka, 05]，我们证明Hitting可由扩展弗雷格系统模拟。作为副产品，我们表明多个静态（半）代数系统可在确定性多项式时间内验证。我们考虑了Hitting的多种扩展。Hitting(+)公式是子句的合取，这些子句包含仿射方程而非仅文字，且每个赋值最多证伪一个子句。由此产生的系统与Res(+)证明系统相关——后者尚无已知超多项式下界：Hitting(+)模拟了树状版本的Res(+)，并且至少具有拟多项式强度的优势。我们给出了Hitting(+)的指数级下界。