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

zbMATH Keywords

satisfiabilityhardnessknowledge compilationgeneralized unit-propagationnested input resolutionpolynomial time SAT decisionsingle lookahead unit resolutionunit-refutation completeness

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (5)

Generalising and Unifying SLUR and Unit-Refutation Completeness ⋮ On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\) ⋮ Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers ⋮ Generalising unit-refutation completeness and SLUR via nested input resolution ⋮ XOR local search for Boolean Brent equations

Uses Software

• JBool

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