Resolution Lower Bounds for Clique Certification

Research-attempt provenance

Definitions and mathematical statement

Shared notation.

Standard number systems are denoted by $\mathbb N,\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$; index ranges, computational models and specialized notation follow the cited problem source and the definitions below.

Resolution derives $A\lor B$ from $A\lor x$ and $B\lor\neg x$ and refutes a CNF by deriving the empty clause. A clique is a set of pairwise adjacent vertices; nonexistence must be encoded into the source's CNF.

A refutation is a derivation of contradiction from an unsatisfiable constraint system using specified inference rules. Proof size counts the encoded derivation, and degree in algebraic proof systems is the largest polynomial degree appearing.

Statement recorded in the supplied source.

Can one prove an unconditional lower bound of the form $n^{\Omega(k)}$ for resolution, or for another restricted proof system, when certifying that an $n$-vertex graph has no $k$-clique? [S2]

Scope qualification.

The graph family, non-clique promise, formula encoding, and scaling of $k$ must be supplied by the report.

Source status.

The supplied catalogue labels this record partially solved. Its source-status metadata was checked against the supplied snapshot on 2026-10-11. This import does not independently establish current open status or mathematical correctness. The catalogue literature assessment is dated 2026-08-21.

Short English statement

Prove the stated parameter-dependent lower bounds for proofs of clique nonexistence.

Sources

• S1 Ulam AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 30003552 (OWR-15580-004). Catalogue curation and metadata: CC BY 4.0. The supplied source question is retained; definitions and the English summary are editorial additions. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Proof Complexity and Beyond $2018$, Oberwolfach Reports, DOI 10.4171/owr/2017/37, pp. 2299--2361 https://doi.org/10.4171/owr/2017/37.
• S3 Clique Is Hard on Average for Regular Resolution https://doi.org/10.1145/3449352. Underlying Oberwolfach Reports material retains its source-specific licence, including CC BY-SA 4.0 where applicable; see THIRD_PARTY_NOTICES.md.

Preparation and review.

Original question attributed to the cited source and UnsolvedMath contributors. Codex (GPT-6; exact serving revision not exposed) assisted with definitions, English summaries, source inspection and formatting. No new human mathematical authorship or independent proof verification is asserted. Canonical ID 30003552 and source code OWR-15580-004 checked against the complete supplied registry and existing repository statements; known flagged repetitions and obvious identical conjectures excluded. Full mathematical-equivalence/literature review has not been performed. Statement preparation and final review followed contribution prompts C and D; automated checks verify structure and identity, not open status.

Literature and context check

The primary OWR 37/2017 talk, pp. 2317--2318, was read. It explicitly distinguishes general resolution from regular resolution and reports the latter's random-graph lower bound. The primary arXiv abstract of Atserias, Bonacina, de Rezende, Lauria, Nordstrom and Razborov, arXiv:2012.09476, was also consulted; it states the $n^{\Omega(k)}$ regular-resolution result for $k\ll n^{1/4}$ at an appropriate edge density. The full theorem is not re-proved here. Thus the source's "or another restricted system" already includes known material; this attempt does not market it as a new result.

Research attempt: Easy graph certificates and the density gap in a lower-bound route

An explicit polynomial proof on an easy family.

Use the unary clique encoding with variables $X_{i,v}$ for position $i\in\{1,\ldots,k\}$ and graph vertex $v\in\{1,\ldots,n\}$. Include the clauses $P_i=\bigvee_v X_{i,v}$ and the clauses $\neg X_{i,u}\lor\neg X_{j,v}$ forbidding equal or nonadjacent vertices in distinct positions. Additional functionality clauses may be present but are unnecessary below.

Let the graph be empty, with $n\ge1$ and $k\ge2$. For each fixed $u$, all $n$ clauses $\neg X_{1,u}\lor\neg X_{2,v}$ occur. Resolve $P_2$ successively against them, once for each $v$, deriving $\neg X_{1,u}$ in $n$ steps. Resolving $P_1$ successively against these $n$ unit clauses gives the empty clause. The total number of new lines is at most $n^2+n$, independent of $k$. It is even a regular derivation: each path inside a unit-clause subproof resolves each position-two variable at most once; after joining the final chain it resolves each position-one variable at most once, and the two sets of pivots are disjoint.

Thus an $n^{\Omega(k)}$ claim cannot quantify over every graph with no $k$-clique. The actual source asks for suitably hard families, so this is a boundary test rather than a disproof of its intended target.

