PaperlayerView exact revision on arXiv

Source-linked AI summary

Short Resolution Refutations for CNFs with Bounded Weighted Incidence Treewidth

Shaowei Cai, Ziqun Li

arXiv:2610.02047v1cs.CC

TL;DR

Whether every unsatisfiable CNF has an FPT-sized resolution refutation parameterized by incidence treewidth remains open. The paper develops refutation constructions using log-weighted incidence decompositions and establishes several length and width bounds. It also gives FPT-sized refutations for formulas with extension variables representing every nonempty subclause.

  • Problem

    It remains open whether every unsatisfiable CNF formula has an FPT-sized resolution refutation parameterized by incidence treewidth.

    Source: §1 · p. 3

  • Method

    The paper uses a log-weighted incidence tree decomposition in its construction of resolution refutations.

    Source: §2.4 · p. 8

  • Results

    Every unsatisfiable CNF has a resolution refutation of length k(n + m)2^O(tw*_log(F)) and width at most tw*_log(F) + k, and a regular resolution refutation of length (n + m)2^O(tw*_log(F)).

    Source: §1.2 · pp. 4–5

  • Takeaways & Limitations

    Introducing variables for every nonempty subclause gives FPT-sized resolution refutations parameterized by incidence treewidth.

    Source: §2.7 · p. 11

    The results do not resolve whether every unsatisfiable CNF has an FPT-sized resolution refutation parameterized by incidence treewidth.

    Source: §8 · p. 42

Abstract

from arXiv · show

It is an open problem in proof complexity whether every unsatisfiable CNF formula has an FPT-sized resolution refutation parameterized by incidence treewidth. In this paper, we establish several upper bounds on resolution refutation length related to this problem. Consider an unsatisfiable CNF formula $F$ with $n$ variables, $m$ clauses, maximum clause width $k$, and incidence treewidth $\mathrm{tw}^*(F)$. In this paper, we introduce two variants of incidence treewidth. Their definitions can be stated informally as follows. The first is log-weighted incidence treewidth $\mathrm{tw}_{\log}^*(F)$, which is the treewidth of the weighted incidence graph, in which variables have weight one and each clause has weight equal to the logarithm of its width. The second is partially log-weighted incidence treewidth $\mathrm{tw}^*_{\mathrm{plog}}(F)$, which is a refinement of log-weighted incidence treewidth. In this variant, for a nice tree decomposition of the incidence graph, each clause has weight one along a path selected for that clause and elsewhere has weight equal to the logarithm of one plus the number of its literals whose variables do not appear in any bag on that path, and variables have weight one. For every unsatisfiable CNF formula $F$, we prove the existence of (i) an FPT-sized resolution refutation parameterized by log-weighted incidence treewidth, with width at most $\mathrm{tw}_{\log}^*(F)+k$; (ii) a resolution refutation of length $(n+m)k^{O(\mathrm{tw}^*(F))}$ and width at most $\mathrm{tw}^*(F)+k$; (iii) an FPT-sized resolution refutation parameterized by partially log-weighted incidence treewidth; and (iv) an FPT-sized regular resolution refutation parameterized by log-weighted incidence treewidth. Our main idea is to construct FPT-sized $k$-DNF resolution refutations parameterized by incidence treewidth, and then convert them into resolution refutations.

1 Introduction

The paper addresses whether incidence-treewidth structure can yield FPT-sized resolution refutations for every unsatisfiable CNF, and establishes partial progress through new bounds and weighted variants. Its results improve prior upper bounds while leaving the general question open.

1 Introduction

  • The open question is whether every unsatisfiable CNF has an FPT-sized resolution refutation parameterized by incidence treewidth.The paper frames this as how to use the structure of an incidence tree decomposition to construct short refutations.Source: §1 · p. 3

1.1 Related Work

  • Prior results give FPT-sized resolution refutations from primal treewidth, but primal treewidth can be arbitrarily large even when incidence treewidth is bounded.For bounded clause width, earlier work also gives FPT-sized refutations parameterized by incidence treewidth; other approaches transform the formula and may introduce additional variables.Source: §1.1 · p. 3

