5th International School on Rewriting
3 – 8 July 2010, Drift 21, Utrecht, Netherlands
SAT Solving for Term Rewriting
Lecturer
Hans Zantema (Technische Universiteit Eindhoven and Radbout Universiteit Nijmegen, The Netherlands)Introduction
(advanced track, 2 sessions, mixed theoretical and practical)
SATisfiability is the following problem: given a propositional formula over a set of Boolean variables, decide whether it is satisfiable, that is, Boolean values can be assigned to the variables such that the formula yields true. Current SAT solvers easily solve instances over thousands of variables.
Several problems in term rewriting are essentially constraint problems that can be expressed in SAT solving. For instance, proving termination of a TRS by recursive path order corresponds to finding a precedence and status function such that a number of conditions hold. Rather than writing an algorithm for searching for a precedence and status function, one can express the requirements as a SAT problem, call a SAT solver, and then extract the found precendence and status function from the satisfying assignment found by the SAT solver. The latter approach turns out to be much more efficient. Similar observations hold for other techniques for proving termination, like finding argument filters and polynomial interpretations.
All current termination solvers like AProVE and TTT2 heavily use SAT solving. SAT solving also applies for other problems, like proving confluence or checking convertibility. More recent developments make use of SMT solving (satisfiability modulo theories), being an extension of SAT solving in which, for instance, one can express linear inequalities on integers directly, instead of encoding these inequalities as a SAT formula on the bits of the binary encoding of the numbers.