SAT Instances for Termination Analysis with AProVE
Carsten Fuhs · 2009
Recently, SAT solving has become the backbone for tackling the search problems in automated termination analysis for term rewrite systems and for programming languages. Indeed, even since the last SAT competition in 2007, many new termination techniques have been pub- lished where automation heavily relies on the eciency of modern SAT solvers. Here, a successful satisfiability proof of the SAT instance results in a step in the modular termination proof and simplifies the termination problem to be analyzed. The present SAT benchmark submission was created using the auto- mated termination prover AProVE. The CNFs stem from termination proof steps using various recent termination techniques. All instances of this submission are satisfiable, and any speed-up for SAT solvers on these instances will directly lead to performance improvements also for automated termination provers.