First moments do not identify a hard family.

For an Erdős--Rényi graph with independent edge probability $p$ and $2\le k\le n$, let $Y$ count $k$-cliques. Then \[ \mathbb EY=\binom nk p^{k(k-1)/2}. \] For $p=n^{-2(1+\epsilon)/(k-1)}$ and $\epsilon>0$, this is at most $n^{-\epsilon k}/k!$, so the probability of containing a $k$-clique is at most that number. This proves that the random formulas are usually unsatisfiable, but supplies no resolution lower bound.

The missing implication is falsified by a more extreme density. If $p\le n^{-3}$, a union bound gives $\Pr(G\text{ has any edge})\le\binom n2p\le1/(2n)$. With probability tending to one the graph is empty and has the short regular refutation just constructed. For example, $k=\lceil\log n\rceil$ (for sufficiently large $n$) still gives only $O(n^2)$ proof length on that event, far below $n^{c k}$ for every fixed $c>0$. Selecting a density because it ensures clique absence is therefore inadequate; a lower-bound proof needs the appropriate residual extension structure or another invariant in addition to absence.

Where the attempted generalization stops.

Regular proofs forbid repeating a pivot on a path. General resolution does not. A counting argument about branches of a regular search proof cannot simply count general proof DAG nodes: different histories may merge and later reuse a variable. The explicit upper bound above does not address that obstacle. Establishing a lower-bound measure preserved under arbitrary reuse, in the source's intended unary encoding and hard density regime, is the missing step.

Verification and adversarial audit

The short proof was checked for $n=1$, $k=2$, the presence of optional functionality clauses, and regularity of every path. The random-graph estimates use independent edges, not independent clique indicators; Markov and a union bound suffice, so no false clique-independence assumption is used. The known regular-resolution theorem is reported only at the scope actually stated in its consulted primary abstract.

Audit corrections.

Removed an implicit universal quantifier over all clique-free graphs and an invalid inference from first-moment clique absence to proof hardness. Preserved the distinction between regular and unrestricted resolution.

External computation.

None; symbolic arguments and boundary checks only.

Scope and remaining gaps

No general-resolution lower bound of the requested scale is proved, and the known regular-resolution answer is not rederived or claimed as new. The graph family, encoding and $k$ regime are essential. The first gap is a hard-family lower-bound invariant; mere unsatisfiability and naive branch counting do not provide it.

Integration review.

Codex (GPT-6; exact serving revision not exposed) reviewed the written arguments and expanded layout and source-reference wrappers. Repository metadata and the production web renderer were checked using Python 3.13 and JavaScript with MathJax 3.2.2. This model-assisted review is not independent human proof verification; no PDF compilation or formal proof checking is asserted.

Completion Estimate

COMPLETION: 0% The calculations below the preserved source statement investigate a concrete route, but establish no substantiated new progress toward the entire original target. Known special cases and failed sufficient conditions are not credited as a solution.

References

The original source references and catalogue attribution are preserved in the Sources section above. The following URLs were actually consulted for this attempt; retention of an additional original reference does not claim fresh consultation of it.

• https://ems.press/content/serial-article-files/46700 (consulted 2026-10-11).
• https://arxiv.org/abs/2012.09476 (consulted 2026-10-11).

Model and contributor disclosure

OpenAI gpt-6-astra, requested reasoning configuration ultra, generated this research attempt on 2026-10-11. The exact serving revision is not exposed. Codex GPT-6 performed orchestration, repository-format review, and written-proof review of this attempt; its exact serving revision is also not exposed. The mathematical route, boundary checks and final adversarial self-audit followed contribution prompts A then B in docs/contribution_prompts.md, after reading CONTRIBUTING.md. Python 3.14.2 assembled the standalone documents; any mathematical computation is specified in Verification. No theorem prover was used. No human mathematical authorship, substantial human proof correction, or independent human proof checking is asserted. Model-assisted review, source retrieval, and structural checks do not establish correctness or novelty. Full private reasoning transcripts are unavailable as reproducibility artifacts; the complete arguments, inputs and outcomes actually used are stated here or in the companion batch audit.

Final status

Unresolved as a new research contribution. This is a concrete route investigation, not a claim of new complete resolution or a current-status certification. A known answer reproduced for context does not become a new contribution. The catalogue's source-status label is preserved; this attempt status does not assert that a source-labelled solved question is open.