Bounded-depth Frege complexity of Tseitin formulas for all graphs
From MaRDI portal
Publication:2084956
DOI10.1016/j.apal.2022.103166OpenAlexW2946966057WikidataQ113880321 ScholiaQ113880321MaRDI QIDQ2084956
Nicola Galesi, Anastasia Sofronova, Artur Riazanov, Dmitry Itsykson
Publication date: 14 October 2022
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2022.103166
Graph minors (05C83) Classical propositional logic (03B05) Complexity of proofs (03F20) Parameterized complexity, tractability and kernelization (68Q27)
Cites Work
- Unnamed Item
- Satisfiability, branch-width and Tseitin tautologies
- Boolean function complexity. Advances and frontiers.
- Exponential lower bounds for the pigeonhole principle
- The treewidth of line graphs
- On tree-partition-width
- The intractability of resolution
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- Quickly excluding a planar graph
- The complexity of the pigeonhole principle
- Simplified lower bounds for propositional proofs
- Resolution lower bounds for the weak functional pigeonhole principle.
- Hard examples for the bounded depth Frege proof system
- Cops-robber games and the resolution of Tseitin formulas
- A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
- Resolution lower bounds for perfect matching principles
- An exponential separation between the parity principle and the pigeonhole principle
- Improved bounds on the planar branchwidth with respect to the largest grid minor size
- Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
- On Tseitin formulas, read-once branching programs and treewidth
- Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space
- A Structure Theorem for Strong Immersions
- Excluded Grid Theorem
- Parity, circuits, and the polynomial-time hierarchy
- Resolution Is Not Automatizable Unless W[P Is Tractable]
- Polynomial size proofs of the propositional pigeonhole principle
- Hard examples for resolution
- Approximation and Small-Depth Frege Proofs
- The relative efficiency of propositional proof systems
- Short proofs are narrow—resolution made simple
- An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
- Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP
- Tight Lower Bounds on the Resolution Complexity of Perfect Matching Principles
- Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs
- Automating Resolution is NP-Hard
- Towards Tight(er) Bounds for the Excluded Grid Theorem
- Poly-logarithmic Frege depth lower bounds via an expander switching lemma
- Resolution lower bounds for the weak pigeonhole principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
This page was built for publication: Bounded-depth Frege complexity of Tseitin formulas for all graphs
