About some UP-based polynomial fragments of SAT
From MaRDI portal
Publication:513329
DOI10.1007/s10472-015-9452-zzbMath1404.68137MaRDI QIDQ513329
Olivier Fourdrinoy, Balasim Al-Saedi, Bertrand Mazure, Éric Grégoire, Lakhdar Saïs
Publication date: 6 March 2017
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-015-9452-z
68Q25: Analysis of algorithms and problem complexity
68T27: Logic in artificial intelligence
68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A simplified NP-complete satisfiability problem
- LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
- A hierarchy of tractable satisfiability problems
- A linear time algorithm for unique Horn satisfiability
- Recognition of \(q\)-Horn formulae in linear time
- A perspective on certain polynomial-time solvable classes of satisfiability
- Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
- Balanced matrices
- Properties of SLUR Formulae
- A note on Dowling and Gallier's top-down algorithm for propositional Horn satisfiability
- Using Boolean Constraint Propagation for Sub-clauses Deduction
- Eliminating Redundant Clauses in SAT Instances
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Algorithms for testing the satisfiability of propositional formulae
- Unit Refutations and Horn Sets
- Renaming a Set of Clauses as a Horn Set
- Extended Horn sets in propositional logic
- Theory and Applications of Satisfiability Testing
- The complexity of theorem-proving procedures
- Theory and Applications of Satisfiability Testing
