smt

This paper investigates numerical Totally-Ordered HTN planning by extending SAT-based encodings with SMT to handle numeric fluents, introduces a benchmark suite, and shows competitive performance as a baseline for future work.

This paper presents two sound encodings (MIP and SMT) for multi-agent path planning with spatio-temporal and topological constraints expressed in STL-GO, and evaluates them on a multi-UAV search-and-rescue benchmark.

Introduces an SMT-based pipeline for synthesizing maze solution paths from input patterns and constructing planar and 3D maze structures. Extends a conference paper with detailed construction methods and SMT-LIB examples.

This paper introduces Verifiable Transformers, a framework that converts task-localized Transformer circuits into bounded, solver-checkable claims, enabling formal verification of properties such as functional equivalence, edge necessity, and robustness.