Are Hitting Formulas Hard for Resolution?

TL;DR

This paper investigates the resolution complexity of hitting formulas, a class of propositional formulas with polynomial-time satisfiability, and provides theoretical insights and experimental evidence suggesting they are hard for resolution.

Contribution

The paper establishes that the resolution complexity of hitting formulas is governed by irreducible hitting formulas and presents an algorithm to enumerate and analyze small irreducible hitting formulas.

Findings

Resolution complexity is dominated by irreducible hitting formulas.

Large irreducible hitting formulas are difficult to construct and may be rare.

Experimental results indicate hitting formulas are hard for resolution.

Abstract

Hitting formulas, introduced by Iwama, are an unusual class of propositional CNF formulas. Not only is their satisfiability decidable in polynomial time, but even their models can be counted in closed form. This stands in stark contrast with other polynomial-time decidable classes, which usually have algorithms based on backtracking and resolution and for which model counting remains hard, like 2-SAT and Horn-SAT. However, those resolution-based algorithms usually easily imply an upper bound on resolution complexity, which is missing for hitting formulas. Are hitting formulas hard for resolution? In this paper we take the first steps towards answering this question. We show that the resolution complexity of hitting formulas is dominated by so-called irreducible hitting formulas, first studied by Kullmann and Zhao, that cannot be composed of smaller hitting formulas. However, by definition, large irreducible unsatisfiable hitting formulas are difficult to construct; it is not even known whether infinitely many exist. Building upon our theoretical results, we implement an efficient algorithm on top of the Nauty software package to enumerate all irreducible unsatisfiable hitting formulas with up to 14 clauses. We also determine the exact resolution complexity of the generated hitting formulas with up to 13 clauses by extending a known SAT encoding for our purposes. Our experimental results suggest that hitting formulas are indeed hard for resolution.