Resolution with counting: dag-like lower bounds and different moduli

DOI10.1007/s00037-020-00202-xOpenAlexW3119890049MaRDI QIDQ2029775

Fedor Part, Iddo Tzameret

Publication date: 4 June 2021

Published in: Computational Complexity (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1806.09383

zbMATH Keywords

lower boundsresolutionpolynomial calculusproof complexitypropositional pigeonhole principlelinear decision treesresolution over linear equationstseitin formulas

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20) Solving polynomial systems; resultants (13P15)

Related Items (3)

The power of the binary value principle ⋮ Depth lower bounds in Stabbing Planes for combinatorial principles ⋮ Propositional proof complexity

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exponential lower bounds for the pigeonhole principle
• Resolution over linear equations and multilinear proofs
• The intractability of resolution
• Ramanujan graphs
• Covering the cube by affine hyperplanes
• Hard examples for the bounded depth Frege proof system
• Essential covers of the cube by hyperplanes
• Resolution over linear equations modulo two
• A feasible interpolation for random resolution
• The relative efficiency of propositional proof systems
• Discretely ordered modules as a first-order extension of the cutting planes proof system
• Short proofs are narrow—resolution made simple
• On monotone circuits with local oracles and clique lower bounds
• Some Subsystems of Constant-Depth Frege with Parity
• Circuit Complexity, Proof Complexity, and Polynomial Identity Testing
• An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
• Proof Complexity Lower Bounds from Algebraic Circuit Complexity
• Linear gaps between degrees for the polynomial calculus modulo distinct primes

This page was built for publication: Resolution with counting: dag-like lower bounds and different moduli