An upper bound for resolution size: characterization of tractable SAT instances

DOI10.1007/978-3-319-53925-6_28MaRDI QIDQ2980924zbMATH OpenOpenAlexFDO

Authors Kensuke Imanishi

Publication date 5 May 2017

Published in WALCOM: Algorithms and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-53925-6_28

zbMATH Keywords

pathwidthparameterized complexitysatisfiabilityincidence graphresolution size

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Complexity of proofs (03F20) Parameterized complexity, tractability and kernelization (68Q27) Computational aspects of satisfiability (68R07)

Recommendations

• Parameterized and Exact Computation
• On finding short resolution refutations and small unsatisfiable subsets
• A note on width-parameterized SAT: an exact machine-model characterization
• Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width
• Theory and Applications of Satisfiability Testing

Cites work

• A Computing Procedure for Quantification Theory
• A linear time algorithm for finding tree-decompositions of small treewidth
• A machine program for theorem-proving
• Algorithms for propositional model counting
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Conjunctive-query containment and constraint satisfaction
• Constructive linear time algorithms for branchwidth
• Efficient and Constructive Algorithms for the Pathwidth and Treewidth of Graphs
• Minimum propositional proof length is NP-hard to linearly approximate
• Narrow proofs may be maximally long
• Resolution Is Not Automatizable Unless W[P] Is Tractable
• Satisfiability, branch-width and Tseitin tautologies
• Short proofs are narrow -- resolution made simple
• The intractability of resolution
• Tree-width, path-width, and cutwidth

Cited in

(2)

• From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
• Theory and Applications of Satisfiability Testing

This page was built for publication: An upper bound for resolution size: characterization of tractable SAT instances

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