Generalising and Unifying SLUR and Unit-Refutation Completeness

DOI10.1007/978-3-642-35843-2_20zbMath1303.68071OpenAlexW53965781MaRDI QIDQ2927648

Oliver Kullmann, Matthew Gwynne

Publication date: 4 November 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-35843-2_20

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (6)

On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\) ⋮ Bounds on the size of PC and URC formulas ⋮ Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers ⋮ Propagation complete encodings of smooth DNNF theories ⋮ The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas ⋮ Generalising unit-refutation completeness and SLUR via nested input resolution

Cites Work

• 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
• Generalising unit-refutation completeness and SLUR via nested input resolution
• Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
• Properties of SLUR Formulae
• Knowledge Compilation with Empowerment
• Unit Refutations and Horn Sets
• Present and Future of Practical SAT Solving
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Generalising and Unifying SLUR and Unit-Refutation Completeness