Generalising and unifying SLUR and unit-refutation completeness

DOI10.1007/978-3-642-35843-2_20MaRDI QIDQ2927648zbMATH OpenOpenAlexFDO

Authors Matthew Gwynne, Oliver Kullmann

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

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

Recommendations

• Generalising unit-refutation completeness and SLUR via nested input resolution
• Properties of SLUR Formulae
• A hierarchy of tractable satisfiability problems
• On resolution with short clauses
• A perspective on certain polynomial-time solvable classes of satisfiability

Cites work

• A perspective on certain polynomial-time solvable classes of satisfiability
• A short note on some tractable cases of the satisfiability problem.
• Generalising unit-refutation completeness and SLUR via nested input resolution
• scientific article; zbMATH DE number 5852793 (Why is no real title available?)
• scientific article; zbMATH DE number 1113994 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Knowledge compilation with empowerment
• Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
• On finding solutions for extended Horn formulas
• On generalized Horn formulas and k-resolution
• On the power of clause-learning SAT solvers as resolution engines
• Present and Future of Practical SAT Solving
• Properties of SLUR Formulae
• Unit Refutations and Horn Sets
• Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems

Cited in

(6)

• 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
• Synthesis of domain specific CNF encoders for bit-vector solvers
• On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
• Bounds on the size of PC and URC formulas

This page was built for publication: Generalising and unifying SLUR and unit-refutation completeness

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