Short proofs are narrow -- resolution made simple

DOI10.1145/301250.301392MaRDI QIDQ2819584zbMATH OpenOpenAlexFDO

Authors Eli Ben-Sasson, A. Wigderson

Publication date 29 September 2016

Published in Proceedings of the thirty-first annual ACM symposium on Theory of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/301250.301392

Mathematics Subject Classification ID

Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Short proofs are narrow—resolution made simple
• From small space to small width in resolution
• Theory and Applications of Models of Computation
• Width versus size in resolution proofs
• Near optimal seperation of tree-like and general resolution

Cited in

(40)

• The intractability of resolution
• Resolution and binary decision diagrams cannot simulate each other polynomially
• Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
• A complexity gap for tree resolution
• Relating size and width in variants of Q-resolution
• Cliques enumeration and tree-like resolution proofs
• Space bounds for resolution
• On the automatizability of resolution and related propositional proof systems
• Mutilated chessboard problem is exponentially hard for resolution
• On a generalization of extended resolution
• Andrews Skolemization may shorten resolution proofs non-elementarily
• Width versus size in resolution proofs
• The complexity of properly learning simple concept classes
• Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width
• An upper bound for resolution size: characterization of tractable SAT instances
• A dichotomy for local small-bias generators
• Relativisation Provides Natural Separations for Resolution-Based Proof Systems
• Cutting planes and the parameter cutwidth
• Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities
• Short proofs are narrow—resolution made simple
• scientific article; zbMATH DE number 1948187 (Why is no real title available?)
• scientific article; zbMATH DE number 1948189 (Why is no real title available?)
• Space complexity of random formulae in resolution
• Are Short Proofs Narrow? QBF Resolution is not Simple.
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple
• scientific article; zbMATH DE number 1361471 (Why is no real title available?)
• Lifting lower bounds for tree-like proofs
• scientific article; zbMATH DE number 938516 (Why is no real title available?)
• On exponential lower bounds for partially ordered resolution
• On linear resolution
• Short Proofs Are Hard to Find
• Resolution and the binary encoding of combinatorial principles
• scientific article; zbMATH DE number 7300350 (Why is no real title available?)
• The proof-search problem between bounded-width resolution and bounded-degree semi-algebraic proofs
• A Resolution Calculus for Shortening Proofs
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Models of Computation
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Supercritical size-width tree-like resolution trade-offs for graph isomorphism

This page was built for publication: Short proofs are narrow -- resolution made simple

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819584)