1.2 Main Results

  • The paper introduces log-weighted incidence treewidth, assigning variables weight one and clauses weight max{log |C|, 1}, and partially log-weighted incidence treewidth, a refinement based on selected paths.Partially log-weighted incidence treewidth is no greater than log-weighted incidence treewidth or one-sided incidence treewidth.Source: §1.2 · p. 4
  • Theorem 1 gives resolution length k(n + m)2^O(tw*_log(F)) and width at most tw*_log(F) + k, plus length (n + m)k^O(tw*(F)) and width at most tw*(F) + k.It also gives a k-DNF-Res refutation of length (n + m)2^O(tw*(F)) and a resolution refutation of length k^2(n + m)2^O(tw*_plog(F)); the latter two resolution bounds using weighted parameters are FPT bounds.Source: §1.2 · p. 4
  • Theorem 2 gives a regular resolution refutation of length (n + m)2^O(tw*_log(F)), or (n + m)k^O(tw*(F)) when k ≥ 2.The paper also notes that its bounds help rule out certain formula families as candidates for incidence-treewidth resolution-length lower bounds.Source: §1.2 · p. 5

1.3 Comparison with previous results

  • The incidence-treewidth upper bound improves n^O(1)2^O(tw*(F)k) to n2^O(tw*(F) log k).The paper also describes a construction using extension variables that directly uses an incidence tree decomposition of the original formula to obtain FPT-sized refutations.Source: §1.3 · p. 5

2 Main Ideas and Proof Overview

The overview motivates an incidence-treewidth approach: simulate SAT dynamic programming with k-DNF-Res, then convert the derivation into resolution, refining expansions to control their size.

2.1 Motivation for Our Construction

  • The construction is motivated by using extension variables for subclauses to simulate SAT dynamic programming, alongside the correspondence between k-DNF-Res and resolution with extension variables.The authors associate clauses with each DNF and derive them in the order of the original refutation; refinements to the construction and expansion yield the partially log-weighted bound.Source: §2.1 · p. 6

2.2 Multiset proof systems

  • The mRes and k-mDNF-Res systems retain repeated literals or terms as multisets, with contraction available to adjust multiplicities and proofs convertible to their original systems.mRes also supports the regularity argument by allowing certain resolution steps to become weakening steps during conversion.Source: §2.2 · pp. 6–7

2.3 Inconsistent States

  • The proof simulates dynamic programming by representing inconsistent states at decomposition nodes as mDNFs and deriving them from leaves toward the root.A state records a node, an assignment to its bag variables, and a set of bag clauses; inconsistency means no subtree assignment extending that assignment satisfies the required clauses.Source: §2.3 · p. 7

2.4 Log-weighted incidence treewidth and the construction

  • Log-weighted incidence treewidth controls expansion size, while ordinary incidence treewidth bounds expansion-clause width and yields resolution length and width bounds.The construction derives a k-mDNF-Res refutation from inconsistent states and converts it to resolution using expansions.Source: §2.4 · pp. 8–9

2.5 Partially log-weighted incidence treewidth and the refined construction

  • Partially log-weighted incidence treewidth reduces expansion size by weighting clauses one along selected paths and by the logarithm of one plus the number of literals outside those paths elsewhere.The modified construction yields a resolution refutation, but its expansion multiclauses may have large width, so it provides no comparable width bound.Source: §2.5 · pp. 9–10

2.6 Constructing regular resolution refutations

  • The regular-resolution construction derives multiclauses directly in mRes and maintains pathwise conditions that ensure conversion to a regular resolution refutation.In particular, each variable is resolved at most once by a variable-eliminating resolution on a directed path.Source: §2.6 · pp. 10–11

2.7 Further discussion

  • Subpolynomial maximum clause width yields FPT-sized resolution refutations parameterized by incidence treewidth under a suitable computability condition; extension variables also give such refutations when representing every nonempty subclause.The discussion also considers limitations of the classic length–width relation and implications of the upper bounds for candidate formula families.Source: §2.7 · p. 11

3 Preliminaries

