Search Results

Documents authored by Hirsch, Edward A.

Document
DOI: 10.4230/LIPIcs.STACS.2025.8
Tropical Proof Systems: Between R(CP) and Resolution

Authors: Yaroslav Alekseev, Dima Grigoriev, and Edward A. Hirsch

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
Propositional proof complexity deals with the lengths of polynomial-time verifiable proofs for Boolean tautologies. An abundance of proof systems is known, including algebraic and semialgebraic systems, which work with polynomial equations and inequalities, respectively. The most basic algebraic proof system is based on Hilbert’s Nullstellensatz [Paul Beame et al., 1996]. Tropical ("min-plus") arithmetic has many applications in various areas of mathematics. The operations are the real addition (as the tropical multiplication) and the minimum (as the tropical addition). Recently, [Bertram and Easton, 2017; Dima Grigoriev and Vladimir V. Podolskii, 2018; Joo and Mincheva, 2018] demonstrated a version of Nullstellensatz in the tropical setting. In this paper we introduce (semi)algebraic proof systems that use min-plus arithmetic. For the dual-variable encoding of Boolean variables (two tropical variables x and x ̅ per one Boolean variable x) and {0,1}-encoding of the truth values, we prove that a static (Nullstellensatz-based) tropical proof system polynomially simulates daglike resolution and also has short proofs for the propositional pigeon-hole principle. Its dynamic version strengthened by an additional derivation rule (a tropical analogue of resolution by linear inequality) is equivalent to the system Res(LP) (aka R(LP)), which derives nonnegative linear combinations of linear inequalities; this latter system is known to polynomially simulate Krajíček’s Res(CP) (aka R(CP)) with unary coefficients. Therefore, tropical proof systems give a finer hierarchy of proof systems below Res(LP) for which we still do not have exponential lower bounds. While the "driving force" in Res(LP) is resolution by linear inequalities, dynamic tropical systems are driven solely by the transitivity of the order, and static tropical proof systems are based on reasoning about differences between the input linear functions. For the truth values encoded by {0,∞}, dynamic tropical proofs are equivalent to Res(∞), which is a small-depth Frege system called also DNF resolution. Finally, we provide a lower bound on the size of derivations of a much simplified tropical version of the {Binary Value Principle} in a static tropical proof system. Also, we establish the non-deducibility of the tropical resolution rule in this system and discuss axioms for Boolean logic that do not use dual variables. In this extended abstract, full proofs are omitted.
Cite as

Yaroslav Alekseev, Dima Grigoriev, and Edward A. Hirsch. Tropical Proof Systems: Between R(CP) and Resolution. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{alekseev_et_al:LIPIcs.STACS.2025.8,
  author =	{Alekseev, Yaroslav and Grigoriev, Dima and Hirsch, Edward A.},
  title =	{{Tropical Proof Systems: Between R(CP) and Resolution}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.8},
  URN =		{urn:nbn:de:0030-drops-228332},
  doi =		{10.4230/LIPIcs.STACS.2025.8},
  annote =	{Keywords: Cutting Planes, Nullstellensatz refutations, Res(CP), semi-algebraic proofs, tropical proof systems, tropical semiring}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2024.48
Proving Unsatisfiability with Hitting Formulas

Authors: Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)

