Towards NP-P via proof complexity and search
From MaRDI portal
Publication:408544
DOI10.1016/j.apal.2011.09.009zbMath1257.03086MaRDI QIDQ408544
Publication date: 10 April 2012
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.2011.09.009
propositional logic; lower bounds; resolution; satisfiability; survey article; proof search; proof complexity
03D15: Complexity of computation (including implicit computational complexity)
03B05: Classical propositional logic
68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q15: Complexity classes (hierarchies, relations among complexity classes, etc.)
03F20: Complexity of proofs
Related Items
Unnamed Item, Unnamed Item, A note on SAT algorithms and proof complexity, Relating size and width in variants of Q-resolution, Understanding cutting planes for QBFs, A game characterisation of tree-like Q-resolution size, A Game Characterisation of Tree-like Q-resolution Size
Uses Software
Cites Work
- Disjointness is hard in the multiparty number-on-the-forehead model
- Random CNF's are hard for the polynomial calculus
- Exponential lower bounds for the pigeonhole principle
- On optimal heuristic randomized semidecision procedures, with applications to proof complexity and cryptography
- A lower bound for intuitionistic logic
- On lengths of proofs in non-classical logics
- On the hardness of approximating label-cover
- The intractability of resolution
- Solving satisfiability in less than \(2^ n\) steps
- The monotone circuit complexity of Boolean functions
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- Propositional consistency proofs
- Linearizing intuitionistic implication
- Lower bounds for the polynomial calculus
- The complexity of Horn fragments of linear logic
- A probabilistic algorithm for \(k\)-SAT based on limited local search and restart
- Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
- Optimal proof systems imply complete sets for promise classes
- Resolution lower bounds for the weak functional pigeonhole principle.
- Which problems have strongly exponential complexity?
- Non-automatizability of bounded-depth Frege proofs
- Resolution lower bounds for perfect matching principles
- On the automatizability of polynomial calculus
- Lower bounds for the polynomial calculus and the Gröbner basis algorithm
- On the complexity of the reflected logic of proofs
- Lambek calculus is NP-complete
- BerkMin: A fast and robust SAT-solver
- Minimum propositional proof length is NP-hard to linearly approximate
- On the weak pigeonhole principle
- The independence of the modulo p counting principles
- An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
- Exponential Lower Bounds and Integrality Gaps for Tree-Like Lovász–Schrijver Procedures
- Resolution Is Not Automatizable Unless W[P Is Tractable]
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- Many hard examples for resolution
- Twelve Problems in Proof Complexity
- Lower Bounds for Lovász–Schrijver Systems and Beyond Follow from Multiparty Communication Complexity
- An improved exponential-time algorithm for k -SAT
- An exponential separation between regular and general resolution
- Resolution lower bounds for the weak pigeonhole principle
- The NP-Completeness of Reflected Fragments of Justification Logics
- Product-Free Lambek Calculus Is NP-Complete
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
- An overview of computational complexity
- Polynomial size proofs of the propositional pigeonhole principle
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- Lower bounds to the size of constant-depth propositional proofs
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- On Interpolation and Automatization for Frege Systems
- GRASP: a search algorithm for propositional satisfiability
- An algorithm for the satisfiability problem of formulas in conjunctive normal form
- An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
- Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic
- Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
- Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds
- An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
- Lower bounds for modal logics
- The Complexity of Propositional Proofs
- 3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- The complexity of theorem-proving procedures
- Exponential Lower Bounds on the Lengths of Some Classes of Branch-and-Cut Proofs
- Principles and Practice of Constraint Programming – CP 2004
- Natural proofs
- Linear gaps between degrees for the polynomial calculus modulo distinct primes
- On the complexity of \(k\)-SAT
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