The preliminaries define the proof systems and graph-decomposition terminology used to state the paper’s results. They also specify how refutations and FPT-sized proof bounds are measured.

3.1 Resolution-based proof systems

  • Assignments may be partial, and a clause is satisfied when an assigned variable makes at least one of its literals true.The preliminaries also define clauses, terms, width, and the assumption that formulas contain neither empty nor tautological clauses.Source: §3.1 · pp. 11–12
  • A resolution refutation derives ⊥ using initial clauses, weakening, and resolution; its length counts clauses, its width is the maximum clause width, and regularity forbids resolving a variable twice along a proof-DAG path.The proof DAG links each derived clause to the clauses used to derive it.Source: §3.1 · p. 12

(∧-introduction),

  • A k-DNF-Res derivation starts from clauses or the axiom x ∨ ¬x and applies its inference rules to derive DNF formulas; a refutation ends with ⊥.A k-DNF is a disjunction of terms, each containing at most k literals.Source: §3.1 · p. 12, (∧-introduction) · p. 13

3.2 Graph representations and tree decompositions

  • The incidence graph connects variables to clauses containing them, while the primal graph connects variables that occur together in a clause; treewidth is the minimum decomposition width.Incidence treewidth is the treewidth of the incidence graph.Source: §3.2 · p. 13
  • A nice tree decomposition has an empty root and leaves, at most two children per node, and join, introduce, or forget node types for variables and clauses.A tree decomposition covers every vertex and edge, with the bags containing each vertex forming a connected subtree.Source: §3.2 · p. 13
  • FPT-sized refutations have length at most g(tw*(F))(n + m)^c for a computable g and constant c.The definition applies analogously to other proof systems.Source: §3.2 · p. 14

4 Preparations for the constructions

This section develops the preliminaries for later constructions by defining weighted incidence-treewidth variants and technical proof systems and states, and by establishing supporting structural bounds and conversion results. It also characterizes inconsistent states locally at nodes of a nice tree decomposition, including the leaf case and introduce and forget transitions.

4.1 Weighted incidence treewidth

  • Log-weighted incidence treewidth assigns unit weight to variables and max{log |C|, 1} to each clause, while partially log-weighted treewidth refines clause weights using clause paths.For an alternative parameter defined over arbitrary rooted decompositions, the paper gives an FPT resolution-length bound k^2(n + m)2^O(w^2), but does not establish a linear relation to partially log-weighted treewidth.Source: §4.1 · pp. 14–15
  • Optimal log-weighted and partially log-weighted widths admit nice decompositions of polynomially bounded size, and partially log-weighted width is at most one-sided incidence treewidth.The log-weighted decomposition has O((n + m)(tw*_log(F) + 1)) nodes; the one-sided conversion yields partially log-weighted width at most tw_os(F).Source: §4.1 · p. 16

4.2 Multiset proof systems

  • Multiset resolution and k-mDNF resolution simplify construction details, while their refutations transfer to ordinary systems with controlled size and width.An mRes refutation yields a resolution refutation of no greater length or width, and preserves regularity if each variable is resolved at most once per proof-DAG path; k-mDNF-Res length increases by at most a factor of three.Source: §4.2 · pp. 17, 19

4.3 Inconsistent states

  • The inconsistent-state framework associates each decomposition node, bag assignment, and selected bag clauses with extensions satisfying the relevant clauses, and calls the state inconsistent when none exist.The section introduces decomposition lemmas for join, introduce-variable, and introduce-clause nodes as groundwork for computing inconsistent states from leaves to root.Source: §4.3 · pp. 19–20
  • At a leaf with an empty bag, the sole state is consistent, so the leaf has no inconsistent state.The state is (t, ∅, ∅).Source: §4.3 · p. 20
  • At a join node, the criterion considers every pair of child clause subsets whose union is A.The supplied passage begins the iff characterization but is truncated before its full condition.Source: §4.3 · p. 20
  • At an introduce-variable node, a state is inconsistent exactly when its corresponding child state is inconsistent under the restricted assignment.The child state uses α restricted to χv(t′) and the set Ax.Source: §4.3 · p. 20
  • At an introduce-clause node, inconsistency follows from the clause’s membership in A and whether the assignment satisfies it, or from the corresponding child state.The stated cases distinguish c ∉ A, c ∈ A with α satisfying c, and c ∈ A with α not satisfying c.Source: §4.3 · p. 20
  • At a forget-variable node, a state is inconsistent exactly when both child states, extending the assignment with x = 0 and x = 1, are inconsistent.The two extensions are α0 and α1.Source: §4.3 · p. 20
  • At a forget-clause node, inconsistency is equivalent to inconsistency of the child state with the forgotten clause added to A.The child set is A ∪ {c}.Source: §4.3 · p. 20

