arXiv subjects

Robert Robere

Publications and source records attributed to Robert Robere.

14 recordsLinked to original sources

arXiv2026

Provable Reductions in TFNP

We introduce a new family of propositional proof systems, denoted , for an arbitrary TFNP search problem $R$. Informally, a refutation of a CNF formula $F$ in is given by a polynomial-time reduction from the false-clause search problem $Search_F$ to $R$, combined with an Extended Frege proof that the reduction is correct. These are motivated in two ways: 1. They are the propositional translations of witnessing theorems in bounded arithmetic, by which proofs of $\forall \Sigma^b_1$ formulas $\phi$ in a theory $T$ imply algorithms solving the search problem for $\phi$ in a TFNP class corresponding to $T$. 2. They are a white-box analogue of the characterizations of proof systems using decision tree reductions to black-box TFNP problems. We consider the proof system , where Iter is a complete problem for PLS. We prove that is polynomially equivalent to the sequent calculus $G_1$, and also to the implicit Resolution proof system [EF, Resolution]. Hence $G_1$ and [EF, Resolution] are equivalent, which is the first characterization of an implicit proof system by a classical proof system beyond the work of Wang. We also consider for general TFNP relations $R$. We observe that if EF can prove that a search problem $R$ is in FP, then is polynomially equivalent to EF. This contrasts to our above result, which shows that Extended-Frege provable reductions to $Iter$, a problem widely believed not to be in FP, yields a proof system ($G_1$) that is believed to be stronger than Extended Frege. Finally, we show that for any proof system $P$ which is sufficiently strong, there is a polynomial-time computable search problem $R_P \in $ FP such that is polynomially equivalent to $P$. Letting $P =$ [EF, Resolution] and combining our two results shows that is polynomially equivalent to .

cs.CC↗

arXiv2026

Lower Bounds for Approximate Sign Rank

We prove new upper and lower bounds on $\epsilon$-approximate sign-rank, a relaxation of sign-rank introduced by Chornomaz, Moran, and Waknine (STOC 2025). We show that every $m \times n$ sign matrix with approximate sign-rank $d$ contains a monochromatic rectangle of size $d^{-O(d)}m \times d^{-O(d^2)}n$, paralleling classical results for exact sign-rank. As an application, we establish a lower bound of $\Omega(\sqrt{d/\log d})$ on the $\epsilon$-approximate sign-rank of large-margin $d$-dimensional half-spaces. Prior to our work, the only general lower bound technique known for approximate sign-rank yielded bounds of strength $\epsilon^{-1} - 1$, which are constant for fixed $\epsilon$. A key ingredient is a new geometric theorem on hyperplane avoidance: for any set of $n$ points in general position in $\mathbb{R}^d$, there exist $d$ subsets, each of size $d^{-O(d)} n$, such that no hyperplane simultaneously splits all of them. The proof combines the Forster-Barthe isotropic position theorem with the Bourgain-Tzafriri restricted invertibility principle. We also study the relationship between approximate sign-rank and VC dimension. We prove a lower bound on approximate sign-rank in terms of VC dimension, and exhibit concept classes of VC dimension $2$ with large approximate sign-rank. Finally, we study the approximate sign-rank of the $2^m \times 2^m$ Hadamard matrix $H_m$. The sign-rank of $H_m$ is known to be $\Omega(\sqrt{2^m})$ by Forster's classic theorem. Contrasting this, we adapt an argument of Alman and Williams to show that the approximate sign-rank of $H_m$ is at most $m^{O(\sqrt{m} \log(1/\epsilon))}$, and hence the Hadamard matrix does not witness polynomial-strength lower bounds for approximate sign-rank. Using our VC dimension bound, we prove that the approximate sign-rank of $H_m$ is at least $\Omega_\epsilon(m)$.

cs.CC↗

arXiv2024

On Pigeonhole Principles and Ramsey in TFNP

We show that the TFNP problem RAMSEY is not black-box reducible to PIGEON, refuting a conjecture of Goldberg and Papadimitriou in the black-box setting. We prove this by giving reductions to RAMSEY from a new family of TFNP problems that correspond to generalized versions of the pigeonhole principle, and then proving that these generalized versions cannot be reduced to PIGEON. Formally, we define t-PPP as the class of total NP-search problems reducible to finding a t-collision in a mapping from (t-1)N+1 pigeons to N holes. These classes are closely related to multi-collision resistant hash functions in cryptography. We show that the generalized pigeonhole classes form a hierarchy as t increases, and also give a natural condition on the parameters t1, t2 that captures exactly when t1-PPP and t2-PPP collapse in the black-box setting. Finally, we prove other inclusion and separation results between these generalized PIGEON problems and other previously studied TFNP subclasses, such as PLS, PPA and PLC. Our separation results rely on new lower bounds in propositional proof complexity based on pseudoexpectation operators, which may be of independent interest.

