Search Results

Documents authored by Fleming, Noah

Document
DOI: 10.4230/LIPIcs.SAT.2023.27
Limits of CDCL Learning via Merge Resolution

Authors: Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
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.
Cite as

Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh. Limits of CDCL Learning via Merge Resolution. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vinyals_et_al:LIPIcs.SAT.2023.27,
  author =	{Vinyals, Marc and Li, Chunxiao and Fleming, Noah and Kolokolova, Antonina and Ganesh, Vijay},
  title =	{{Limits of CDCL Learning via Merge Resolution}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{27:1--27:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.27},
  URN =		{urn:nbn:de:0030-drops-184894},
  doi =		{10.4230/LIPIcs.SAT.2023.27},
  annote =	{Keywords: proof complexity, resolution, merge resolution, CDCL, learning scheme}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2023.30
TFNP Characterizations of Proof Systems and Monotone Circuits

Authors: Sam Buss, Noah Fleming, and Russell Impagliazzo

Published in: LIPIcs, Volume 251, 14th Innovations in Theoretical Computer Science Conference (ITCS 2023)

Abstract
Connections between proof complexity and circuit complexity have become major tools for obtaining lower bounds in both areas. These connections - which take the form of interpolation theorems and query-to-communication lifting theorems - translate efficient proofs into small circuits, and vice versa, allowing tools from one area to be applied to the other. Recently, the theory of TFNP has emerged as a unifying framework underlying these connections. For many of the proof systems which admit such a connection there is a TFNP problem which characterizes it: the class of problems which are reducible to this TFNP problem via query-efficient reductions is equivalent to the tautologies that can be efficiently proven in the system. Through this, proof complexity has become a major tool for proving separations in black-box TFNP. Similarly, for certain monotone circuit models, the class of functions that it can compute efficiently is equivalent to what can be reduced to a certain TFNP problem in a communication-efficient manner. When a TFNP problem has both a proof and circuit characterization, one can prove an interpolation theorem. Conversely, many lifting theorems can be viewed as relating the communication and query reductions to TFNP problems. This is exciting, as it suggests that TFNP provides a roadmap for the development of further interpolation theorems and lifting theorems. In this paper we begin to develop a more systematic understanding of when these connections to TFNP occur. We give exact conditions under which a proof system or circuit model admits a characterization by a TFNP problem. We show: - Every well-behaved proof system which can prove its own soundness (a reflection principle) is characterized by a TFNP problem. Conversely, every TFNP problem gives rise to a well-behaved proof system which proves its own soundness. - Every well-behaved monotone circuit model which admits a universal family of functions is characterized by a TFNP problem. Conversely, every TFNP problem gives rise to a well-behaved monotone circuit model with a universal problem. As an example, we provide a TFNP characterization of the Polynomial Calculus, answering a question from [Mika Göös et al., 2022], and show that it can prove its own soundness.
Cite as

Sam Buss, Noah Fleming, and Russell Impagliazzo. TFNP Characterizations of Proof Systems and Monotone Circuits. In 14th Innovations in Theoretical Computer Science Conference (ITCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 251, pp. 30:1-30:40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{buss_et_al:LIPIcs.ITCS.2023.30,
  author =	{Buss, Sam and Fleming, Noah and Impagliazzo, Russell},
  title =	{{TFNP Characterizations of Proof Systems and Monotone Circuits}},
  booktitle =	{14th Innovations in Theoretical Computer Science Conference (ITCS 2023)},
  pages =	{30:1--30:40},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-263-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{251},
  editor =	{Tauman Kalai, Yael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2023.30},
  URN =		{urn:nbn:de:0030-drops-175332},
  doi =		{10.4230/LIPIcs.ITCS.2023.30},
  annote =	{Keywords: Proof Complexity, Circuit Complexity, TFNP}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2022.69
On Semi-Algebraic Proofs and Algorithms

Authors: Noah Fleming, Mika Göös, Stefan Grosser, and Robert Robere

Published in: LIPIcs, Volume 215, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)

Abstract
We give a new characterization of the Sherali-Adams proof system, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula C if and only if there is an ε > 0 and a degree-d conical junta J such that viol_C(x) - ε = J, where viol_C(x) counts the number of falsified clauses of C on an input x. Using this result we show that the linear separation complexity, a complexity measure recently studied by Hrubeš (and independently by de Oliveira Oliveira and Pudlák under the name of weak monotone linear programming gates), monotone feasibly interpolates Sherali-Adams proofs. We then investigate separation results for viol_C(x) - ε. In particular, we give a family of unsatisfiable CNF formulas C which have polynomial-size and small-width resolution proofs, but for which any representation of viol_C(x) - 1 by a conical junta requires degree Ω(n); this resolves an open question of Filmus, Mahajan, Sood, and Vinyals. Since Sherali-Adams can simulate resolution, this separates the non-negative degree of viol_C(x) - 1 and viol_C(x) - ε for arbitrarily small ε > 0. Finally, by applying lifting theorems, we translate this lower bound into new separation results between extension complexity and monotone circuit complexity.
Cite as

Noah Fleming, Mika Göös, Stefan Grosser, and Robert Robere. On Semi-Algebraic Proofs and Algorithms. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 69:1-69:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.ITCS.2022.69,
  author =	{Fleming, Noah and G\"{o}\"{o}s, Mika and Grosser, Stefan and Robere, Robert},
  title =	{{On Semi-Algebraic Proofs and Algorithms}},
  booktitle =	{13th Innovations in Theoretical Computer Science Conference (ITCS 2022)},
  pages =	{69:1--69:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-217-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{215},
  editor =	{Braverman, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2022.69},
  URN =		{urn:nbn:de:0030-drops-156658},
  doi =		{10.4230/LIPIcs.ITCS.2022.69},
  annote =	{Keywords: Proof Complexity, Extended Formulations, Circuit Complexity, Sherali-Adams}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2022.70
Extremely Deep Proofs

Authors: Noah Fleming, Toniann Pitassi, and Robert Robere

Published in: LIPIcs, Volume 215, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)

Abstract
We further the study of supercritical tradeoffs in proof and circuit complexity, which is a type of tradeoff between complexity parameters where restricting one complexity parameter forces another to exceed its worst-case upper bound. In particular, we prove a new family of supercritical tradeoffs between depth and size for Resolution, Res(k), and Cutting Planes proofs. For each of these proof systems we construct, for each c ≤ n^{1-ε}, a formula with n^{O(c)} clauses and n variables that has a proof of size n^{O(c)} but in which any proof of size no more than roughly exponential in n^{1-ε}/c must necessarily have depth ≈ n^c. By setting c = o(n^{1-ε}) we therefore obtain exponential lower bounds on proof depth; this far exceeds the trivial worst-case upper bound of n. In doing so we give a simplified proof of a supercritical depth/width tradeoff for tree-like Resolution from [Alexander A. Razborov, 2016]. Finally, we outline several conjectures that would imply similar supercritical tradeoffs between size and depth in circuit complexity via lifting theorems.
Cite as

Noah Fleming, Toniann Pitassi, and Robert Robere. Extremely Deep Proofs. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 70:1-70:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.ITCS.2022.70,
  author =	{Fleming, Noah and Pitassi, Toniann and Robere, Robert},
  title =	{{Extremely Deep Proofs}},
  booktitle =	{13th Innovations in Theoretical Computer Science Conference (ITCS 2022)},
  pages =	{70:1--70:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-217-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{215},
  editor =	{Braverman, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2022.70},
  URN =		{urn:nbn:de:0030-drops-156665},
  doi =		{10.4230/LIPIcs.ITCS.2022.70},
  annote =	{Keywords: Proof Complexity, Tradeoffs, Resolution, Cutting Planes}
}
Document
DOI: 10.4230/LIPIcs.CCC.2021.6
On the Power and Limitations of Branch and Cut

Authors: Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)

Abstract
The Stabbing Planes proof system [Paul Beame et al., 2018] 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 od 2 - which are canonical hard examples for many algebraic proof systems. In a recent (and surprising) result, Dadush and Tiwari [Daniel Dadush and Samarth Tiwari, 2020] 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.
Cite as

Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the Power and Limitations of Branch and Cut. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.CCC.2021.6,
  author =	{Fleming, Noah and G\"{o}\"{o}s, Mika and Impagliazzo, Russell and Pitassi, Toniann and Robere, Robert and Tan, Li-Yang and Wigderson, Avi},
  title =	{{On the Power and Limitations of Branch and Cut}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{6:1--6:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.6},
  URN =		{urn:nbn:de:0030-drops-142809},
  doi =		{10.4230/LIPIcs.CCC.2021.6},
  annote =	{Keywords: Proof Complexity, Integer Programming, Cutting Planes, Branch and Cut, Stabbing Planes}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.22
Distribution-Free Testing of Linear Functions on ℝⁿ

Authors: Noah Fleming and Yuichi Yoshida

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
We study the problem of testing whether a function f:ℝⁿ → ℝ is linear (i.e., both additive and homogeneous) in the distribution-free property testing model, where the distance between functions is measured with respect to an unknown probability distribution over ℝⁿ. We show that, given query access to f, sampling access to the unknown distribution as well as the standard Gaussian, and ε > 0, we can distinguish additive functions from functions that are ε-far from additive functions with O((1/ε)log(1/ε)) queries, independent of n. Furthermore, under the assumption that f is a continuous function, the additivity tester can be extended to a distribution-free tester for linearity using the same number of queries. On the other hand, we show that if we are only allowed to get values of f on sampled points, then any distribution-free tester requires Ω(n) samples, even if the underlying distribution is the standard Gaussian.
Cite as

Noah Fleming and Yuichi Yoshida. Distribution-Free Testing of Linear Functions on ℝⁿ. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.ITCS.2020.22,
  author =	{Fleming, Noah and Yoshida, Yuichi},
  title =	{{Distribution-Free Testing of Linear Functions on \mathbb{R}ⁿ}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.22},
  URN =		{urn:nbn:de:0030-drops-117076},
  doi =		{10.4230/LIPIcs.ITCS.2020.22},
  annote =	{Keywords: Property Testing, Distribution-Free Testing, Linearity Testing}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2018.10
Stabbing Planes

Authors: Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere

Published in: LIPIcs, Volume 94, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018)

Abstract
We introduce and develop a new semi-algebraic proof system, called Stabbing Planes that is in the style of DPLL-based modern SAT solvers. As with DPLL, there is only one rule: the current polytope can be subdivided by branching on an inequality and its "integer negation." That is, we can (nondeterministically choose) a hyperplane a x >= b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying a x >= b, the points satisfying a x <= b-1, and the middle slab b-1 < a x < 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 somewhat surprisingly that Stabbing Planes can efficiently simulate Cutting Planes, and moreover, is strictly stronger than Cutting Planes under a reasonable conjecture. We prove linear lower bounds on the rank of Stabbing Planes refutations, by adapting a lifting argument in communication complexity.
Cite as

Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing Planes. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 94, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{beame_et_al:LIPIcs.ITCS.2018.10,
  author =	{Beame, Paul and Fleming, Noah and Impagliazzo, Russell and Kolokolova, Antonina and Pankratov, Denis and Pitassi, Toniann and Robere, Robert},
  title =	{{Stabbing Planes}},
  booktitle =	{9th Innovations in Theoretical Computer Science Conference (ITCS 2018)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-060-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{94},
  editor =	{Karlin, Anna R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2018.10},
  URN =		{urn:nbn:de:0030-drops-83418},
  doi =		{10.4230/LIPIcs.ITCS.2018.10},
  annote =	{Keywords: Complexity Theory, Proof Complexity, Communication Complexity, Cutting Planes, Semi-Algebraic Proof Systems, Pseudo Boolean Solvers, SAT solvers, Inte}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact