Efficient (Propositional) Proofs of Statements
in Combinatorial Topology and Related Areas

Gabriel Istrategabrielistrate@acm.org

1

Acknowledgment- Research program. Multiple papers (SAT’14, ICALP 2015,2021), plus work in progress.
- Coauthors (chronologically): Adrian Crãciun (Timişoara),
James Aisenberg (Seattle), Sam Buss (San Diego),
Maria-Luisa Bonet (Barcelona), Cosmin Bonchiş(Timişoara).

2

"Philosophical" Summary/Outline
Mathematics (in particular Algebraic Topology) often works
with exponential size objects (nonconstructive proofs).
(When) can we make them "small"/constructive ?
- Concrete statement: Kneser-Lovász Theorem, hard toprove (mathematically). Is its propositional encoding
hard in proof complexity ?
- Surprise: easy to prove (mathematically) (withdisclaimers)- How ? Why ?
- Spoiler: versions of notions of kernelization/data
reduction from parameterized complexity theory.
3

Proof Complexity

Given a class of unsatisfiable propositional formulas, how
hard it is to refute them in a certain proof system ?

- Hardness: length/"complexity" of the proof- ... difficulty of finding it also relevant.
- Proof systems: e.g. resolution ...
- (extended) Frege systems- cutting planes, polynomial calculus, nullenstellensatz,sums of squares, semi-algebraic proofs, IPS ....
4

Boundaries of proof complexity: Frege proofs"Textbook-style" proof systems.
Cook-Reckhow: all Frege proof sys poly simulate eachother• Example, for concreteness [Hilbert Ackermann]• propositional variables p1 , p2 , . . . .
• Connectives ¬, or .
• Axiom schemas:
1. ¬(A or A) or A
2. ¬A or (A or B)
3. ¬(A or B) or (B or A)
4. ¬(¬A or B) or (¬(C or A) or (C or B))• Rule: From A and ¬A or B derive B.

Superpolynomial lower bounds: restricted (e.g. depth)
versions of Frege.
5

Proof complexity of the pigeonhole principlen pigeons in n − 1 holes ⇒ at least two pigeons in same hole !
• E.g. Pigeonhole formula(s): PHPnn−1• Xi,j = 1 "pigeon i goes to hole j".
• Xi,1 or Xi,2 or . . . or Xi,n−1 , 1 ≤ i ≤ n (each pigeon goes to(at least) one hole)• Xk ,j or Xk ,i (pigeon k goes to at most one hole).
• Xk ,j or Xl,j (pigeons k and l do not go together to hole j).
• Resolution complexity: exponential ! (Haken)
Theorem (Buss): PHPn has poly-size Frege proofs.
6Extended Frege proofs
Frege proofs + variable substitutions.
We may introduce variable names for formulas X ⇔ Φ(Y ).
Proves the same formulas but potentially with great
reductions in size.
OPEN PROBLEM: Is extended Frege strictly more powerfulthan Frege ? Most natural candidates for separation
turned out to have subexponential Frege proofs.
Wishful thinking: Perhaps translating into SAT amathematical statement that is (mathematically) hard toprove would yield a natural candidate for the separation.
7

Kneser’s Conjecture- Stated in 1955 (Martin Kneser, Jaresbericht DMV)Let n ≥ 2k − 1 ≥ 1. Let c : kn → [n − 2k + 1]. Then
there exist two disjoint sets A and B withc(A) = c(B).

- k = 1 Pigeonhole principle!
- k = 2, 3 combinatorial proofs (Stahl, Garey & Johnson)- k ≥ 4 only proved in 1977 (Lovász) using Algebraic
Topology.
- Combinatorial proofs known (Matousek, Ziegler). "Hide"
Alg. Topology in combinatorics.
No "purely combinatorial" proof was known

8Kneser’s Conjecture (II)- the chromatic number of a certain graph Knn,k (at least)n − 2k + 2. (exact value)
- Vertices: kn . Edges: disjoint sets.
- E.g. k = 2, n = 5: Petersen’s graph has chromatic number(at least) three.
- "Internal graph" also chromatic number n − 2k + 2(Schrijver’s theorem).

9

