Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width

DOI10.1007/978-3-642-29344-3_33MaRDI QIDQ2894482zbMATH OpenOpenAlexFDO

Authors Martin Fürer

Publication date 29 June 2012

Published in LATIN 2012: Theoretical Informatics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-29344-3_33

zbMATH Keywords

FPTparameterized complexityresolution proofssatisfiability testingtree-width

Mathematics Subject Classification ID

Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Short proofs are narrow -- resolution made simple
• Short proofs are narrow—resolution made simple
• Parameterized and Exact Computation
• Optimal length tree-like resolution refutations for 2SAT formulas
• On finding short resolution refutations and small unsatisfiable subsets

Cited in

(10)

• An upper bound for resolution size: characterization of tractable SAT instances
• Regular Resolution Versus Unrestricted Resolution
• NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
• Satisfiability, branch-width and Tseitin tautologies
• scientific article; zbMATH DE number 7238987 (Why is no real title available?)
• Optimal length tree-like resolution refutations for 2SAT formulas
• Parameterized and Exact Computation
• Width-parametrized SAT: time-space tradeoffs
• Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
• On finding short resolution refutations and small unsatisfiable subsets

This page was built for publication: Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width

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