Parameterized complexity of DPLL search procedures

DOI10.1007/978-3-642-21581-0_3MaRDI QIDQ5892559zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

Publication date 17 June 2011

Published in Theory and Applications of Satisfiability Testing - SAT 2011 (Search for Journal in Brave)

Full work available at URL http://eprints.whiterose.ac.uk/74773/2/final-version-sat11.pdf

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Parameterized Complexity of DPLL Search Procedures
• Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas
• Complexity results on DPLL and resolution
• Automata, Languages and Programming
• Exponential lower bounds for DPLL algorithms on satisfiable random 3-CNF formulas

Cites work

• scientific article; zbMATH DE number 1445296 (Why is no real title available?)
• scientific article; zbMATH DE number 5485586 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• scientific article; zbMATH DE number 3029852 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• A machine program for theorem-proving
• Data reductions, fixed parameter tractability, and random weighted d-CNF satisfiability
• Hard examples for resolution
• Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
• Many hard examples for resolution
• On the relative complexity of resolution refinements and cutting planes proof systems
• Optimality of size-width tradeoffs for resolution
• Parameterized Complexity of DPLL Search Procedures
• Parameterized bounded-depth Frege is not optimal
• Parameterized proof complexity
• Resolution Is Not Automatizable Unless W[P] Is Tractable
• Short proofs are narrow—resolution made simple
• Short resolution proofs for a sequence of tricky formulas
• The efficiency of resolution and Davis-Putnam procedures
• The intractability of resolution
• The parameterized complexity of maximality and minimality problems
• The relative efficiency of propositional proof systems
• The resolution complexity of independent sets and vertex covers in random graphs
• \(k\)-subgraph isomorphism on \(\text{AC}^{0}\) circuits

Cited in

(8)

• Scaling up DPLL(T) string solvers using context-dependent simplification
• Parameterized Complexity of DPLL Search Procedures
• Random Instances of W[2]-Complete Problems: Thresholds, Complexity, and Algorithms
• A characterization of tree-like resolution size
• Clique problem, cutting plane proofs and communication complexity
• Parameterized bounded-depth Frege is not optimal
• Cliques enumeration and tree-like resolution proofs
• Relativization makes contradictions harder for resolution

This page was built for publication: Parameterized complexity of DPLL search procedures

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