cs.CC↗

arXiv2022

Separations in Proof Complexity and TFNP

It is well-known that Resolution proofs can be efficiently simulated by Sherali-Adams (SA) proofs. We show, however, that any such simulation needs to exploit huge coefficients: Resolution cannot be efficiently simulated by SA when the coefficients are written in unary. We also show that Reversible Resolution (a variant of MaxSAT Resolution) cannot be efficiently simulated by Nullstellensatz (NS). These results have consequences for total NP search problems. First, we characterise the classes PPADS, PPAD, SOPL by unary-SA, unary-NS, and Reversible Resolution, respectively. Second, we show that, relative to an oracle, PLS $\not\subseteq$ PPP, SOPL $\not\subseteq$ PPA, and EOPL $\not\subseteq$ UEOPL. In particular, together with prior work, this gives a complete picture of the black-box relationships between all classical TFNP classes introduced in the 1990s.

cs.CC↗

arXiv2022

Proofs, Circuits, and Communication

We survey lower-bound results in complexity theory that have been obtained via newfound interconnections between propositional proof complexity, boolean circuit complexity, and query/communication complexity. We advocate for the theory of total search problems (TFNP) as a unifying language for these connections and discuss how this perspective suggests a whole programme for further research.

cs.CC↗

arXiv2022

Further Collapses in TFNP

We show $\textsf{EOPL}=\textsf{PLS}\cap\textsf{PPAD}$. Here the class $\textsf{EOPL}$ consists of all total search problems that reduce to the End-of-Potential-Line problem, which was introduced in the works by Hubacek and Yogev (SICOMP 2020) and Fearnley et al. (JCSS 2020). In particular, our result yields a new simpler proof of the breakthrough collapse $\textsf{CLS}=\textsf{PLS}\cap\textsf{PPAD}$ by Fearnley et al. (STOC 2021). We also prove a companion result $\textsf{SOPL}=\textsf{PLS}\cap\textsf{PPADS}$, where $\textsf{SOPL}$ is the class associated with the Sink-of-Potential-Line problem.

cs.CC↗

arXiv2021

On the Power and Limitations of Branch and Cut

The Stabbing Planes proof system was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas -- certain unsatisfiable systems of linear equations mod 2 -- which are canonical hard examples for many algebraic proof systems. In a recent (and surprising) result, Dadush and Tiwari showed that these short refutations of the Tseitin formulas could be translated into quasi-polynomial size and depth Cutting Planes proofs, refuting a long-standing conjecture. This translation raises several interesting questions. First, whether all Stabbing Planes proofs can be efficiently simulated by Cutting Planes. This would allow for the substantial analysis done on the Cutting Planes system to be lifted to practical mixed integer programming solvers. Second, whether the quasi-polynomial depth of these proofs is inherent to Cutting Planes. In this paper we make progress towards answering both of these questions. First, we show that any Stabbing Planes proof with bounded coefficients SP* can be translated into Cutting Planes. As a consequence of the known lower bounds for Cutting Planes, this establishes the first exponential lower bounds on SP*. Using this translation, we extend the result of Dadush and Tiwari to show that Cutting Planes has short refutations of any unsatisfiable system of linear equations over a finite field. Like the Cutting Planes proofs of Dadush and Tiwari, our refutations also incur a quasi-polynomial blow-up in depth, and we conjecture that this is inherent. As a step towards this conjecture, we develop a new geometric technique for proving lower bounds on the depth of Cutting Planes proofs. This allows us to establish the first lower bounds on the depth of Semantic Cutting Planes proofs of the Tseitin formulas.

cs.CC↗

arXiv2020

KRW Composition Theorems via Lifting

One of the major open problems in complexity theory is proving super-logarithmic lower bounds on the depth of circuits (i.e., $\mathbf{P}\not\subseteq\mathbf{NC}^1$). Karchmer, Raz, and Wigderson (Computational Complexity 5(3/4), 1995) suggested to approach this problem by proving that depth complexity behaves "as expected" with respect to the composition of functions $f\diamond g$. They showed that the validity of this conjecture would imply that $\mathbf{P}\not\subseteq\mathbf{NC}^1$. Several works have made progress toward resolving this conjecture by proving special cases. In particular, these works proved the KRW conjecture for every outer function $f$, but only for few inner functions $g$. Thus, it is an important challenge to prove the KRW conjecture for a wider range of inner functions. In this work, we extend significantly the range of inner functions that can be handled. First, we consider the $\textit{monotone}$ version of the KRW conjecture. We prove it for every monotone inner function $g$ whose depth complexity can be lower bounded via a query-to-communication lifting theorem. This allows us to handle several new and well-studied functions such as the $s\textbf{-}t$-connectivity, clique, and generation functions. In order to carry this progress back to the $\textit{non-monotone}$ setting, we introduce a new notion of $\textit{semi-monotone}$ composition, which combines the non-monotone complexity of the outer function $f$ with the monotone complexity of the inner function $g$. In this setting, we prove the KRW conjecture for a similar selection of inner functions $g$, but only for a specific choice of the outer function $f$.

