Towards NP-P via proof complexity and search
From MaRDI portal
Publication:408544
DOI10.1016/J.APAL.2011.09.009zbMATH Open1257.03086OpenAlexW2202163874MaRDI QIDQ408544FDOQ408544
Authors: Samuel R. Buss 
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
Recommendations
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Classical propositional logic (03B05) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20) Complexity of computation (including implicit computational complexity) (03D15)
Cites Work
- BerkMin: A fast and robust SAT-solver
- Title not available (Why is that?)
- Which problems have strongly exponential complexity?
- Lambek calculus is NP-complete
- On the possibility of faster \textsc{SAT} algorithms
- The complexity of theorem-proving procedures
- Title not available (Why is that?)
- On the complexity of \(k\)-SAT
- Hard examples for resolution
- Title not available (Why is that?)
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- GRASP: a search algorithm for propositional satisfiability
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- The relative efficiency of propositional proof systems
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- The monotone circuit complexity of Boolean functions
- Title not available (Why is that?)
- Solving satisfiability in less than \(2^ n\) steps
- Many hard examples for resolution
- An algorithm for the satisfiability problem of formulas in conjunctive normal form
- Disjointness is hard in the multiparty number-on-the-forehead model
- Natural proofs
- A probabilistic algorithm for \(k\)-SAT based on limited local search and restart
- On lengths of proofs in non-classical logics
- Title not available (Why is that?)
- Lower bounds for modal logics
- A lower bound for intuitionistic logic
- An improved exponential-time algorithm for k -SAT
- 3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General
- The intractability of resolution
- Title not available (Why is that?)
- Improving PPSZ for 3-SAT using critical variables
- Title not available (Why is that?)
- Title not available (Why is that?)
- Linearizing intuitionistic implication
- On the complexity of the reflected logic of proofs
- On the hardness of approximating label-cover
- Propositional consistency proofs
- Lower bounds for the polynomial calculus
- The complexity of Horn fragments of linear logic
- 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.
- 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
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Resolution Is Not Automatizable Unless W[P] Is Tractable
- Title not available (Why is that?)
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- Twelve Problems in Proof Complexity
- Lower Bounds for Lovász–Schrijver Systems and Beyond Follow from Multiparty Communication Complexity
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- An overview of computational complexity
- Title not available (Why is that?)
- Polynomial size proofs of the propositional pigeonhole principle
- Title not available (Why is that?)
- Lower bounds to the size of constant-depth propositional proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- On Interpolation and Automatization for Frege Systems
- A Note on Conservativity Relations among Bounded Arithmetic Theories
- A proof complexity generator
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- The Complexity of Propositional Proofs
- Title not available (Why is that?)
- Exponential Lower Bounds on the Lengths of Some Classes of Branch-and-Cut Proofs
- Principles and Practice of Constraint Programming – CP 2004
- Linear gaps between degrees for the polynomial calculus modulo distinct primes
- 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
Cited In (27)
- Lower bound techniques for QBF expansion
- Title not available (Why is that?)
- Proof complexity of modal resolution
- ON THE PROOF COMPLEXITY OF THE NISAN–WIGDERSON GENERATOR BASED ON A HARD NP ∩ coNP FUNCTION
- Constructing NP-intermediate problems by blowing holes with parameters of various properties
- Proof complexity of monotone branching programs
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- A note on SAT algorithms and proof complexity
- An Introduction to Lower Bounds on Resolution Proof Systems
- Building strategies into QBF proofs
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- A game characterisation of tree-like Q-resolution size
- Relating size and width in variants of Q-resolution
- Automata, Languages and Programming
- Understanding cutting planes for QBFs
- A (biased) proof complexity survey for SAT practitioners
- Title not available (Why is that?)
- Characterising tree-like Frege proofs for QBF
- Resolution based algorithms for the transversal hypergraph generation problem
- A game characterisation of tree-like Q-resolution size
- Size, cost and capacity: a semantic technique for hard random QBFs
- What one has to know when attacking \(\mathsf{P}\) vs.\(\mathsf{NP}\)
- Towards NP-P via proof complexity and search
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Uses Software
This page was built for publication: Towards NP-P via proof complexity and search
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q408544)
