Towards NP-P via proof complexity and search (Q408544): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(6 intermediate revisions by 5 users not shown) | |||
Property / review text | |||
This article is a survey of proof complexity with particular emphasis on applications of proof complexity to proof search. The survey starts by providing background and some historical notes on proof systems and the P vs. NP question. It then discusses Cook's programme for separating NP and coNP and provides references to state-of-the-art lower bounds for the size of proofs. The next two sections are devoted to proof search and algorithmic consequences of proof complexity. The first item here is the efficient construction of proofs (automatizability) and current barriers towards that goal. Most proof systems are not automatizable (under suitable assumptions) and even to approximate the lengths of proofs is impossible (unless \(\mathrm{P}=\mathrm{NP}\)). The second item under the theme of proof search are relations to SAT solvers. In particular, modern algorithmic solving techniques (DPLL + clause learning) and their connections to subsystems of resolution are explained. The last two sections discuss general approaches for lower bounds (as proof complexity generators) and current barriers in this programme. | |||
Property / review text: This article is a survey of proof complexity with particular emphasis on applications of proof complexity to proof search. The survey starts by providing background and some historical notes on proof systems and the P vs. NP question. It then discusses Cook's programme for separating NP and coNP and provides references to state-of-the-art lower bounds for the size of proofs. The next two sections are devoted to proof search and algorithmic consequences of proof complexity. The first item here is the efficient construction of proofs (automatizability) and current barriers towards that goal. Most proof systems are not automatizable (under suitable assumptions) and even to approximate the lengths of proofs is impossible (unless \(\mathrm{P}=\mathrm{NP}\)). The second item under the theme of proof search are relations to SAT solvers. In particular, modern algorithmic solving techniques (DPLL + clause learning) and their connections to subsystems of resolution are explained. The last two sections discuss general approaches for lower bounds (as proof complexity generators) and current barriers in this programme. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Olaf Beyersdorff / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F20 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B05 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03D15 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q15 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q17 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68T15 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6022773 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
survey article | |||
Property / zbMATH Keywords: survey article / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
proof complexity | |||
Property / zbMATH Keywords: proof complexity / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
proof search | |||
Property / zbMATH Keywords: proof search / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
propositional logic | |||
Property / zbMATH Keywords: propositional logic / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
satisfiability | |||
Property / zbMATH Keywords: satisfiability / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
resolution | |||
Property / zbMATH Keywords: resolution / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
lower bounds | |||
Property / zbMATH Keywords: lower bounds / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: BerkMin / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: Chaff / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.apal.2011.09.009 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2202163874 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The independence of the modulo <i>p</i> counting principles / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Minimum propositional proof length is NP-hard to linearly approximate / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An exponential separation between regular and general resolution / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Resolution Is Not Automatizable Unless W[P] Is Tractable / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4681889 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The monotone circuit complexity of Boolean functions / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Principles and Practice of Constraint Programming – CP 2004 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4650571 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5715680 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4790380 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lower Bounds for Lovász–Schrijver Systems and Beyond Follow from Multiparty Communication Complexity / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Random CNF's are hard for the polynomial calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Non-automatizability of bounded-depth Frege proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On Interpolation and Automatization for Frege Systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4501551 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Polynomial size proofs of the propositional pigeonhole principle / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Propositional consistency proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4357061 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4263835 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear gaps between degrees for the polynomial calculus modulo distinct primes / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proof complexity in algebraic systems and bounded depth Frege systems with modular counting / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The NP-Completeness of Reflected Fragments of Justification Logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Many hard examples for resolution / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3136460 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The complexity of theorem-proving procedures / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4133141 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An overview of computational complexity / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4152212 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The relative efficiency of propositional proof systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Exponential Lower Bounds on the Lengths of Some Classes of Branch-and-Cut Proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A machine program for theorem-proving / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Computing Procedure for Quantification Theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the hardness of approximating label-cover / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4393480 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the automatizability of polynomial calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: BerkMin: A fast and robust SAT-solver / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The intractability of resolution / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: 3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3113688 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On optimal heuristic randomized semidecision procedures, with applications to proof complexity and cryptography / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A lower bound for intuitionistic logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lower bounds for modal logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On lengths of proofs in non-classical logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Note on Conservativity Relations among Bounded Arithmetic Theories / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the complexity of \(k\)-SAT / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Which problems have strongly exponential complexity? / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lower bounds for the polynomial calculus and the Gröbner basis algorithm / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3444802 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5501274 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The complexity of Horn fragments of linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Optimal proof systems imply complete sets for promise classes / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lower bounds to the size of constant-depth propositional proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the weak pigeonhole principle / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4630802 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3072543 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Propositional proof systems, the consistency of first order theories and the complexity of computations / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5606570 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the complexity of the reflected logic of proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Disjointness is hard in the multiparty number-on-the-forehead model / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linearizing intuitionistic implication / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: GRASP: a search algorithm for propositional satisfiability / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Solving satisfiability in less than \(2^ n\) steps / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3689182 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5417690 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An improved exponential-time algorithm for <i>k</i> -SAT / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4484662 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lambek calculus is NP-complete / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Exponential lower bounds for the pigeonhole principle / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Exponential Lower Bounds and Integrality Gaps for Tree-Like Lovász–Schrijver Procedures / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3755452 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3773878 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lower bounds for resolution and cutting plane proofs and monotone computations / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Twelve Problems in Proof Complexity / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Resolution lower bounds for the weak pigeonhole principle / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3758729 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lower bounds on the size of bounded depth circuits over a complete basis with logical addition / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lower bounds for the polynomial calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Resolution lower bounds for the weak functional pigeonhole principle. / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Resolution lower bounds for perfect matching principles / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Natural proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5422270 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Product-Free Lambek Calculus Is NP-Complete / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A probabilistic algorithm for \(k\)-SAT based on limited local search and restart / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An algorithm for the satisfiability problem of formulas in conjunctive normal form / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Complexity of Propositional Proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3682461 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5604434 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Hard examples for resolution / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 02:07, 5 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Towards NP-P via proof complexity and search |
scientific article |
Statements
Towards NP-P via proof complexity and search (English)
0 references
10 April 2012
0 references
This article is a survey of proof complexity with particular emphasis on applications of proof complexity to proof search. The survey starts by providing background and some historical notes on proof systems and the P vs. NP question. It then discusses Cook's programme for separating NP and coNP and provides references to state-of-the-art lower bounds for the size of proofs. The next two sections are devoted to proof search and algorithmic consequences of proof complexity. The first item here is the efficient construction of proofs (automatizability) and current barriers towards that goal. Most proof systems are not automatizable (under suitable assumptions) and even to approximate the lengths of proofs is impossible (unless \(\mathrm{P}=\mathrm{NP}\)). The second item under the theme of proof search are relations to SAT solvers. In particular, modern algorithmic solving techniques (DPLL + clause learning) and their connections to subsystems of resolution are explained. The last two sections discuss general approaches for lower bounds (as proof complexity generators) and current barriers in this programme.
0 references
survey article
0 references
proof complexity
0 references
proof search
0 references
propositional logic
0 references
satisfiability
0 references
resolution
0 references
lower bounds
0 references
0 references
0 references
0 references
0 references
0 references
0 references
0 references
0 references
0 references
0 references
0 references
0 references