Properties of SLUR Formulae

DOI10.1007/978-3-642-27660-6_15zbMath1298.68110OpenAlexW59346742MaRDI QIDQ2891367

Vaclav Vlcek, Ondřej Čepek, Petr Kučera

Publication date: 15 June 2012

Published in: SOFSEM 2012: Theory and Practice of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-27660-6_15

zbMATH Keywords

Boolean functionsCNF satisfiabilityunit resolution

Mathematics Subject Classification ID

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

Related Items

Generalising and Unifying SLUR and Unit-Refutation Completeness, Bounds on the size of PC and URC formulas, About some UP-based polynomial fragments of SAT, The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas, Generalising unit-refutation completeness and SLUR via nested input resolution

Uses Software

• Ltur

Cites Work

• Unnamed Item
• Unnamed Item
• On finding solutions for extended Horn formulas
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• A hierarchy of tractable satisfiability problems
• A perspective on certain polynomial-time solvable classes of satisfiability
• Balanced matrices
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Unification as a complexity measure for logic programming
• Recognizing disguised NR(1) instances of the satisfiability problem
• Renaming a Set of Clauses as a Horn Set
• Extended Horn sets in propositional logic