Document Open Access Logo

Tropical Proof Systems: Between R(CP) and Resolution

Authors Yaroslav Alekseev , Dima Grigoriev, Edward A. Hirsch

PDF
Thumbnail PDF

File

LIPIcs.STACS.2025.8.pdf
  • Filesize: 0.85 MB
  • 20 pages

Document Identifiers

Author Details

Yaroslav Alekseev
  • Technion - Israel Institute of Technology, Haifa, Israel
Dima Grigoriev
  • CNRS, Mathématique, Université de Lille, Villeneuve d'Ascq, 59655, France
Edward A. Hirsch
  • Department of Computer Science, Ariel University, Israel

Funding

  • Hirsch, Edward A.: This research was conducted with the support of the State of Israel, the Ministry of Immigrant Absorption, and the Center for the Absorption of Scientists.

Acknowledgements

The authors are very grateful to Dmitry Itsykson and Dmitry Sokolov for fruitful discussions, and to Marc Vinyals for his inspiring Proof Complexity Zoo project and for pointing to the recent work of Gläser and Pfetsch.

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.STACS.2025.8

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Cutting Planes
  • Nullstellensatz refutations
  • Res(CP)
  • semi-algebraic proofs
  • tropical proof systems
  • tropical semiring

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Marianne Akian, Antoine Béreau, and Stéphane Gaubert. The tropical Nullstellensatz and Positivstellensatz for sparse polynomial systems. In Proc. ACM Intern. Symp. Symb. Algebr. Comput., pages 43-52, 2023. URL: https://doi.org/10.1145/3597066.3597089.
  2. Marianne Akian, Stéphane Gaubert, and Alexander Guterman. The correspondence between tropical convexity and mean payoff games. In 19 Intern. Symp. Math. Theory of Networks and Systems, Budapest, pages 1295-1302, 2012. Google Scholar
  3. Yaroslav Alekseev, Dima Grigoriev, and Edward A. Hirsch. Tropical proof systems. Electron. Colloquium Comput. Complex., TR24-072, 2024. URL: https://eccc.weizmann.ac.il/report/2024/072.
  4. Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, and Iddo Tzameret. Semialgebraic proofs, IPS lower bounds, and the τ-conjecture: Can a natural number be negative? SIAM Journal on Computing, 53(3):648-700, 2024. URL: https://doi.org/10.1137/20M1374523.
  5. Xavier Allamigeon, Uli Fahrenberg, Stéphane Gaubert, Ricardo D. Katz, and Axel Legay. Tropical Fourier-Motzkin elimination, with an application to real-time verification. Int. J. Algebra Comput., 24(5):569-607, 2014. URL: https://doi.org/10.1142/S0218196714500258.
  6. Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing Planes. In Anna R. Karlin, editor, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018), volume 94 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:20, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITCS.2018.10.
  7. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc., 73(3):1-26, 1996. URL: https://doi.org/10.1112/plms/s3-73.1.1.
  8. Aaron Bertram and Robert Easton. The tropical Nullstellensatz for congruences. Adv. Math, 308:36-82, 2017. Google Scholar
  9. Peter Butkovic. Max-linear systems: theory and algorithms. Springer, 2010. Google Scholar
  10. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on the Theory of Computing, pages 174-183, New York, 1996. URL: https://doi.org/10.1145/237814.237860.
  11. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  12. W. Cook, C.R. Coullard, and Gy. Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  13. Klim Efremenko, Michal Garlik, and Dmitry Itsykson. Lower bounds for regular resolution over parities. ECCC TR23-187, 2023. Google Scholar
  14. 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 Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021, July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 6:1-6:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CCC.2021.6.
  15. Max Gläser and Marc E. Pfetsch. Sub-exponential lower bounds for branch-and-bound with general disjunctions via interpolation. Technical Report 2308.04320, arXiv, 2023. Google Scholar
  16. Dima Grigoriev. Complexity of solving tropical linear systems. Comput. Complexity, 22:71-88, 2013. URL: https://doi.org/10.1007/S00037-012-0053-5.
  17. Dima Grigoriev and Vladimir V. Podolskii. Tropical effective primary and dual Nullstellensätze. Discrete and Computational Geometry, 59(3):507-552, 2018. URL: https://doi.org/10.1007/s00454-018-9966-3.
  18. Armin Haken. The intractability of resolution. Theoret. Comput. Sci., 39(2-3):297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  19. Edward A. Hirsch and Arist Kojevnikov. Several notes on the power of Gomory-Chvátal cuts. Ann. Pure Appl. Log., 141(3):429-436, 2006. URL: https://doi.org/10.1016/j.apal.2005.12.006.
  20. Dmitry Itsykson and Dmitry Sokolov. Resolution over linear equations modulo two. Ann. Pure Appl. Log., 171(1), 2020. URL: https://doi.org/10.1016/J.APAL.2019.102722.
  21. Daniel Joo and Kalina Mincheva. Prime congruences of additively idempotent semirings and a Nullstellensatz for tropical polynomials. Selecta Math., 24:2207-2233, 2018. Google Scholar
  22. Stasys Jukna. Boolean Function Complexity. Springer, 2012. Google Scholar
  23. Jan Krajícek. Discretely ordered modules as a first-order extension of the cutting planes proof system. J. Symb. Log., 63(4):1582-1596, 1998. URL: https://doi.org/10.2307/2586668.
  24. Jan Krajícek. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-3):123-140, 2001. Google Scholar
  25. Jan Krajíček. Proof Complexity. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2019. Google Scholar
  26. Diane Maclagan and Felipe Rincon. Tropical ideals. Compos. Math., 154:640-670, 2018. Google Scholar
  27. Diane Maclagan and Bernd Sturmfels. Introduction to Tropical Geometry. Springer, 2015. Google Scholar
  28. Fedor Part and Iddo Tzameret. Resolution with counting: Dag-like lower bounds and different moduli. Comput. Complex., 30(1):2, 2021. URL: https://doi.org/10.1007/S00037-020-00202-X.
  29. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, 1997. URL: http://www.jstor.org/stable/2275583, URL: https://doi.org/10.2307/2275583.
  30. Ran Raz and Iddo Tzameret. Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Logic, 155(3):194-224, 2008. URL: https://doi.org/10.1016/j.apal.2008.04.001.
  31. Grigori Tseitin. On the complexity of derivations in propositional calculus. In Studies in constructive mathematics and mathematical logic. Part II, pages 115-125. Consultants Bureau, New-York-London, 1968. Google Scholar
  32. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. URL: https://doi.org/10.1145/7531.8928.
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 About DROPS Imprint Privacy Contact