Tanja Schindler
I am a postdoctoral researcher in the Artificial Intelligence group at the University of Basel.
My current research focus lies on classical planning.
I am particularly interested in certifying planning algorithms and in the connections between different approaches to planning.
I am also interested in automated deduction, in particular in satisfiability modulo theories.
Short bio
From 2016 to 2022, I was a doctoral researcher in the
Software Engineering group headed by
Prof. Dr. Andreas Podelski
at the University of Freiburg, Germany,
where I worked on satisfiability modulo theories,
and received my PhD in July 2022.
From 2022 to 2023, I was a postdoctoral researcher in the Distributed Systems group headed by
Prof. Dr. Pascal Fontaine
at the University of Liège, Belgium.
In December 2023, I joined the Artificial Intelligence group headed by
Prof. Dr. Malte Helmert
at the University of Basel.
Publications
(Show all abstracts)
(Hide all abstracts)
2026
-
Tanja Schindler, David Speck and Malte Helmert.
Cartesian Abstraction Refinement for Simple Numeric Planning.
In
Proceedings of the 36th International Conference on Automated Planning and Scheduling
(ICAPS 2026).
2026.
(Show abstract)
(Hide abstract)
(PDF)
(code, benchmarks, and data)
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.
-
Anubhav Singh, Florian Pommerening, Tanja Schindler, J. Christopher Beck and Malte Helmert.
Operator-Counting Heuristics for Domain-Independent Dynamic Programming.
In
Proceedings of the 36th International Conference on Automated Planning and Scheduling
(ICAPS 2026).
2026.
(Show abstract)
(Hide abstract)
(PDF)
(supplemental material; PDF)
(code and data)
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.
2025
-
Simon Dold, Malte Helmert, Jakob Nordström, Gabriele Röger and Tanja Schindler.
Pseudo-Boolean Proof Logging for Optimal Classical Planning.
In
Proceedings of the 35th International Conference on Automated Planning and Scheduling
(ICAPS 2025), pp. 54-63.
2025.
(Show abstract)
(Hide abstract)
(PDF)
(extended version)
(slides; PDF)
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.
