Solving the resolution-free SAT problem by submodel propagation in linear time

DOI10.1007/s10472-005-0423-7zbMath1099.68101OpenAlexW4256704812MaRDI QIDQ1777398

Gábor Kusper

Publication date: 13 May 2005

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-005-0423-7

zbMATH Keywords

SATresolution-free SATsubmodel propagationUnicorn-SAT

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites Work

• Nested satisfiability
• A simplified NP-complete satisfiability problem
• A hierarchy of tractable satisfiability problems
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Recognition of \(q\)-Horn formulae in linear time
• New methods for 3-SAT decision and worst-case analysis
• A note on Dowling and Gallier's top-down algorithm for propositional Horn satisfiability
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Recognizing disguised NR(1) instances of the satisfiability problem
• On the Complexity of Timetable and Multicommodity Flow Problems
• A Complexity Index for Satisfiability Problems
• Extended Horn sets in propositional logic