Tree-like resolution complexity of two planar problems

TL;DR

This paper proves exponential lower bounds on the tree-like resolution complexity of two planar CSP problems, one related to Sperner's lemma and the other to arrow matching, highlighting their computational hardness.

Contribution

It establishes exponential tree-like resolution complexity bounds for two specific planar CSPs, connecting them to PPAD-complete problems and extending known lower bounds.

Findings

Tree-like resolution complexity is $2^{ heta(n)}$ for both CSPs.

Lower bound of $ ext{Omega}(n)$ requests for Sperner's lemma CSP.

Both CSPs are related to PPAD-complete problems.

Abstract

We consider two CSP problems: the first CSP encodes 2D Sperner's lemma for the standard triangulation of the right triangle on $n^2$ small triangles; the second CSP encodes the fact that it is impossible to match cells of $n \times n$ square to arrows (two horizontal, two vertical and four diagonal) such that arrows in two cells with a common edge differ by at most $45^\circ$, and all arrows on the boundary of the square do not look outside (this fact is a corollary of the Brower's fixed point theorem). We prove that the tree-like resolution complexities of these CSPs are $2^{\Theta(n)}$. For Sperner's lemma our result implies $\Omega(n)$ lower bound on the number of request to colors of vertices that is enough to make in order to find a trichromatic triangle; this lower bound was originally proved by Crescenzi and Silvestri. CSP based on Sperner's lemma is related with the $\rm PPAD$-complete problem. We show that CSP corresponding to arrows is also related with a $\rm PPAD$-complete problem.