An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances
From MaRDI portal
Publication:2980924
DOI10.1007/978-3-319-53925-6_28zbMath1485.68118OpenAlexW2588004537MaRDI QIDQ2980924
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
Graph theory (including graph drawing) in computer science (68R10) Complexity of proofs (03F20) Parameterized complexity, tractability and kernelization (68Q27) Computational aspects of satisfiability (68R07)
Cites Work
- Satisfiability, branch-width and Tseitin tautologies
- The intractability of resolution
- Conjunctive-query containment and constraint satisfaction
- Tree-width, path-width, and cutwidth
- Algorithms for propositional model counting
- Minimum propositional proof length is NP-hard to linearly approximate
- Short proofs are narrow—resolution made simple
- Resolution Is Not Automatizable Unless W[P Is Tractable]
- Constructive linear time algorithms for branchwidth
- Efficient and Constructive Algorithms for the Pathwidth and Treewidth of Graphs
- A linear time algorithm for finding tree-decompositions of small treewidth
- Narrow Proofs May Be Maximally Long
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
This page was built for publication: An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances
