ouml; rg Hoffmann

IJCAI Conference 2016 Conference Paper

Decoupled Strong Stubborn Sets

• Daniel Gnad
• Martin Wehrle
• J
• ouml; rg Hoffmann

Recent work has introduced fork-decoupled search, addressing classical planning problems where a single center component provides preconditions for several leaf components. Given a fixed center path π C, the leaf moves compliant with π C can then be scheduled independently for each leaf. Fork-decoupled search thus searches over center paths only, maintaining the compliant paths for each leaf separately. This can yield dramatic benefits. It is empirically complementary to partial order reduction via strong stubborn sets, in that each method yields its strongest reductions in different benchmarks. Here we show that the two methods can be combined, in the form of strong stubborn sets for fork-decoupled search. This can yield exponential advantages relative to both methods. Empirically, the combination reliably inherits the best of its components, and often outperforms both.

IJCAI Conference 2016 Conference Paper

On State-Dominance Criteria in Fork-Decoupled Search

• aacute; lvaro Torralba
• Daniel Gnad
• Patrick Dubbert
• J
• ouml; rg Hoffmann

Fork-decoupled search is a recent approach to classical planning that exploits fork structures, where a single center component provides preconditions for several leaf components. The decoupled states in this search consist of a center state, along with a price for every leaf state. Given this, when does one decoupled state dominate another? Such state-dominance criteria can be used to prune dominated search states. Prior work has devised only a trivial criterion. We devise several more powerful criteria, show that they preserve optimality, and establish their interrelations. We show that they can yield exponential reductions. Experiments on IPC benchmarks attest to the possible practical benefits.

IJCAI Conference 2015 Conference Paper

Simulation-Based Admissible Dominance Pruning

• aacute; lvaro Torralba
• J
• ouml; rg Hoffmann

In optimal planning as heuristic search, admissible pruning techniques are paramount. One idea is dominance pruning, identifying states “better than” other states. Prior approaches are limited to simple dominance notions, like “more STRIPS facts true” or “higher resource supply”. We apply simulation, well-known in model checking, to compute much more general dominance relations based on comparing transition behavior across states. We do so effectively by expressing state-space simulations through the composition of simulations on orthogonal projections. We show how simulation can be made more powerful by intertwining it with a notion of label dominance. Our experiments show substantial improvements across several IPC benchmark domains.

IJCAI Conference 2011 Conference Paper

Computing Perfect Heuristics in Polynomial Time: On Bisimulation and Merge-and-Shrink Abstraction in Optimal Planning

• Raz Nissim
• J
• ouml; rg Hoffmann
• Malte Helmert

A* with admissible heuristics is a very successful approach to optimal planning. But how to derive such heuristics automatically? Merge-and-shrink abstraction (M&S) is a general approach to heuristic design whose key advantage is its capability to make very fine-grained choices in defining abstractions. However, little is known about how to actually make these choices. We address this via the well-known notion of bisimulation. When aggregating only bisimilar states, M&S yields a perfect heuristic. Alas, bisimulations are exponentially large even in trivial domains. We show how to apply label reduction - not distinguishing between certain groups of operators - without incurring any information loss, while potentially reducing bisimulation size exponentially. In several benchmark domains, the resulting algorithm computes perfect heuristics in polynomial time. Empirically, we show that approximating variants of this algorithm improve the state of the art in M&S heuristics. In particular, a simple hybrid of two such variants is competitive with the leading heuristic LM-cut.

IJCAI Conference 2007 Conference Paper

• J
• ouml; rg Hoffmann
• Carla Gomes
• Bart Selman
• Henry Kautz

Translation to Boolean satisfiability is an important approach for solving state-space reachability problems that arise in planning and verification. Many important problems, however, involve numeric variables; for example, C programs or planning with resources. Focussing on planning, we propose a method for translating such problems into propositional SAT, based on an approximation of reachable variable domains. We compare to a more direct translation into "SAT modulo theory" (SMT), that is, SAT extended with numeric variables and arithmetic constraints. Though translation to SAT generates much larger formulas, we show that it typically outperforms translation to SMT almost up to the point where the formulas don't fit into memory any longer. We also show that, even though our planner is optimal, it tends to outperform state-of-the-art sub-optimal heuristic planners in domains with tightly constrained resources. Finally we present encouraging initial results on applying the approach to model checking.