5 General resolution upper bounds

This section develops local k-mDNF derivations over tree decompositions and uses them to construct resolution refutations, including conversion to resolution and a construction guided by clause paths. It establishes upper bounds parameterized by ordinary, log-weighted, and partially log-weighted incidence treewidth.

5.1 Local derivations

  • For an inconsistent state with B empty, its mDNF has |χv(t)| + |A| terms, at most w + 1.The size bound follows from |χ(t)| ≤ w + 1.Source: §5.1 · p. 21
  • If (t0, α, A) is inconsistent, D(t0, α, A, B0) has a k-mDNF-Res derivation from the corresponding inconsistent child formulas, of total length O(2^a) = O(2^w), where a ≤ |χc(t0)| ≤ w + 1.Source: §5.1 · pp. 21, 23
  • At an introduce-variable node, an inconsistent state has a k-mDNF-Res derivation of length O(w), with mDNFs of size at most w + 1 when B is empty.Source: §5.1 · pp. 23–24
  • At an introduce-clause node, an inconsistent state has a k-mDNF-Res derivation of length O(w), with intermediate mDNFs of size at most w + 1 when B is empty.Source: §5.1 · pp. 24–25
  • Local forget-variable and forget-clause transitions derive k-mDNFs in at most one step, with size at most w + 1 when B is empty, except for the initial clause.These are local derivation steps used by the refutation constructions.Source: §5.1 · pp. 25–26

5.2 From local derivations to refutations

  • A nice tree decomposition of width w yields a k-mDNF-Res refutation of length |V(T)|2^O(w), with noninitial mDNFs of size at most w + 1.The construction processes the decomposition bottom-up from inconsistent states.Source: §5.2 · p. 27
  • A decomposition of width w and log-weighted width wlog yields a resolution refutation of length k|V(T)|2^O(wlog) and width at most w + k.The proof converts the k-mDNF refutation by expanding its formulas into multiclause derivations.Source: §5.2 · p. 29
  • Given a clause-path family, a width-w decomposition yields a k-mDNF-Res refutation of length |V(T)|2^O(w).The construction derives the empty formula at the root from the inconsistent root state.Source: §5.2 · pp. 29–30
  • For a nice decomposition and clause-path family of partially log-weighted width wplog, resolution refutation length is k|V(T)|2^O(wplog); using a one-sided decomposition makes the refutation regular.Theorem 33 gives the length bound, and the regularity condition is stated for the construction from a one-sided tree decomposition.Source: §5.2 · pp. 31, 33
  • Log-weighted incidence treewidth yields a resolution refutation of length k(n + m)2^O(tw*_log(F)) and width at most tw*_log(F) + k.The bound follows by using a log-weighted tree decomposition.Source: §5.2 · p. 34
  • Ordinary incidence treewidth yields a resolution refutation of length (n + m)k^O(tw*(F)) and width at most tw*(F) + k.This bound uses the decomposition chosen for the k-DNF-Res refutation.Source: §5.2 · p. 34
  • Partially log-weighted incidence treewidth yields a resolution refutation of length k^2(n + m)2^O(tw*_plog(F)).The proof selects a decomposition and clause-path family of partially log-weighted width tw*_plog(F) + 1.Source: §5.2 · p. 34
  • Ordinary incidence treewidth also yields a k-DNF-Res refutation of length (n + m)2^O(tw*(F)).A k-mDNF-Res refutation converts to k-DNF-Res with the same asymptotic length.Source: §5.2 · p. 34

