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

DOI10.1007/S10472-005-0423-7MaRDI QIDQ1777398zbMATH OpenOpenAlexFDO

Authors 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

resolution-free SATSATsubmodel propagationUnicorn-SAT

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2065279
• scientific article; zbMATH DE number 5770428
• On tackling the limits of resolution in SAT solving
• Parameterized and subexponential-time complexity of satisfiability problems and applications
• Parameterized and subexponential-time complexity of satisfiability problems and applications
• scientific article; zbMATH DE number 1979549
• scientific article; zbMATH DE number 5542984
• Solving constraint satisfaction problems with SAT modulo theories

Cites work

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

Cited in

(3)

• Solving QSAT in sublinear depth
• scientific article; zbMATH DE number 5770428 (Why is no real title available?)
• scientific article; zbMATH DE number 2065279 (Why is no real title available?)

This page was built for publication: Solving the resolution-free SAT problem by submodel propagation in linear time

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