Lovász-Kneser as an (unsatisfiable) SAT formula- naïve encoding XA,k = TRUE iff A colored with color k .
- XA,1 or XA,2 or . . . or XA,n−2k +1 "every set is colored with(at least) one color"- XA,j or XB,j (A ∩ B = ∅) "no two disjoint sets are coloredwith the same color"- XA,j or XA,k "no set has two colors".
- Fixed k : Kneserk ,n has poly-size (in n).
- Extends encoding of PHP

10

Our results in a nutshell
k +1- Knesernk reduces to (is a special case of) Knesern−2.
- Thus all known lower bounds that hold for PHP hold for
any Kneserk .
- Cases with combinatorial proofs:• k = 2: polynomial size Frege proofs• k = 3: polynomial size extended Frege proofs- k ≥ 4: surprisingly, quasipoly Frege/poly extended Frege
proofs.
Most important, "take-home" message: for every fixed k ,Kneser∗k can be proved (mathematically) by aneasy-to-describe reduction to a finite set of values of n,(to be checked, perhaps on a computer)completely bypassing Algebraic Topology !
(ICALP 2015/Information and Computation 2018, but written in the language of proof complexity)11

Proof idea

Assume there was a (n − 2k + 1)-coloring of Knesernk .
A color class Cl is star shaped if the intersection of allmembers is nonempty.
Theorem: If Cl is not star-shaped then |Cl | ≤ k 2 kn−2−2 .
Reduction, assuming theorem:
If n > k 4 then kn > (n − 2k + 1)k 2 kn−2−2 , hence some color
class is star-shaped Cl . Remove Cl and the central element ofclass Cl .
k .
Conclusion: We get a (n − 2k )-coloring of Knesern−112Proof of the theorem

Let Cl be a non-star-shaped color class.
• Fix some S = {a1 , ..., ak } ∈ Cl .
• For every ai let Si ∈ Pl , ai ̸∈ Si (Cl not star-shaped)• To specify arbitrary T ∈ Cl :• Specify ai ∈ T (S ∩ T ̸= ∅)• Specify x ∈ Si ∩ T .
• Specify the remaining k − 2 elements.

Nr. of choices: k · k · kn−2−2 .

13

If Kneser is not difficult, then what is ?
Discrete version of Borsuk-Ulam: Octahedral Tucker’s lemma.
• Intuition: Borsuk-Ulam - no continuous (a.k.a simplicial) antipodal map from the n-ball to the n-sphere.
• For any labeling of T with vertices from {±1, . . . , ±(n − 1)} antipodal on the boundary there exist twoadjacent vertices v ∼ w with c(v ) = −c(w).

14Octahedral Tucker Lemma
Definition: Let n ≥ 1. The octahedral ball B n is:
B n := {(A, B) : A, B ⊆ [n] and A ∩ B = ∅}.

Definition: Two pairs (A1 , B1 ) and (A2 , B2 ) in B n arecomplementary with respect to λ if A1 ⊆ A2 , B1 ⊆ B2 andλ(A1 , B1 ) = −λ(A2 , B2 ).
Theorem (Octahedral Tucker lemma)
If λ : B n → {1, ±2, . . . , ±n} is antipodal, then there are twoelements in B n that are complementary.
- barycentric subdivision ⇒ exponentially large formula !
15

A class of "hard" formulas based on Octahedral Tucker Lemma- Kneser follows from a new "low dimensional" Tucker lemma.
- Avoid barycentric subdivision. Instead "truncated version".
n is:Definition: Let 1 ≤ k ≤ n. The truncated octahedral ball B≤knn
B≤k:= (A, B) ∈ B n : |A| ≤ k , |B| ≤ k }.

Definition: Let ⪯ be the partial order on sets inby A ⪯ B iff (A ∪ B)≤k = B.

n≤kdefinedn , write
Definition: For (A1 , B1 ) and (A2 , B2 ) in B≤k(A1 , B1 ) ⪯ (A2 , B2 ) when A1 ⪯ A2 , B1 ⪯ B2 , and Ai ∩ Bj = ∅ fori, j ∈ {1, 2}. The pairs (A1 , B1 ) and (A2 , B2 ) arenk -complementary with respect to an antipodal map λ on B≤kif (A1 , B1 ) ⪯ (A2 , B2 ) and λ(A1 , B1 ) = −λ(A2 , B2 ).
16

