8 Search Results for "Buss, Sam"

Document
DOI: 10.4230/LIPIcs.STACS.2024.59
Lower Bounds for Set-Blocked Clauses Proofs

Authors: Emre Yolcu

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study propositional proof systems with inference rules that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. Each system we study is built on resolution. They are called BC⁻, RAT⁻, SBC⁻, and GER⁻, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution - all "without new variables." They may be viewed as weak versions of extended resolution (ER) since they are defined by first generalizing the extension rule and then taking away the ability to introduce new variables. Except for SBC⁻, they are known to be strictly between resolution and extended resolution. Several separations between these systems were proved earlier by exploiting the fact that they effectively simulate ER. We answer the questions left open: We prove exponential lower bounds for SBC⁻ proofs of a binary encoding of the pigeonhole principle, which separates ER from SBC⁻. Using this new separation, we prove that both RAT⁻ and GER⁻ are exponentially separated from SBC⁻. This completes the picture of their relative strengths.
Cite as

Emre Yolcu. Lower Bounds for Set-Blocked Clauses Proofs. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 59:1-59:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{yolcu:LIPIcs.STACS.2024.59,
  author =	{Yolcu, Emre},
  title =	{{Lower Bounds for Set-Blocked Clauses Proofs}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{59:1--59:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.59},
  URN =		{urn:nbn:de:0030-drops-197698},
  doi =		{10.4230/LIPIcs.STACS.2024.59},
  annote =	{Keywords: proof complexity, separations, resolution, extended resolution, blocked clauses}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2023.56
Robustness for Space-Bounded Statistical Zero Knowledge

Authors: Eric Allender, Jacob Gray, Saachi Mutreja, Harsha Tirumala, and Pengxiang Wang

Published in: LIPIcs, Volume 275, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)

Abstract
We show that the space-bounded Statistical Zero Knowledge classes SZK_L and NISZK_L are surprisingly robust, in that the power of the verifier and simulator can be strengthened or weakened without affecting the resulting class. Coupled with other recent characterizations of these classes [Eric Allender et al., 2023], this can be viewed as lending support to the conjecture that these classes may coincide with the non-space-bounded classes SZK and NISZK, respectively.
Cite as

Eric Allender, Jacob Gray, Saachi Mutreja, Harsha Tirumala, and Pengxiang Wang. Robustness for Space-Bounded Statistical Zero Knowledge. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 56:1-56:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{allender_et_al:LIPIcs.APPROX/RANDOM.2023.56,
  author =	{Allender, Eric and Gray, Jacob and Mutreja, Saachi and Tirumala, Harsha and Wang, Pengxiang},
  title =	{{Robustness for Space-Bounded Statistical Zero Knowledge}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)},
  pages =	{56:1--56:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-296-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{275},
  editor =	{Megow, Nicole and Smith, Adam},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.56},
  URN =		{urn:nbn:de:0030-drops-188815},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2023.56},
  annote =	{Keywords: Interactive Proofs}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.22
Even Shorter Proofs Without New Variables

Authors: Adrián Rebola-Pardo

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

Abstract
Proof formats for SAT solvers have diversified over the last decade, enabling new features such as extended resolution-like capabilities, very general extension-free rules, inclusion of proof hints, and pseudo-boolean reasoning. Interference-based methods have been proven effective, and some theoretical work has been undertaken to better explain their limits and semantics. In this work, we combine the subsumption redundancy notion from [Sam Buss and Neil Thapen, 2019] and the overwrite logic framework from [Adrián Rebola{-}Pardo and Martin Suda, 2018]. Natural generalizations then become apparent, enabling even shorter proofs of the pigeonhole principle (compared to those from [Marijn J. H. Heule et al., 2017]) and smaller unsatisfiable core generation.
Cite as

