Robert Robere

Riju Bindu, Hamed Hatami, Hasti Karimi et al.

We prove new upper and lower bounds on $ε$-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 $Ω(\sqrt{d/\log d})$ on the $ε$-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 $ε^{-1} - 1$, which are constant for fixed $ε$. 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 $Ω(\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/ε))}$, 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 $Ω_ε(m)$.

Noah Fleming, Stefan Grosser, Toniann Pitassi et al.

We introduce a new family of propositional proof systems, denoted <EF, R>, for an arbitrary TFNP search problem $R$. Informally, a refutation of a CNF formula $F$ in <EF, R> 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 Σ^b_1$ formulas $ϕ$ in a theory $T$ imply algorithms solving the search problem for $ϕ$ 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 <EF, Iter>, where Iter is a complete problem for PLS. We prove that <EF, Iter> 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 <EF, R> for general TFNP relations $R$. We observe that if EF can prove that a search problem $R$ is in FP, then <EF, R> 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 <EF, $R_P$> is polynomially equivalent to $P$. Letting $P =$ [EF, Resolution] and combining our two results shows that <EF, Iter> is polynomially equivalent to <EF, $R_{[EF, Resolution]}$>.

Edward Zulkoski, Ruben Martins, Christoph Wintersteiger et al.

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.