[Proof Complexity] a new preprint: Hitting formulas

[Edward A. Hirsch]

Dear Colleagues,

A new preprint is available:
   http://arxiv.org/abs/2302.06241
The details are below, and your comments are very welcome.

Best regards,
Edward

Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, Marc Vinyals

*Proving Unsatisfiability with Hitting Formulas*
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 the 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(+).