Reasoning about state constraints in the situation calculus
Naiqi Li, Yi Fan, Yongmei Liu · Griffith Research Online · 2013
In dynamic systems, state constraints are formulas that hold in every reachable state. It has been shown that state constraints can be used to greatly reduce the planning search space. They are also useful in program veri?cation. In this paper, we propose a sound but incomplete method for automatic veri?- cation and discovery of /forall^*/exists^* state constraints for a class of action theories that include many planning benchmarks. Our method is formulated in the situation calculus, theoretically based on Skolemization and Herbrand Theorem, and implemented with SAT solvers. Basically, we verify a state constraint by strengthening it in a novel and smart way so that it becomes a state invariant. We experimented with the blocks world, logistics and satellite domains, and the results showed that, almost all known state constraints can be veri?ed in a reasonable amount of time, and meanwhile succinct and intuitive related state constraints are discovered.