Truncated Octahedral Tucker Lemman → {1, ±2 . . . , ±n} is
THEOREM: Let n ≥ k ≥ 1. If λ : B≤kn that are
antipodal, then there are two elements in B≤kk -complementary.

- (Mathematically) follows from "ordinary" octahedral
Tucker lemma.
- k -truncated Tucker Implies Kneserk .
- Translates (naturally) to formulas Truncatednk , whose
proof complexity unknown.
- Generates search problem Truncatedk .

17

Complexity of Truncated Tucker Lemma

THEOREM: [ABCCI, journal version] Formulas Tuckern1 havepoly-size extended Frege proofs.
THEOREM: (Aisenberg) Tuckerk ⪯m Tuckerk +1 .
THEOREM: (Aisenberg) Tuckerk hard for PPP.
CONCLUSION: Kneserk may not be "hard", but Tuckerk (which
encodes the topological principle used to prove it) probably is!

18

Why is Kneser easy? What else is?

- kernelization: reduce instance (x, k ) to "kernelinstance" (x ′ , k ′ ), s.t. (x, k ) ∈ L iff (x ′ , k ′ ) ∈ L and|x ′ |, k ′ ≤ g(k ) for some computable g.
- data reduction: algorithm A that maps in timepoly(|x| + k ) (x, k ) to (x ′ , k ′ ) s.t.
(x, k ) ∈ L iff (x ′ , k ′ ) ∈ L and |x ′ | ≤ |x|.
- given r data reductions A1 , . . . , Ar , a data
reduction chain for instance (x, k ) of L: seq.
(x0 , k0 ), (x1 , k1 ), . . . , (xm , km ), where(x0 , k0 ) = (x, k ), At (xm , km ) = (xm , km ) fort = 1, . . . r and, for i = 1, . . . , m ∃j ∈ 1, . . . , r s.t.
(xi , ki ) = Aj (xi−1 , ki−1 ).
19Main idea

- "Negative" instance (x, k ) of parameterized problem in
NP maps "canonically" to formula Φ(x, k ) ∈ SAT .
- If Πi proof for soundness of the reduction rule(xi , ki ) = Aj (xi−1 , ki−1 ) and Πm+1 is a "brute force
proof of unsatisfiability" for the kernel instancethen one can prove Φ(x, k ) ∈ SAT by"concatenating" Π1 , . . . , Πm and Πm+1 .
- Need: data reduction of length O(log(n)) to unwind
variable substitutions.
20

Applications of Kernelization Techniques to Proof Complexity- Extend results on Kneser to Schrijver’s theorem.
- classical (ad-hoc) kernelization for VertexCover ⇒ for every
fixed k , negative instances of VC with parameter k havepoly-size Frege proofs.
- crown decomposition for DualColoring ⇒ negative instances ofVC with parameter k poly-size Frege proofs.
- improved (ad-hoc) kernelization for EDGE CLIQUE COLOR ⇒negative instances (G,k) of EDGE CLIQUE COVER have extended
Frege proofs of poly size and Frege proofs of quasipoly size.
- sunflower lemma-based kernelization of d-HittingSet⇒
negative instances of d-HittingSet extended Frege proofs ofpoly size .
- NEW Turing kernelization: Instances of CLIQUE(VC) havepoly-size Frege proofs.

21Applications to Computational Social Choice- Arrow, Gibbard-Satterthwaite: Fundamental impossibility
results on ranking m objects by n agents.
- Tang & Lin (Artificial Intelligence, 2009): Arrow’s Theorem has
computer-assisted propositional proofs by reducing thegeneral case to the case n = 2, m = 3. Similar results(2008) for the Gibbard-Satterthwaite theorem.
- Their proofs: data reductions of length Θ(n + m).
We give: data reductions of length O(n), whose soundness
can be witnessed by efficient Frege proofs.
Theorem
Formulas Arrowm,n , GSm,n have:• quasipoly size Frege proofs• poly size Frege proofs for fixed n.

22

Further work & Open problems- Proof complexity of parameterized intractable (W[1] andhigher) problems ?
- Open problem: search complexity of the Octahedral
Tucker Lemma ?
- Open problem Proof complexity of cutting planes for
Knesern2 ?
- Logics for implicit proof systems ? Other combinatorial
principles ?

23

Thank you. Questions ?

23