Properties of SLUR Formulae

DOI10.1007/978-3-642-27660-6_15zbMath1298.68110MaRDI 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 functions; CNF satisfiability; unit resolution

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

03B05: Classical propositional logic

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

Related Items

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, Generalising and Unifying SLUR and Unit-Refutation Completeness

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