Finding the Hardest Formulas for Resolution (Extended Abstract)

1 Introduction

Resolution is a fundamental proof system that can be used to certify the unsatisfiability of a propositional formula in conjunctive normal form (CNF) [Davis and Putnam, 1960]. What makes resolution particularly interesting is that the length of a shortest resolution proof of a given CNF formula (called the resolution complexity of the formula) provides an unconditional lower bound on the running time of modern SAT solvers [Pipatsrisawat and Darwiche, 2009]. 1 Since we know that there are classes of unsatisfiable CNF formulas (such as the formulas based on the Pigeonhole Principle) with exponential resolution complexity [Haken, 1985], we have an exponential lower bound on the running time. It is a natural question to ask: which formulas are the hardest for resolution? i.e., which formulas have the highest resolution complexity? This is an intriguing and surprisingly hard question, which has been approached mainly in an asymptotic way, by propositional proof complexity [Urquhart, 1995].

In this paper, following a recent trend in tackling combinatorial problems using SAT and CSP methods [Heule et al., 2016; Heule, 2018; Codish et al., 2019], we consider the question of resolution complexity in exact, rather than asymptotic terms. We define the resolution hardness numbers (hm)∞m=1 , which, for a given integer m, give the highest resolution complexity of a CNF formula with m clauses. Results from proof complexity, such as Haken's exponential lower bound for the resolution complexity of the pigeonhole formulas [Haken, 1985], translate into statements about the asymptotics of the resolution hardness numbers hm-in particular, hm cannot grow polynomially in m. We aim to look beyond asymptotics and compute hm exactly.

∗The full version appeared in JAIR and at CP 2020 (preliminary).

†Contact Author

1 More precisely, resolution complexity provides a lower bound on the running time of conflict-driven clause learning (CDCL), on which modern SAT solvers are based. Supplemental solving techniques may prevail against the resolution lower bound.

For small values of m, we compute a set of formulas with fewer than m variables and (exactly) m clauses that contain at least one hardest formula for resolution. With these formulas, we can compute the first 10 resolution hardness numbers.

We obtain our results by combining two techniques:

1. A candidate filtering and symmetry breaking search scheme to limit the number of potential candidate formulas with m variables and resolution complexity hm.
2. An efficient SAT encoding for computing the resolution complexity of a given candidate formula.

In our search scheme, we reduce the candidate formulas to a certain class of minimally unsatisfiable (MU) formulas that obey additional structural constraints. We model these formulas by suitable graphs, and generate these graphs modulo isomorphisms by an adaptation of the Nauty graph symmetry package [McKay and Piperno, 2014].

This still leaves us with a large number of formulas whose resolution complexity we must determine algorithmically. For this task, we devise an efficient SAT encoding that produces for a given candidate formula F and an integer s a CNF formula shorts(F), which is satisfiable if and only if F admits a resolution proof no longer than s. We determine the resolution complexity of F by feeding shorts(F) to a SAT solver with increasing values of s. While a SAT encoding for this problem has been proposed before [Menc´ıa and Marques-Silva, 2019], and we do take some inspiration from it, we make crucial adaptations tailored towards minimally unsatisfiable formulas. Furthermore, we introduce a symmetry-breaking scheme that fully breaks all symmetries resulting from permuting the clauses in a proof.

In addition to the resolution hardness numbers themselves, we can draw a detailed map of the hardest formulas with a particular number of variables and clauses. Our results reveal the significance of regular saturated minimally unsatisfiable (RSMU) formulas, which are unsatisfiable formulas that (i) become satisfiable by adding any further literal to any clause, and (ii) where each literal appears in at least two clauses. As a by-product of our computations, we obtain a catalog of RSMU formulas with a small number of variables and clauses, which may be of independent interest in the research on minimal unsatisfiability. For instance, the computed formulas' structure could possibly be used to come up with infinite sequences of hard formulas, inspiring general proof-complexity results.

An alternative but not very interesting object of study would be νn, the highest resolution complexity among formulas with n variables. It is not hard to see by simple induction on the number of variables that every unsatisfiable formula on n variables has a resolution proof of length ≤ 2n+1 - 1 and that indeed νn = 2n+1 - 1, witnessed by the formula which contains all possible clauses of width n.

2 Preliminaries

We assume familiarity with standard notions of graph theory, including those of (un)directed graphs, connectivity, acyclicity, vertex degrees, etc. Any graphs we refer to, directed or not, contain no loops or multiedges.

Formulas

