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.

Classical planning and checking the safety of hardware models are similar problems that can both be expressed as reachability in transition systems. When an algorithm claims that a set of target states is not reachable, this claim cannot be easily independently verified. Certifying algorithms address this limitation by producing computer-verifiable proofs of unreachability. Studying classical planning and hardware model checking, we compare both the underlying representation formalisms and the approaches that have been proposed for certifying unreachability. We show how bounded-cost plan existence can be expressed as a hardware circuit and that the certificates used in planning can be understood as a special case of certificates used in hardware model checking.

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.