Proving Unsatisfiability with Hitting Formulas

TL;DR

This work investigates hitting formulas and the Hitting proof system, a static framework that refutes CNFs via unsatisfiable hitting formulas whose clauses are weakenings of input clauses. It establishes a quasi-polynomial separation between tree-like resolution and Hitting, showing Hitting is simulable by Extended Frege (via PIT-based techniques) but not by tl-Res in polynomial size, and it studies stronger variants such as Hitting(⊕) and OddHitting. The authors develop Raz–Shpilka style polynomial identity testing to simulate Hitting in algebraic proof systems (Ext-PC/Extended Frege) and prove exponential lower bounds for Hitting(⊕), as well as upper-lower bound separations with tl-Res, Res, and NS. The work also clarifies the landscape of static semialgebraic proof systems, demonstrates efficient verification for a broad class of proofs, and highlights connections to SAT-solving heuristics through the lens of proof complexity and partition bounds. Overall, it advances understanding of when hitting-based reasoning can be efficiently captured by classical proof systems and outlines rich directions for further separating or unifying these frameworks.

Abstract

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(+).

Figures (2)

• Figure 1: Arrow means that $B$ p-simulates $A$, a dashed arrow means $B$ quasi-polynomially simulates $A$. means a quasi-polynomial separation (a lower bound is for the system $A$). An arrowhead in the tail means that $A$ is exponentially separated from $B$. A dotted line means that we do not know any simulations between $A$ and $B$. Known simulations involving CP and Extended Frege are not shown.
• Figure 2: The graphs $A(0), A(1), B(0)$, and $B(1)$ and their pairwise symmetric differences. Only $A(1) \oplus B(1)$ is not a matching.

Theorems & Definitions (105)

• Definition 2.1: Hitting formula
• Definition 2.2: Unambiguous DNF
• Definition 2.3: Hitting proof system
• Definition 2.4: Hitting Res
• Proposition 2.5
• proof
• Definition 2.6: Odd hitting formula
• Definition 2.7: Odd Hitting proof system
• Definition 2.8: Hitting-$k$ formula
• Definition 2.9: Hitting$[k]$