Short propositional refutations for dense random 3CNF formulas
From MaRDI portal
Publication:741088
DOI10.1016/j.apal.2014.08.001zbMath1391.03042OpenAlexW2950542447MaRDI QIDQ741088
Publication date: 10 September 2014
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.2014.08.001
Analysis of algorithms and problem complexity (68Q25) Complexity of computation (including implicit computational complexity) (03D15) First-order arithmetic and fragments (03F30) Classical propositional logic (03B05) Complexity of proofs (03F20)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Random CNF's are hard for the polynomial calculus
- The intractability of resolution
- Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
- The proof complexity of linear algebra
- Dual weak pigeonhole principle, Boolean complexity, and derandomization
- Cutting planes, connectivity, and threshold logic
- On the weak pigeonhole principle
- The Efficiency of Resolution and Davis--Putnam Procedures
- Optimality of size-degree tradeoffs for polynomial calculus
- Short Propositional Refutations for Dense Random 3CNF Formulas
- ON THE PROOF COMPLEXITY OF THE NISAN–WIGDERSON GENERATOR BASED ON A HARD NP ∩ coNP FUNCTION
- Resolution Is Not Automatizable Unless W[P Is Tractable]
- Recognizing more random unsatisfiable 3-SAT instances efficiently
- Many hard examples for resolution
- Proving Infinitude of Prime Numbers Using Binomial Coefficients
- Lower bounds for k-DNF resolution on random 3-CNFs
- Matrix Analysis
- The relative efficiency of propositional proof systems
- Lower bounds to the size of constant-depth propositional proofs
- Short proofs are narrow—resolution made simple
- On Interpolation and Automatization for Frege Systems
- A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
- Sparser Random 3-SAT Refutation Algorithms and the Interpolation Problem
- Theories for TC0 and Other Small Complexity Classes
- Short proofs for the determinant identities
- Recognizing More Unsatisfiable Random k-SAT Instances Efficiently
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Notes on polynomially bounded arithmetic
This page was built for publication: Short propositional refutations for dense random 3CNF formulas
