Generalising unit-refutation completeness and SLUR via nested input resolution
DOI10.1007/s10817-013-9275-8zbMath1319.03036arXiv1204.6529OpenAlexW3104714466MaRDI QIDQ2352484
Oliver Kullmann, Matthew Gwynne
Publication date: 2 July 2015
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1204.6529
satisfiabilityhardnessknowledge compilationgeneralized unit-propagationnested input resolutionpolynomial time SAT decisionsingle lookahead unit resolutionunit-refutation completeness
Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Related Items (5)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the power of clause-learning SAT solvers as resolution engines
- On finding solutions for extended Horn formulas
- On generalized Horn formulas and \(k\)-resolution
- Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems
- A short note on some tractable cases of the satisfiability problem.
- A perspective on certain polynomial-time solvable classes of satisfiability
- Relaxations of the satisfiability problem using semidefinite programming
- Generalising unit-refutation completeness and SLUR via nested input resolution
- Complexity of constraints. An overview of current research themes
- Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
- Pebble Games, Proof Complexity, and Time-Space Trade-offs
- Properties of SLUR Formulae
- Knowledge Compilation with Empowerment
- Generalising and Unifying SLUR and Unit-Refutation Completeness
- Effective Incorporation of Double Look-Ahead Procedures
- Unit Refutations and Horn Sets
- On SAT Representations of XOR Constraints
- Present and Future of Practical SAT Solving
This page was built for publication: Generalising unit-refutation completeness and SLUR via nested input resolution