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：该系统对CNF公式的反驳是一个不可满足的命中公式，且其每个子句均为被反驳CNF公式子句的弱化形式。将该系统与归结及其他证明系统进行比较，等价于研究命中公式的困难度。我们证明树状归结与Hitting系统存在拟多项式分离，并证实Hitting可被树状归结拟多项式模拟，因此命中公式对归结不可能具有指数级困难度，从而部分反驳了Peitl-Szeider猜想。然而Hitting系统在多项式模拟层面表现出惊人的困难性。借助非交换电路多项式恒等式检验（PIT）的思想[Raz-Shpilka,05]，我们证明Hitting可被扩展弗雷格系统模拟。作为副产品，我们展示了一系列静态（半）代数系统可在确定性多项式时间内验证。我们进一步研究Hitting的多种扩展形式：Hitting(+)公式是包含仿射方程（而非仅文字）的子句合取式，且每个赋值至多证伪一个子句。由此衍生的系统与Res(+)证明系统相关联（后者目前尚未发现超多项式下界）：Hitting(+)可模拟树状Res(+)系统，并至少具有拟多项式优势。我们最终给出了Hitting(+)的指数级下界证明。