About some UP-based polynomial fragments of SAT

DOI10.1007/S10472-015-9452-ZMaRDI QIDQ513329zbMATH OpenOpenAlexFDO

Authors Balasim Al-Saedi, Olivier Fourdrinoy, E. Grégoire, Bertrand Mazure, Lakhdar Sais

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

zbMATH Keywords

SATunit propagationpolynomial classesQuadUP-Horn

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25) Logic in artificial intelligence (68T27)

Recommendations

• An improved upper bound for SAT
• Theory and Applications of Satisfiability Testing
• Satisfiability problem: Some polynomial classes of conjunctive normal forms
• Complexity of satisfiability problems with symmetric polynomial clauses
• A perspective on certain polynomial-time solvable classes of satisfiability
• Algorithms for Sat and upper bounds on their complexity
• On Some SAT-Variants over Linear Formulas
• scientific article; zbMATH DE number 17806
• New worst-case upper bounds for SAT
• New worst-case upper bounds for SAT

Cites work

• scientific article; zbMATH DE number 5852793 (Why is no real title available?)
• scientific article; zbMATH DE number 956858 (Why is no real title available?)
• A hierarchy of tractable satisfiability problems
• A linear time algorithm for unique Horn satisfiability
• A note on Dowling and Gallier's top-down algorithm for propositional Horn satisfiability
• A perspective on certain polynomial-time solvable classes of satisfiability
• A simplified NP-complete satisfiability problem
• Algorithms for testing the satisfiability of propositional formulae
• Balanced matrices
• Eliminating Redundant Clauses in SAT Instances
• Exploiting the real power of unit propagation lookahead
• Extended Horn sets in propositional logic
• Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• New inference rules for Max-SAT
• Properties of SLUR Formulae
• Recognition of q-Horn formulae in linear time
• Renaming a Set of Clauses as a Horn Set
• The complexity of theorem-proving procedures
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Unit Refutations and Horn Sets
• Using Boolean Constraint Propagation for Sub-clauses Deduction

Describes a project that uses

Uses Software

• Ltur
• DIMACS
• JBool
• MiniSat

This page was built for publication: About some UP-based polynomial fragments of SAT

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