Tanja Schindler – Publications

Cartesian abstractions are a successful approach for obtaining admissible heuristics in optimal classical planning. In this paper, we generalize the counterexample-guided abstraction refinement (CEGAR) algorithm to compute Cartesian abstractions for simple numeric planning. Specifically, our CEGAR algorithm operates on a special form of Cartesian states consisting of a single interval per numeric variable. We prove that, in the absence of zero-cost actions, this algorithm is semi-complete and optimal. Our experimental evaluation shows that our approach performs similarly to other abstraction heuristics and provides better heuristic estimates in multiple domains.

Domain-independent Dynamic Programming (DIDP) recently emerged as a model-and-solve framework. Its performance heavily depends on a user-specified dual bound function. We introduce a way to automatically derive such bounds generalizing operator-counting heuristics from classical planning. The method approximates by how much an operator can change the value of a feature, which we compute using SAT modulo theories (SMT). We tighten the operator-counting LP using invariants derived by Abstract Interpretation. The dual bounds derived this way match well-known domain-specific dual bounds in TSP and Bin Packing. We evaluate our new dual bounds empirically in an established set of benchmarks.

We introduce lower-bound certificates for classical planning tasks, which can be used to prove the unsolvability of a task or the optimality of a plan in a way that can be verified by an independent third party. We describe a general framework for generating lower-bound certificates based on pseudo-Boolean constraints, which is agnostic to the planning algorithm used. As a case study, we show how to modify the A∗ algorithm to produce proofs of optimality with modest overhead, using pattern database heuristics and hmax as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.