We consider propositional formulas in conjunctive normal form (CNF) represented as sets of clauses. We assume an infinite set var of (propositional) variables. A literal ℓ is a variable x or a negated variable ¬x; we write lit := { x, ¬x | x ∈ var }. For a literal ℓ we put ℓ := ¬x if ℓ = x, and ℓ := x if ℓ = ¬x. For a set of C literals we put C := { ℓ | ℓ ∈ C }. C is tautological if C ∩ C ̸= ∅. A finite non-tautological set of literals is a clause; a finite set of clauses is a (CNF) formula. The empty clause is denoted by □. We write CNF(n,m) for the class of all CNF formulas on n variables and m clauses, and CNF(m) = ⋃∞n=0 CNF(n,m). For a clause C, we put var(C) = { var(ℓ) | ℓ ∈ C }, and for a formula F, var(F) = ⋃C∈F var(C). Similarly, we put lit(F) := var(F) ∪ var(F). An assignment is a mapping τ : var(F) → {0, 1}. A formula F is satisfiable if there is a satisfying assignment, i.e., a mapping τ : var(F) → {0, 1} such that every clause of F contains either a literal x with τ(x) = 1 or a literal ¬x with τ(x) = 0; otherwise it is unsatisfiable. A formula is minimally unsatisfiable (MU) if it is unsatisfiable, but every proper subset is satisfiable.

Resolution

If C1 ∩ C2 = {ℓ} for clauses C1,C2 and a literal ℓ, then the resolution rule allows the derivation of the clause D = (C1 ∪ C2) \ {ℓ, ℓ}; D is the resolvent of the premises C1 and C2, and we say that D is obtained by resolving on ℓ. Let F be a formula and C a clause. A sequence P = L1, . . . , Ls of clauses (proof lines) is a resolution derivation of Ls from F if for each i ∈ {1, . . . , s} at least one of the following holds.

1. Li ∈ F ("Li is an axiom");
2. Li is the resolvent of Lj and Lj ′ for some 1 ≤ j, j ′ < i.

We write |P| := s and call s the length of P. If Ls is the empty clause, then P is a resolution refutation or resolution proof of F. A line Li in a resolution derivation may have different possible "histories;" i.e., Li may be the resolvent of more than one pair of clauses preceding Li, or Li may be both an axiom and obtained from preceding clauses by resolution, etc. In the sequel, however, we assume that an arbitrary but fixed history is associated with each considered resolution derivation. Thus, with a proof P we can associate the directed acyclic graph (DAG) G(P) whose vertices are the proof lines, and which has an arc fromLi to Lj if there is Lk, i, k < j, such that Lj is the resolvent of Li and Lk.

It is well known that resolution is a complete proof system for unsatisfiable formulas; i.e., a formula F is unsatisfiable if and only if there exists a resolution refutation of it. The resolution complexity or resolution hardness h(F) of an unsatisfiable formula F is the length of a shortest resolution refutation of F. For a nonempty set C of formulas, we put h(C) = maxF∈C h(F ).

Isomorphisms of Formulas

Two formulas F and F ′ are isomorphic if there exists a bijection ϕ : lit(F) → lit(F ′ ) such that for each literal ℓ ∈ lit(F) we have ϕ(ℓ) = ϕ(ℓ) and for each C ⊆ lit(F) we have C ∈ F if and only if ϕ(C) ∈ F ′ . For instance the formulas F = {{x, y}, {x, y}, {y}}, and F ′ = {{z,w}, {z,w}, {w}} are isomorphic.

A 2-graph is an undirected graph G = (V,E) together with a partition of its vertex set into two subsets V = V1 ⊎V2. Two 2-graphs G = (V1 ⊎ V2, E) and G′ = (V ′ 1 ⊎V ′ 2 , E′ ) are isomorphic if there exists a bijection ϕ : V1 ⊎ V2 → V ′ 1 ⊎ V ′ 2 such that v ∈ Vi if and only if ϕ(v) ∈ V ′ i , i = 1, 2, and {u, v} ∈ E if and only if {ϕ(u), ϕ(v}} ∈ E′ .

The clause-literal graph of a formula F is the 2-graph G(F) = (V1 ⊎ V2,E) with V1 = lit(F), V2 = F, and E = { {x, x} | x ∈ var(F) } ∪ { {C, ℓ} | C ∈ F, ℓ ∈ C }. We refer to the edges {x, x} as variable edges.

For instance, the formulas F and F ′ mentioned above give rise to the following two isomorphic clause-literal graphs.

3 Theoretical Framework

We define the m-th resolution hardness number as the highest resolution complexity among formulas with m clauses:

We also let H(m) := {F ∈ CNF(m) : h(F) = hm}.

In this section, we describe on a high level our approach to computing hm. Due to space constraints, we refer the reader to the full version for proofs of the results [Peitl and Szeider, 2020; Peitl and Szeider, 2021a].

We begin by establishing the unsurprising basic fact that resolution hardness numbers form an increasing sequence.

