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

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

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)

Cites Work

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

Cited In (11)

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

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)