An upper bound for resolution size: characterization of tractable SAT instances
DOI10.1007/978-3-319-53925-6_28zbMATH Open1485.68118OpenAlexW2588004537MaRDI QIDQ2980924FDOQ2980924
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
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
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
- Efficient and Constructive Algorithms for the Pathwidth and Treewidth of Graphs
- Algorithms for propositional model counting
- Satisfiability, branch-width and Tseitin tautologies
- Conjunctive-query containment and constraint satisfaction
- A linear time algorithm for finding tree-decompositions of small treewidth
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Constructive linear time algorithms for branchwidth
- Short proofs are narrow -- resolution made simple
- The intractability of resolution
- Minimum propositional proof length is NP-hard to linearly approximate
- Resolution Is Not Automatizable Unless W[P] Is Tractable
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- Tree-width, path-width, and cutwidth
- Narrow proofs may be maximally long
Cited In (2)
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)