cs.CC↗

arXiv2020

Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling

We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph $G$ can be reversibly pebbled in time $t$ and space $s$ if and only if there is a Nullstellensatz refutation of the pebbling formula over $G$ in size $t+1$ and degree $s$ (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.

cs.CC↗

arXiv2020

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems: * We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. * We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known. An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

cs.CC↗

arXiv2017

Stabbing Planes

We develop a new semi-algebraic proof system called Stabbing Planes which formalizes modern branch-and-cut algorithms for integer programming and is in the style of DPLL-based modern SAT solvers. As with DPLL there is only a single rule: the current polytope can be subdivided by branching on an inequality and its "integer negation." That is, we can (nondeterministically choose) a hyperplane $ax \geq b$ with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying $ax \geq b$, the points satisfying $ax \leq b-1$, and the middle slab $b - 1 < ax < b$. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomial-time checkable. Among our results, we show that Stabbing Planes can efficiently simulate the Cutting Planes proof system, and is equivalent to a tree-like variant of the RCP system of [Krajicek98]. As well, we show that it possesses short proofs of the canonical family of systems of $\mathbb{F}_2$-linear equations known as the Tseitin formulas. Finally, we prove linear lower bounds on the rank of Stabbing Planes refutations by adapting lower bounds in communication complexity and use these bounds in order to show that Stabbing Planes proofs cannot be balanced. In doing so, we show that real communication protocols cannot be balanced and establish the first lower bound on the real communication complexity of the set disjointness function.

cs.CC↗

arXiv2017

Relating Complexity-theoretic Parameters with SAT Solver Performance

Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide variety of large industrial Boolean instances. While some of these parameters have been studied empirically, until now there has not been a unified comparative study of their explanatory power on a comprehensive benchmark. We correct this state of affairs by conducting a large-scale empirical evaluation of CDCL SAT solver performance on nearly 7000 industrial and crafted formulas against several structural parameters such as backdoors, treewidth, backbones, and community structure. Our study led us to several results. First, we show that while such parameters only weakly correlate with CDCL solving time, certain combinations of them yield much better regression models. Second, we show how some parameters can be used as a "lens" to better understand the efficiency of different solving heuristics. Finally, we propose a new complexity-theoretic parameter, which we call learning-sensitive with restarts (LSR) backdoors, that extends the notion of learning-sensitive (LS) backdoors to incorporate restarts and discuss algorithms to compute them. We mathematically prove that for certain class of instances minimal LSR-backdoors are exponentially smaller than minimal-LS backdoors.

cs.AI↗

arXiv2017

Random CNFs are Hard for Cutting Planes

The random k-SAT model is the most important and well-studied distribution over k-SAT instances. It is closely connected to statistical physics; it is used as a testbench for satisfiability algorithms, and average-case hardness over this distribution has also been linked to hardness of approximation via Feige's hypothesis. We prove that any Cutting Planes refutation for random k-SAT requires exponential size, for k that is logarithmic in the number of variables, in the (interesting) regime where the number of clauses guarantees that the formula is unsatisfiable with high probability.

cs.CC↗

arXiv2015

Path Graphs, Clique Trees, and Flowers

An \emph{asteroidal triple} is a set of three independent vertices in a graph such that any two vertices in the set are connected by a path which avoids the neighbourhood of the third. A classical result by Lekkerkerker and Boland \cite{6} showed that interval graphs are precisely the chordal graphs that do not have asteroidal triples. Interval graphs are chordal, as are the \emph{directed path graphs} and the \emph{path graphs}. Similar to Lekkerkerker and Boland, Cameron, Hoáng, and Lévêque \cite{4} gave a characterization of directed path graphs by a "special type" of asteroidal triple, and asked whether or not there was such a characterization for path graphs. We give strong evidence that asteroidal triples alone are insufficient to characterize the family of path graphs, and give a new characterization of path graphs via a forbidden induced subgraph family that we call \emph{sun systems}. Key to our new characterization is the study of \emph{asteroidal sets} in sun systems, which are a natural generalization of asteroidal triples. Our characterization of path graphs by forbidding sun systems also generalizes a characterization of directed path graphs by forbidding odd suns that was given by Chaplick et al.~\cite{9}.

cs.DM↗