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

DOI10.2168/LMCS-3(1:6)2007zbMATH Open1128.68093OpenAlexW2950188036MaRDI QIDQ5310682FDOQ5310682

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

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

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)

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

Uses Software

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

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)