Lukáš Folwarczný
Abstract
Dag-like communication protocols, a generalization of the classical tree-like communication protocols, are useful objects in the realm of proof complexity (most importantly for monotone feasible interpolation) and circuit complexity. We consider three kinds of protocols in this article (d is the degree of a protocol):
— | IEQ-d-dags: feasible sets of these protocols are described by inequality which means that the feasible sets are combinatorial triangles; these protocols are also called triangle-dags in the literature, | ||||
— | EQ-d-dags: feasible sets are described by equality, and | ||||
— | c-IEQ-d-dags: feasible sets are described by a conjunction of c inequalities. | ||||
As our main contribution, we prove the following statement: EQ-2-dags can efficiently simulate c-IEQ-d-dags when c and d are constants. This implies that EQ-2-dags are at least as strong as IEQ-d-dags and that EQ-2-dags have the same strength as c-IEQ-d-dags for c ≥ 2 (because 2-IEQ-2-dags can trivially simulate EQ-2-dags).
Hrubeš and Pudlák (Information Processing Letters, 2018) proved that IEQ-d-dags over the monotone Karchmer-Wigderson relation are equivalent to monotone real circuits which implies that we have exponential lower bounds for these protocols. Lower bounds for EQ-2-dags would directly imply lower bounds for the proof system R(LIN).
- [1] . 2007. Lower bounds for Lovász–Schrijver systems and beyond follow from multiparty communication complexity. SIAM Journal on Computing 37, 3 (2007), 845–869.
DOI: Google Scholar
Cross Ref
- [2] . 2019. Representations of monotone boolean functions by linear programs. ACM Transactions on Computing Theory 11, 4 (2019), 22:1–22:31.
DOI: Google ScholarDigital Library
- [3] . 2022. Guest column: Proofs, circuits, and communication. SIGACT News 53, 1 (2022), 59–82.
DOI: Google ScholarDigital Library - [4] . 2020. Monotone circuit lower bounds from resolution. Theory of Computing 16, 13 (2020), 1--30. https://theoryofcomputing.org/articles/v016a013/v016a013.pdf.Google ScholarCross Ref
- [5] . 1992. A simple lower bound for monotone clique using a communication game. Information Processing Letters 41, 4 (1992), 221–226.
DOI: Google ScholarDigital Library - [6] . 2019. Adventures in monotone complexity and TFNP. In Proceedings of the 10th Innovations in Theoretical Computer Science Conference, (Ed.), Vol. 124. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 38:1–38:19.
DOI: Google ScholarCross Ref - [7] . 2018. Communication lower bounds via critical block sensitivity. SIAM Journal on Computing 47, 5 (2018), 1778–1806.
DOI: Google ScholarDigital Library - [8] . 1999. An exponential lower bound for the size of monotone real circuits. Journal of Computer and System Sciences 58, 2 (1999), 326–335.
DOI: Google ScholarDigital Library - [9] . 2018. A note on monotone real circuits. Information Processing Letters 131, 3 (2018), 15–19. https://www.sciencedirect.com/science/article/abs/pii/S0020019017301965.Google ScholarCross Ref
- [10] . 2020. Resolution over linear equations modulo two. Annals of Pure and Applied Logic 171, 1 (2020), 102722.
DOI: Google ScholarCross Ref - [11] . 1988. Monotone circuits for connectivity require super-logarithmic depth. In Proceedings of the 20th Annual ACM Symposium on Theory of Computing, (Ed.). ACM, 539–550.
DOI: Google ScholarDigital Library - [12] . 2018. Randomized feasible interpolation and monotone circuits with a local oracle. Journal of Mathematical Logic 18, 2 (2018), 1850012.
DOI: Google ScholarCross Ref - [13] . 1994. Lower bounds to the size of constant-depth propositional proofs. The Journal of Symbolic Logic 59, 1 (1994), 73–86.
DOI: Google ScholarDigital Library - [14] . 1997. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic 62, 2 (1997), 457–486.
DOI: Google ScholarCross Ref - [15] . 1998. Interpolation by a game. Mathematical Logic Quarterly 44, 4 (1998), 450–458.
DOI: Google ScholarCross Ref - [16] . 2018. On monotone circuits with local oracles and clique lower bounds. Chicago Journal of Theoretical Computer Science 2018, 1 (2018), 1--18. http://cjtcs.cs.uchicago.edu/articles/2018/1/cj18-01.pdf.Google ScholarCross Ref
- [17] . 2019. Proof Complexity. Cambridge University Press.Google ScholarCross Ref
- [18] . 2017. Strongly exponential lower bounds for monotone computation. In Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, , , and (Eds.). ACM, 1246–1255.
DOI: Google ScholarDigital Library - [19] . 1997. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic 62, 3 (1997), 981–998.
DOI: Google ScholarCross Ref - [20] . 2010. On extracting computations from propositional proofs (a survey). In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, and (Eds.), Vol. 8. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 30–41.
DOI: Google ScholarCross Ref - [21] . 1996. Algebraic models of computation and interpolation for algebraic proof systems. In Proceedings of the DIMACS Workshop Proof Complexity and Feasible Arithmetics, (DIMACS Series in Discrete Mathematics and Theoretical Computer Science), and (Eds.), Vol. 39. DIMACS/AMS, 279–295.
DOI: Google ScholarCross Ref - [22] . 2008. Resolution over linear equations and multilinear proofs. Annals of Pure and Applied Logic 155, 3 (2008), 194–224.
DOI: Google ScholarCross Ref - [23] . 1992. Monotone circuits for matching require linear depth. Journal of the ACM 39, 3 (1992), 736–744.
DOI: Google ScholarDigital Library - [24] . 1995. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izv. Ross. Akad. Nauk Ser. Mathematics 59, 1 (1995), 201–224.
DOI: Google ScholarCross Ref - [25] . 2016. Guest column: Proof complexity and beyond. SIGACT News 47, 2 (2016), 66–86.
DOI: Google ScholarDigital Library - [26] . 2016. Exponential lower bounds for monotone span programs. In Proceedings of the IEEE 57th Annual Symposium on Foundations of Computer Science, (Ed.). IEEE Computer Society, 406–415.
DOI: Google ScholarCross Ref - [27] . 1997. Monotone real circuits are more powerful than monotone boolean circuits. Information Processing Letters 61, 3 (1997), 161–164.
DOI: Google ScholarDigital Library - [28] . 2017. Dag-like communication and its applications. In Proceedings of the 12th International Computer Science Symposium in Russia Computer Science - Theory and Applications
Lecture Notes in Computer Science , (Ed.), Vol. 10304. Springer, 294–307.DOI: Google ScholarCross Ref - [29] . 1988. The gap between monotone and non-monotone circuit complexity is exponential. Combinatorica 8, 1 (1988), 141–142.
DOI: Google ScholarCross Ref
Index Terms
- On Protocols for Monotone Feasible Interpolation
Recommendations
Small Depth Proof Systems
A proof system for a language L is a function f such that Range(f) is exactly L. In this article, we look at proof systems from a circuit complexity point of view and study proof systems that are computationally very restricted. The restriction we study ...
Verifying proofs in constant depth
In this paper we initiate the study of proof systems where verification of proofs proceeds by NC0 circuits. We investigate the question which languages admit proof systems in this very restricted model. Formulated alternatively, we ask which languages ...
Monotone circuit lower bounds from resolution
STOC 2018: Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of ComputingFor any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, we show that a gadget-composed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocols—or, equivalently, ...
Comments