A note on SAT algorithms and proof complexity

DOI10.1016/J.IPL.2012.03.009zbMATH Open1243.68192OpenAlexW2009304285MaRDI QIDQ436581FDOQ436581

Authors Jan Krajíček

Publication date 25 July 2012

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2012.03.009

zbMATH Keywords

computational complexitySAT algorithms

Mathematics Subject Classification ID

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

Recommendations

• Hard satisfiable instances for DPLL-type algorithms
• scientific article; zbMATH DE number 1113991
• scientific article; zbMATH DE number 1222558
• Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas
• Automata, Languages and Programming

Cites work

• scientific article; zbMATH DE number 3912375 (Why is no real title available?)
• scientific article; zbMATH DE number 4066875 (Why is no real title available?)
• scientific article; zbMATH DE number 3557241 (Why is no real title available?)
• scientific article; zbMATH DE number 1215500 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• scientific article; zbMATH DE number 2212138 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
• An improved separation of regular resolution from pool resolution and clause learning
• Automata, Languages and Programming
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Logical foundations of proof complexity
• On the automatizability of resolution and related propositional proof systems
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• The relative efficiency of propositional proof systems
• Towards NP-P via proof complexity and search

Cited in

(11)

• scientific article; zbMATH DE number 2213633 (Why is no real title available?)
• Satisfiability via smooth pictures
• A remark on pseudo proof systems and hard instances of the satisfiability problem
• Proof Complexity for the Maximum Satisfiability Problem and its Use in SAT Refutations
• scientific article; zbMATH DE number 5914170 (Why is no real title available?)
• INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH
• SAT-Problems and Reductions with Respect to the Number of Variables
• Long proofs of (seemingly) simple formulas
• Ironic complicity: satisfiability algorithms and circuit lower bounds
• Complexity of SAT Problems, Clone Theory and the Exponential Time Hypothesis
• Hard satisfiable instances for DPLL-type algorithms

This page was built for publication: A note on SAT algorithms and proof complexity

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