Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning

DOI10.2168/LMCS-3(1:6)2007MaRDI QIDQ5310682zbMATH OpenOpenAlexFDO

Authors J. Hoffmann, Carla P. Gomes, Bart Selman

Publication date 11 October 2007

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/lmcs-3(1:6)2007

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• SAT-based planning in complex domains: Concurrency, constraints and nondeterminism
• Planning as satisfiability: parallel plans and algorithms for plan search
• SAS+ planning as satisfiability
• Complexity, decidability and undecidability results for domain-independent planning
• Logics in Artificial Intelligence
• Friends or foes? On planning as satisfiability and abstract CNF encodings
• DPLL: the core of modern satisfiability solvers
• Planning as constraint satisfaction: Solving the planning graph by compiling it into CSP

Cited in

(3)

• Tradeoffs in the Complexity of Backdoor Detection
• Backdoor sets of quantified Boolean formulas
• Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search

Describes a project that uses

Uses Software

• Graphplan
• Walksat
• IPC-4
• SymChaff
• MiniSat

This page was built for publication: Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning

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