Noah Fleming

STOC Conference 2025 Conference Paper

Truly Supercritical Trade-Offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler-Leman

• Susanna F. de Rezende
• Noah Fleming
• Duri Andrea Janett
• Jakob Nordström
• Shuo Pang 0002

STOC Conference 2024 Conference Paper

Black-Box PPP Is Not Turing-Closed

• Noah Fleming
• Stefan Grosser
• Toniann Pitassi
• Robert Robere

SAT Conference 2023 Conference Paper

Limits of CDCL Learning via Merge Resolution

• Marc Vinyals
• Chunxiao Li 0002
• Noah Fleming
• Antonina Kolokolova
• Vijay Ganesh 0001

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. However, previous work does not address the tightness of the simulation, i. e. , the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.

SODA Conference 2023 Conference Paper

Low Degree Testing over the Reals

• Vipul Arora 0002
• Arnab Bhattacharyya 0001
• Noah Fleming
• Esty Kelman
• Yuichi Yoshida

SAT Conference 2021 Conference Paper

On the Hierarchical Community Structure of Practical Boolean Formulas

• Chunxiao Li 0002
• Jonathan Chung 0003
• Soham Mukherjee
• Marc Vinyals
• Noah Fleming
• Antonina Kolokolova
• Alice Mu
• Vijay Ganesh 0001

Abstract 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 between practice and theory is a central problem in solver research. It is believed that SAT solvers exploit structure inherent in industrial instances, and hence there have been numerous attempts over the last 25 years at characterizing this structure via parameters. These can be classified as rigorous, i. e. , they serve as a basis for complexity-theoretic upper bounds (e. g. , backdoors), or correlative, i. e. , they correlate well with solver run time and are observed in industrial instances (e. g. , community structure). Unfortunately, no parameter proposed to date has been shown to be both strongly correlative and rigorous over a large fraction of industrial instances. Given the sheer difficulty of the problem, we aim for an intermediate goal of proposing a set of parameters that is strongly correlative and has good theoretical properties. Specifically, we propose parameters based on a graph partitioning called Hierarchical Community Structure (HCS), which captures the recursive community structure of a graph of a Boolean formula. We show that HCS parameters are strongly correlative with solver run time using an Empirical Hardness Model, and further build a classifier based on HCS parameters that distinguishes between easy industrial and hard random/crafted instances with very high accuracy. We further strengthen our hypotheses via scaling studies. On the theoretical side, we show that counterexamples which plagued flat community structure do not apply to HCS, and that there is a subset of HCS parameters such that restricting them limits the size of embeddable expanders.

SAT Conference 2020 Conference Paper

Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers

• Chunxiao Li 0002
• Noah Fleming
• Marc Vinyals
• Toniann Pitassi
• Vijay Ganesh 0001

Abstract 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 well-established empirically, a theoretical understanding of whether restarts are indeed crucial to the power of CDCL solvers is missing. In this paper, we prove a series of theoretical results that characterize the power of restarts for various models of SAT solvers. More precisely, we make the following contributions. First, we prove an exponential separation between a drunk randomized CDCL solver model with restarts and the same model without restarts using a family of satisfiable instances. Second, we show that the configuration of CDCL solver with VSIDS branching and restarts (with activities erased after restarts) is exponentially more powerful than the same configuration without restarts for a family of unsatisfiable instances. To the best of our knowledge, these are the first separation results involving restarts in the context of SAT solvers. Third, we show that restarts do not add any proof complexity-theoretic power vis-a-vis a number of models of CDCL and DPLL solvers with non-deterministic static variable and value selection.

FOCS Conference 2017 Conference Paper

Random Θ(log n)-CNFs Are Hard for Cutting Planes

• Noah Fleming
• Denis Pankratov
• Toniann Pitassi
• Robert Robere

The random k-SAT model is the most important and well-studied distribution over k-SAT instances. It is closely connected to statistical physics and is a benchmark for satisfiability algorithms. We show that when k = Θ(log n), any Cutting Planes refutation for random k-SAT requires exponential size in the interesting regime where the number of clauses guarantees that the formula is unsatisfiable with high probability.