Our strategy for computing hm is to find and automatically generate a set χ(m) ⊆ CNF(m) with the following desired properties:

1. χ(m) contains at least one formula with hardness hm;

1. χ(m) is as small and easy to enumerate as possible.

Once we find a suitable χ(m), we simply generate all its formulas and for each compute its hardness; the largest value gives the hardness number hm.

3.1 Finding χ(m)

The central role is played by saturated minimally unsatisfiable (SMU) formulas-minimally unsatisfiable formulas that are rendered satisfiable by adding any literal to any clause. Lemma 2 tells us that χ(m) can be limited to SMU formulas.

Lemma 2. All formulas in H(m) are minimally unsatisfiable; moreover, at least one is saturated.

A simple lower bound for the hardness of minimally unsatisfiable formulas follows from the need to 'connect' all axioms in the proof, reading each clause at least once.

Lemma 3. Let F be a minimally unsatisfiable formula with m clauses. Then h(F ) ≥ 2m - 1.

SMU formulas have two key properties that make them suitable for our purpose: they are the hardest of MU formulas; and they have a well studied structure we can exploit.

In particular, SMU allows us to treat singular and regular formulas separately. A formula is called singular if it contains a singular literal-one that only appears once-and regular otherwise. Singular SMU (SSMU) formulas are well behaved with respect to Davis-Putnam (DP) reduction (variable elimination by exhaustive resolution, [Kullmann and Zhao, 2013, Lemma 12]), which allows us to obtain all SSMU formulas by a simple reverse process, which we term DP-lifting, from smaller SMU formulas. Thanks to that, we can split the generation phase in two, generating only regular formulas first. In the first, expensive phase we get a speedup from pruning via regularity-DP-lifting for SSMU formulas afterwards turns out to be cheap.

Another important notion in the context of minimal unsatisfiability is the deficiency δ(F) of a formula F, defined as δ(F) = |F |-|var(F)|. By a lemma attributed to Tarsi [Aharoni and Linial, 1986], δ(F) is positive if F is MU.

Lemma 4 ([Aharoni and Linial, 1986]). Let F be a minimally unsatisfiable formula. Then log2 |F| ≤ |var(F)| < |F|.

We denote by MU(n,m)(SMU(n,m)) the class of (saturated) minimally unsatisfiable formulas with n variables and m clauses; RSMU(n,m) (SSMU(n,m)) is the subclass of SMU(n,m) consisting of regular (singular) formulas.

The structure of SMU formulas of deficiencies 1 and 2 is well understood [Kleine B¨uning and Kullmann, 2009]. It is known that each deficiency-1 SMU formula with at least one variable has a 1-singular literal (one whose negation is also a singular literal). It is also known that, up to isomorphism, there is a unique deficiency-2 regular MU formula-we pick F 2m, which consists of the clauses

This allows us to obtain resolution hardness of SMU(m1,m) and RSMU(m- 2,m) formulas in closed form.

Propositions 2 and 3, together with Lemma 4, give us a refined lower bound for hm.

In order to determine hm for m ≥ 4, we will need to generate χ(m), which, according to the results above, can be restricted to SMU(n,m) formulas for n ≤ m - 2, ignoring deficiency 1, whose hardness we know. We can further facilitate this step by only generating regular formulas, which we need only for n ≤ m-3 because we know RSMU(m-2, m); we get singular formulas afterwards by DP-lifting.

Naturally, we do not need to include two different isomorphic formulas in χ(m); their hardness properties are identical. Hence, we want to enumerate an isomorph-free subset of χ(m), which we achieve through the correspondence to 2-graphs (Proposition 1) and a tailor-made adaptation of the genbg utility from the graph symmetry package Nauty [McKay and Piperno, 2014] to enumerate such graphs. Nauty allows us to specify constraints on the output graphs, such as connectedness (necessary for MU), triangle-freeness (triangles are tautological clauses), neighbourhood incomparability (no subsumed clauses), or degree bounds (regularity), which can enforce regularity and some necessary conditions for minimal unsatisfiability. However, it is not possible to directly instruct Nauty to generate only SMU formulas, and so we need to generate a superset and filter for saturated minimal unsatisfiability. For that purpose, we proposed a streamlined brute-force SMU testing algorithm, which we omit here due to space constraints.

3.2 Computing Hardness

To compute shortest proofs of formulas, we devise a SAT encoding to answer the following decision problem, which we call SHORT(F, s).

Given a formula F with the clauses (axioms) A1, . . . , Am and var(F) = {x1, . . . , xn}, does there exist a resolution refutation L1, . . . , Ls′ of F of length s′ ≤ s?