6 Regular resolution upper bounds

This section establishes regular resolution upper bounds parameterized by log-weighted incidence treewidth, constructing a path-restricted mRes refutation and converting it into a regular resolution refutation. For formulas with maximum clause width k ≥ 2, it also gives a refutation length bound in terms of n, m, k, and incidence treewidth.

6 Regular resolution upper bounds

  • A log-weighted-width wlog nice tree decomposition yields an mRes refutation of length |V(T)|2^O(wlog), with each variable used in at most one variable-eliminating resolution per proof-DAG path.This path restriction enables conversion of the mRes refutation into a regular resolution refutation.Source: §6 · p. 35
  • Every unsatisfiable CNF with n variables and m clauses has a regular resolution refutation of length (n + m)2^O(tw^*_{log}(F)); for maximum clause width k ≥ 2, the length is (n + m)k^O(tw^*(F)).The bound follows by combining a nice tree decomposition of log-weighted width with the mRes construction and its conversion to regular resolution.Source: §6 · p. 39
  • (n + m)k^{O(tw^*(F))} bounds the length of a regular resolution refutation when F has maximum clause width k ≥ 2.The bound follows from Lemma 5.Source: §6 · p. 40

7 Further discussion

The discussion derives further consequences of the paper’s upper bounds: subpolynomial clause width yields FPT-sized refutations under a computability condition, while the bounds constrain routes to stronger lower bounds and permit restricted extension variables.

7.1 FPT-sized resolution refutations under restrictions on clause width

  • For maximum clause width k ≤ f(n) with f(n) = n^o(1), refutations have length at most g(tw*(F))(n + m)^2, and a stated computability condition makes the bound FPT-sized.The condition requires a computable N such that f(n) ≤ n^(1/q) for all q ≥ 1 and n ≥ N(q).Source: §7.1 · p. 40

7.2 Implications for lower bounds

  • The width bound tw*(F) + k limits direct length–width lower bounds to at most 2^O(tw*(F)), so stronger bounds require more than that relation alone.Candidate families with log-weighted or partially log-weighted incidence treewidth bounded by O(tw*(F) + log n) can also be ruled out for certain stronger lower bounds.Source: §7.2 · p. 41

7.3 FPT-length refutations with restricted extension variables

  • The restricted-extension construction uses the original formula’s incidence tree decomposition directly, without first transforming the formula to one of small primal treewidth.This contrasts with the approach discussed for [23, 15].Source: §7.3 · p. 41
  • For every unsatisfiable F, adding variables representing its nonempty clause subclauses yields a resolution refutation of length k(n + m)2^O(tw*(F)).Each added variable y_C represents the subclause C, and the resulting formula is equisatisfiable with F.Source: §7.3 · p. 41

8 Conclusion and future directions

Whether every unsatisfiable CNF has an FPT-sized resolution refutation parameterized by incidence treewidth remains open. The paper improves upper bounds and identifies further questions, but resolving the problem may require new techniques or more complex formulas.

8 Conclusion and future directions

  • The weighted-incidence-treewidth bounds improve previous upper bounds but do not settle whether all unsatisfiable CNFs have FPT-sized resolution refutations parameterized by incidence treewidth.Extending the results to all such formulas appears to require new techniques.Source: §8 · p. 42
  • A negative answer may require formulas with more complex structure, since the constructions exclude some simple formula families as lower-bound candidates.Source: §8 · p. 42
  • The authors raise adapting a technique for long clauses, studying regular refutations under partially log-weighted incidence treewidth, and efficiently computing or approximating that parameter as future questions.The regular-refutation result established in the paper is for log-weighted incidence treewidth.Source: §8 · p. 42

A Proofs of Lemmas 7 and 8

The appendix bounds the size of nice tree decompositions for both weighted incidence-treewidth variants. It obtains the log-weighted bound by simplifying and refining a decomposition, and the partially log-weighted bound by selecting clause paths and key nodes.