Adrián Rebola-Pardo. Even Shorter Proofs Without New Variables. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{rebolapardo:LIPIcs.SAT.2023.22,
  author =	{Rebola-Pardo, Adri\'{a}n},
  title =	{{Even Shorter Proofs Without New Variables}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{22:1--22:20},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.22},
  URN =		{urn:nbn:de:0030-drops-184844},
  doi =		{10.4230/LIPIcs.SAT.2023.22},
  annote =	{Keywords: Interference, SAT solving, Unsatisfiability proofs, Unsatisfiable cores}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2023.3
Kolmogorov Complexity Characterizes Statistical Zero Knowledge

Authors: Eric Allender, Shuichi Hirahara, and Harsha Tirumala

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

Abstract
We show that a decidable promise problem has a non-interactive statistical zero-knowledge proof system if and only if it is randomly reducible via an honest polynomial-time reduction to a promise problem for Kolmogorov-random strings, with a superlogarithmic additive approximation term. This extends recent work by Saks and Santhanam (CCC 2022). We build on this to give new characterizations of Statistical Zero Knowledge SZK, as well as the related classes NISZK_L and SZK_L.
Cite as

Eric Allender, Shuichi Hirahara, and Harsha Tirumala. Kolmogorov Complexity Characterizes Statistical Zero Knowledge. In 14th Innovations in Theoretical Computer Science Conference (ITCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 251, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{allender_et_al:LIPIcs.ITCS.2023.3,
  author =	{Allender, Eric and Hirahara, Shuichi and Tirumala, Harsha},
  title =	{{Kolmogorov Complexity Characterizes Statistical Zero Knowledge}},
  booktitle =	{14th Innovations in Theoretical Computer Science Conference (ITCS 2023)},
  pages =	{3:1--3:19},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2023.3},
  URN =		{urn:nbn:de:0030-drops-175063},
  doi =		{10.4230/LIPIcs.ITCS.2023.3},
  annote =	{Keywords: Kolmogorov Complexity, Interactive Proofs}
}
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-dev.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.CSL.2020.12
Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs

Authors: Sam Buss, Anupam Das, and Alexander Knop

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs, deterministic or non-deterministic. Decision trees (DTs) are represented by a natural term syntax, inducing the system LDT, and non-determinism is modelled by including disjunction, ∨, as primitive (system LNDT). Branching programs generalise DTs to dag-like structures and are duly handled by extension variables in our setting, as is common in proof complexity (systems eLDT and eLNDT). Deterministic and non-deterministic branching programs are natural nonuniform analogues of log-space (L) and nondeterministic log-space (NL), respectively. Thus eLDT and eLNDT serve as natural systems of reasoning corresponding to L and NL, respectively. The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in LDT, LNDT, eLDT and eLNDT. We also compare them with Frege systems, constant-depth Frege systems and extended Frege systems.
Cite as

Sam Buss, Anupam Das, and Alexander Knop. Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{buss_et_al:LIPIcs.CSL.2020.12,
  author =	{Buss, Sam and Das, Anupam and Knop, Alexander},
  title =	{{Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.12},
  URN =		{urn:nbn:de:0030-drops-116553},
  doi =		{10.4230/LIPIcs.CSL.2020.12},
  annote =	{Keywords: proof complexity, decision trees, branching programs, logspace, sequent calculus, non-determinism, low-depth complexity}
}
Document
DOI: 10.4230/LIPIcs.CCC.2018.16
Reordering Rule Makes OBDD Proof Systems Stronger

Authors: Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov

Published in: LIPIcs, Volume 102, 33rd Computational Complexity Conference (CCC 2018)

Abstract
Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(^, weakening), simulates CP^* (Cutting Planes with unary coefficients). We show that OBDD(^, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring tautologies have polynomial size proofs in the OBDD(^, weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD(^, weakening, reordering) is strictly stronger than OBDD(^, weakening). This is proved using the Clique-Coloring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD(^) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolve an open question proposed by Groote and Zantema. Applying dag-like and tree-like lifting techniques to the mentioned results, we completely analyze which of the systems among CP^*, OBDD(^), OBDD(^, reordering), OBDD(^, weakening) and OBDD(^, weakening, reordering) polynomially simulate each other. For dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.
Cite as

Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering Rule Makes OBDD Proof Systems Stronger. In 33rd Computational Complexity Conference (CCC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 102, pp. 16:1-16:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{buss_et_al:LIPIcs.CCC.2018.16,
  author =	{Buss, Sam and Itsykson, Dmitry and Knop, Alexander and Sokolov, Dmitry},
  title =	{{Reordering Rule Makes OBDD Proof Systems Stronger}},
  booktitle =	{33rd Computational Complexity Conference (CCC 2018)},
  pages =	{16:1--16:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-069-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{102},
  editor =	{Servedio, Rocco A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2018.16},
  URN =		{urn:nbn:de:0030-drops-88720},
  doi =		{10.4230/LIPIcs.CCC.2018.16},
  annote =	{Keywords: Proof complexity, OBDD, Tseitin formulas, the Clique-Coloring principle, lifting theorems}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2017.31
Expander Construction in VNC1

Authors: Sam Buss, Valentine Kabanets, Antonina Kolokolova, and Michal Koucky

Published in: LIPIcs, Volume 67, 8th Innovations in Theoretical Computer Science Conference (ITCS 2017)

Abstract
We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson (2002), and show that this analysis can be formalized in the bounded arithmetic system VNC^1 (corresponding to the "NC^1 reasoning"). As a corollary, we prove the assumption made by Jerabek (2011) that a construction of certain bipartite expander graphs can be formalized in VNC^1. This in turn implies that every proof in Gentzen's sequent calculus LK of a monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlak (2002).
Cite as

Sam Buss, Valentine Kabanets, Antonina Kolokolova, and Michal Koucky. Expander Construction in VNC1. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 67, pp. 31:1-31:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{buss_et_al:LIPIcs.ITCS.2017.31,
  author =	{Buss, Sam and Kabanets, Valentine and Kolokolova, Antonina and Koucky, Michal},
  title =	{{Expander Construction in VNC1}},
  booktitle =	{8th Innovations in Theoretical Computer Science Conference (ITCS 2017)},
  pages =	{31:1--31:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-029-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{67},
  editor =	{Papadimitriou, Christos H.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2017.31},
  URN =		{urn:nbn:de:0030-drops-81871},
  doi =		{10.4230/LIPIcs.ITCS.2017.31},
  annote =	{Keywords: expander graphs, bounded arithmetic, alternating log time, sequent calculus, monotone propositional logic}
}
  • Refine by Author
  • 4 Buss, Sam
  • 2 Allender, Eric
  • 2 Knop, Alexander
  • 2 Tirumala, Harsha
  • 1 Das, Anupam
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Complexity classes
  • 2 Theory of computation → Computational complexity and cryptography
  • 2 Theory of computation → Proof complexity
  • 1 Hardware → Theorem proving and SAT solving
  • 1 Theory of computation → Circuit complexity

  • Refine by Keyword
  • 2 Interactive Proofs
  • 2 proof complexity
  • 2 sequent calculus
  • 1 Circuit Complexity
  • 1 Interference
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 4 2023
  • 1 2017
  • 1 2018
  • 1 2020
  • 1 2024

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