It is easy to see that SHORT(F, s) is coNP-hard (s given in binary): since each unsatisfiable formula F with n variables has a resolution refutation of length at most 2n+1 -1, we have UNSAT(F ) = SHORT(F, 2n+1 - 1); using a SAT-based approach is thus justified. On the other hand, membership in NEXPTIME is trivial: guess a refutation of length s and verify that it is correct. The precise complexity of SHORT(F, s) is an open problem.

The basic idea of our encoding, called shorts(F), is to have variables pos[i, v] and neg[i, v] that determine whether v and v occur in Li, and variables arc[i, j], which describe the proof DAG G(P ), together fully determining a candidate resolution proof sequence P . We additionally use auxiliary variables to express certain constraints more succinctly.

We draw inspiration from a similar recently proposed encoding (MSM, [Menc´ıa and Marques-Silva, 2019]), but make improvements focused on MU formulas. One of the strongest points of MSM, enumerating minimal correction subsets (MCSes, i.e., inclusion-minimal sets of clauses whose removal makes the formula satisfiable) in preprocessing, becomes trivial for MU formulas: the MCSes are by definition precisely all singletons. Instead, we require that all axioms are used in the proof.

On the other hand, we extend the encoding with symmetry breaking, inspired by an idea of Schidler and Szeider [2020]. The source of symmetries we aim to break are different topological sorts of a proof DAG G(P). We define a canonical topological sort, and introduce symmetry breaking constraints to ensure that no other topological sort is accepted. The canonical sort is obtained by the topological sorting procedure where in each step the largest available vertex under an arbitrary fixed total order of vertices is picked-in our case a lexicographic ordering of clauses. Another novelty of our encoding is the capacity to reject a partially constructed proof early based on a counting argument involving the number of times each clause is used in resolution steps, similar to Lemma 3. Space constraints prevent us from explaining these ideas in detail here-we refer the reader to the full version. Here we limit ourselves to a summary in Theorem 1.

Theorem 1. Let F be a formula on n variables and m clauses, s an integer. It holds that

1. the size of shorts(F) is polynomial inmax(n,m, s) (s can be exponential in the input length);
2. shorts(F) is satisfiable if and only if F has a resolution refutation P of length s; any model can naturally be interpreted as a canonically topologically sorted resolution refutation of F ;

Theorem 1 gives rise to a simple algorithm. Start with s = 1 and increment while shorts(F) is unsatisfiable. When shorts(F) becomes satisfiable, s equals h(F), and a shortest proof can be extracted from a model of shorts(F). For MU formulas, we can start at s = 2m- 1, as per Lemma 3. We implemented the encoding and this algorithm in Python in the PySAT framework [Ignatiev et al., 2018].

4 Results

Finally, we review our most important results. See the full version [Peitl and Szeider, 2021a] for a much deeper analysis.

Table 1 lists the maximum hardness of an SMU(n, m) formula, and, by taking the maximum in each column (bold), also values of hm. In particular, we obtain the first ten resolution hardness numbers:

It is known that every MU(n,m) formula F has a proof of length at most 2δ(F)-1n + m [Kleine B¨uning and Kullmann, 2009, Section 11.3]; along with the existence of formulas with super-polynomial hardness, this implies that maximum hardness cannot forever be attained by formulas of Table 1: Values of h(SMU(n,m)), and in parentheses the number of hardest formulas in SMU(n, m). For all 3 ≤ n ≤ 9 and n + 2 ≤ m ≤ 10, we found that all hardest SMU(n, m) formulas are regular, except for SMU(7, 10), which contains 5 regular and 19 singular hardest formulas. Formulas are counted modulo isomorphism.

bounded deficiency. We discover m = 10 to be the first point where no formula of deficiency 2 is among the hardest: up to isomorphism, there are exactly three hardest 10-clause SMU formulas, all of deficiency 4, shown as clause-literal graphs in Figure 1. Notice the graphs are drawn vertically symmetrically. Apart from F 2m, these are the only hardest formulas that can be drawn in such a way-symmetrically and with a cycle containing all variable edges drawn as a circle. We calculated these drawings (and non-existence for other graphs) with MiniZinc [Nethercote et al., 2007; Stuckey et al., 2014].

Our encoding [Peitl and Szeider, 2021c] and our catalog of SMU formulas [Peitl and Szeider, 2021b], including the data from our computation, are publicly available.

5 Conclusion

We conducted an extensive computational investigation into resolution hardness, computing the first ten resolution hardness numbers along with a catalog of the corresponding hardest formulas. Our results indicate that regular saturated minimally unsatisfiable formulas achieve the highest hardness. It remains as an interesting theoretical question whether the hardest formulas are always regular.

Acknowledgments

We thank Brendan McKay for adapting Nauty genbg for us. We further acknowledge support by the FWF (projects P32441 and J-4361) and by the WWTF (project ICT19-065).