Abstract
A hitting formula is a set of Boolean clauses such that any two of the clauses cannot be simultaneously falsified. Hitting formulas have been studied in many different contexts at least since [Iwama, 1989] and, based on experimental evidence, Peitl and Szeider [Tomás Peitl and Stefan Szeider, 2022] conjectured that unsatisfiable hitting formulas are among the hardest for resolution. Using the fact that hitting formulas are easy to check for satisfiability we make them the foundation of a new static proof system {{rmHitting}}: a refutation of a CNF in {{rmHitting}} is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. Our first result is that {{rmHitting}} is quasi-polynomially simulated by tree-like resolution, which means that hitting formulas cannot be exponentially hard for resolution and partially refutes the conjecture of Peitl and Szeider. We show that tree-like resolution and {{rmHitting}} are quasi-polynomially separated, while for resolution, this question remains open. For a system that is only quasi-polynomially stronger than tree-like resolution, {{rmHitting}} is surprisingly difficult to polynomially simulate in another proof system. Using the ideas of Raz-Shpilka’s polynomial identity testing for noncommutative circuits [Raz and Shpilka, 2005] we show that {{rmHitting}} is p-simulated by {{rmExtended {{rmFrege}}}}, but we conjecture that much more efficient simulations exist. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in deterministic polynomial time. We consider multiple extensions of {{rmHitting}}, and in particular a proof system {{{rmHitting}}(⊕)} related to the {{{rmRes}}(⊕)} proof system for which no superpolynomial-size lower bounds are known. {{{rmHitting}}(⊕)} p-simulates the tree-like version of {{{rmRes}}(⊕)} and is at least quasi-polynomially stronger. We show that formulas expressing the non-existence of perfect matchings in the graphs K_{n,n+2} are exponentially hard for {{{rmHitting}}(⊕)} via a reduction to the partition bound for communication complexity. See the full version of the paper for the proofs. They are omitted in this Extended Abstract.
Cite as

Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.ITCS.2024.48,
  author =	{Filmus, Yuval and Hirsch, Edward A. and Riazanov, Artur and Smal, Alexander and Vinyals, Marc},
  title =	{{Proving Unsatisfiability with Hitting Formulas}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{48:1--48:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.48},
  URN =		{urn:nbn:de:0030-drops-195762},
  doi =		{10.4230/LIPIcs.ITCS.2024.48},
  annote =	{Keywords: hitting formulas, polynomial identity testing, query complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.46
On the Limits of Gate Elimination

Authors: Alexander Golovnev, Edward A. Hirsch, Alexander Knop, and Alexander S. Kulikov

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
Although a simple counting argument shows the existence of Boolean functions of exponential circuit complexity, proving superlinear circuit lower bounds for explicit functions seems to be out of reach of the current techniques. There has been a (very slow) progress in proving linear lower bounds with the latest record of 3 1/86*n-o(n). All known lower bounds are based on the so-called gate elimination technique. A typical gate elimination argument shows that it is possible to eliminate several gates from an optimal circuit by making one or several substitutions to the input variables and repeats this inductively. In this note we prove that this method cannot achieve linear bounds of cn beyond a certain constant c, where c depends only on the number of substitutions made at a single step of the induction.
Cite as

Alexander Golovnev, Edward A. Hirsch, Alexander Knop, and Alexander S. Kulikov. On the Limits of Gate Elimination. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 46:1-46:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{golovnev_et_al:LIPIcs.MFCS.2016.46,
  author =	{Golovnev, Alexander and Hirsch, Edward A. and Knop, Alexander and Kulikov, Alexander S.},
  title =	{{On the Limits of Gate Elimination}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{46:1--46:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.46},
  URN =		{urn:nbn:de:0030-drops-64593},
  doi =		{10.4230/LIPIcs.MFCS.2016.46},
  annote =	{Keywords: circuit complexity, lower bounds, gate elimination}
}
Document
DOI: 10.4230/DagRep.4.10.51
Optimal algorithms and proofs (Dagstuhl Seminar 14421)

Authors: Olaf Beyersdorff, Edward A. Hirsch, Jan Krajicek, and Rahul Santhanam

Published in: Dagstuhl Reports, Volume 4, Issue 10 (2015)

Abstract
This report documents the programme and the outcomes of the Dagstuhl Seminar 14421 "Optimal algorithms and proofs". The seminar brought together researchers working in computational and proof complexity, logic, and the theory of approximations. Each of these areas has its own, but connected notion of optimality; and the main aim of the seminar was to bring together researchers from these different areas, for an exchange of ideas, techniques, and open questions, thereby triggering new research collaborations across established research boundaries.
Cite as

Olaf Beyersdorff, Edward A. Hirsch, Jan Krajicek, and Rahul Santhanam. Optimal algorithms and proofs (Dagstuhl Seminar 14421). In Dagstuhl Reports, Volume 4, Issue 10, pp. 51-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.4.10.51,
  author =	{Beyersdorff, Olaf and Hirsch, Edward A. and Krajicek, Jan and Santhanam, Rahul},
  title =	{{Optimal algorithms and proofs (Dagstuhl Seminar 14421)}},
  pages =	{51--68},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{10},
  editor =	{Beyersdorff, Olaf and Hirsch, Edward A. and Krajicek, Jan and Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.10.51},
  URN =		{urn:nbn:de:0030-drops-48923},
  doi =		{10.4230/DagRep.4.10.51},
  annote =	{Keywords: computational complexity, proof complexity, approximation algorithms, optimal algorithms, optimal proof systems, speedup theorems}
}
Document
DOI: 10.4230/LIPIcs.STACS.2010.2475
On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity

Authors: Edward A. Hirsch and Dmitry Itsykson

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
The existence of a ($p$-)optimal propositional proof system is a major open question in (proof) complexity; many people conjecture that such systems do not exist. Kraj\'{\i}\v{c}ek and Pudl\'{a}k \cite{KP} show that this question is equivalent to the existence of an algorithm that is optimal\footnote{Recent papers \cite{Monroe} call such algorithms \emph{$p$-optimal} while traditionally Levin's algorithm was called \emph{optimal}. We follow the older tradition. Also there is some mess in terminology here, thus please see formal definitions in Sect.~\ref{sec:prelim} below.} on all propositional tautologies. Monroe \cite{Monroe} recently gave a conjecture implying that such algorithm does not exist. We show that in the presence of errors such optimal algorithms \emph{do} exist. The concept is motivated by the notion of heuristic algorithms. Namely, we allow the algorithm to claim a small number of false ``theorems'' (according to any polynomial-time samplable distribution on non-tautologies) and err with bounded probability on other inputs. Our result can also be viewed as the existence of an optimal proof system in a class of proof systems obtained by generalizing automatizable proof systems.
Cite as

Edward A. Hirsch and Dmitry Itsykson. On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 453-464, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{hirsch_et_al:LIPIcs.STACS.2010.2475,
  author =	{Hirsch, Edward A. and Itsykson, Dmitry},
  title =	{{On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{453--464},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2475},
  URN =		{urn:nbn:de:0030-drops-24753},
  doi =		{10.4230/LIPIcs.STACS.2010.2475},
  annote =	{Keywords: Propositional proof complexity, optimal algorithm}
}
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact