2 citations · 4 across the 6 of their papers we have counts for
9 papers
Truly Supercritical Trade-offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler-Leman
Susanna F. de Rezende, Noah Fleming, Duri Andrea Janett +2
We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any circuit must have depth super-linear or even s…
Limits of CDCL Learning via Merge Resolution
Marc Vinyals, Chunxiao Li, Noah Fleming +2
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. Howeve…
Low Degree Testing over the Reals
Vipul Arora, Arnab Bhattacharyya, Noah Fleming +2
We study the problem of testing whether a function is a polynomial of degree at most in the \emph{distribution-free} testing model. Here, the d…
On the Hierarchical Community Structure of Practical Boolean Formulas
Chunxiao Li, Jonathan Chung, Soham Mukherjee +5
Modern CDCL SAT solvers easily solve industrial instances containing tens of millions of variables and clauses, despite the theoretical intractability of the SAT problem. This gap…
On the Power and Limitations of Branch and Cut
Noah Fleming, Mika Göös, Russell Impagliazzo +4
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 simul…
Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
Chunxiao Li, Noah Fleming, Marc Vinyals +2
Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been…