A Proofs of Lemmas 7 and 8

  • A log-weighted-width-optimal nice decomposition with empty root and leaves can be constructed with O((n + m)(tw*_log(F) + 1)) nodes.The proof first uses a decomposition with at most n + m nodes, then converts it to a nice decomposition while controlling bag weights and path lengths.Source: A Proofs of Lemmas 7 and 8 · pp. 43–44
  • For a nice decomposition of partially log-weighted width w, another nice decomposition exists with O(k(n + m)w) nodes.The construction selects paths for clauses and marks the root, nodes covering vertices and edges, and endpoints of nonempty clause paths.Source: A Proofs of Lemmas 7 and 8 · p. 44
  • The log-weighted construction contracts adjacent equal-bag nodes and bounds the refined decomposition by controlling the path segments between marked nodes.Source: A Proofs of Lemmas 7 and 8 · pp. 44–46

B Proofs of Lemmas 12 and 13

The appendix proves two normalization results: multiclause refutations can be reduced to resolution without increasing length or width, and mDNF refutations can be reduced to k-DNF-Res with constant-factor length.

Lemma 12

  • Every mRes refutation yields a resolution refutation of no greater length or width.If each variable is resolved at most once per proof-DAG path in variable-eliminating steps, the resulting resolution refutation is regular.Source: B Proofs of Lemmas 12 and 13 · pp. 46–47
  • The reduction of an mRes resolution step uses resolution when its pivot is eliminated, and weakening when a pivot remains.Together with deleting tautological clauses, this constructs the ordinary resolution refutation from the reduced multiclauses.Source: B Proofs of Lemmas 12 and 13 · p. 47

Lemma 13

  • Every k-mDNF-Res refutation yields a k-DNF-Res refutation of length at most 3|π|.The construction derives the reduction of each mDNF while preserving the bound of k literals per term.Source: B Proofs of Lemmas 12 and 13 · pp. 47–48

C Proofs of the lemmas in Subsection 4.3

These proofs establish bag invariants for tree-decomposition nodes and characterize inconsistency through local conditions at join, introduce, and forget nodes.

Join nodes

  • At a join node, the children’s variable and clause sets unite to the parent’s, and their intersections equal the parent’s bags.Clauses outside the parent clause bag that occur in a child are satisfied by the restriction of any satisfying assignment to that child’s variables.Source: C Proofs of the lemmas in Subsection 4.3 · pp. 48–49
  • A join state is inconsistent exactly when every partition of its clause set leaves at least one child state inconsistent.The proof combines child assignments because they agree on the shared variable bag.Source: C Proofs of the lemmas in Subsection 4.3 · pp. 49–50

Introduce-variable nodes

  • When a variable is introduced, inconsistency is equivalent to inconsistency in the child state after adjusting its clause set for the assigned literal.The literal is determined by the assignment to the introduced variable.Source: C Proofs of the lemmas in Subsection 4.3 · p. 50

Introduce-clause nodes

  • When a clause is introduced, inconsistency depends on whether it is in the tracked clause set and whether the bag assignment satisfies it.If it is tracked but not satisfied, the state is inconsistent; if satisfied, it can be removed from the child’s tracked set.Source: C Proofs of the lemmas in Subsection 4.3 · p. 50

Forget-variable nodes

Forget-clause nodes

D Proof of Theorem 37

The proof constructs a resolution refutation of an extended formula from a bounded-width mDNF refutation. Its stated length is k(n+m)2^O(tw*(F)).

Proof of Theorem 37

  • k(n+m)2^O(tw*(F)) is the length bound for a resolution refutation of the extended formula F′.F′ adds extension-variable clauses for nonempty subsets of the clauses of F.Source: D Proof of Theorem 37 · pp. 51, 53
  • The proof starts from a k-mDNF-Res refutation of F of length (n+m)2^O(tw*(F)).Source: D Proof of Theorem 37 · p. 52
  • Each mDNF derivation step is simulated in O(k) steps in mRes, and Lemma 12 converts the resulting refutation to resolution without increasing its length.Source: D Proof of Theorem 37 · p. 53
Loading 2610.02047v1…