Comparing CSP and SAT solvers for polynomial constraints in
termination provers
Authors
Salvador Lucas and Rafael Navarro
Abstract
Proofs of termination in term rewriting involve solving constraints
between terms coming from (parts of) the rules of the
term rewriting system. A common way to deal with such constraints
in termination tools is treating them as polynomial constraints.
Several recent works develop connections
between these problems and more standard constraint solving problems
for which well-known and efficient techniques apply.
In particular, SAT techniques are receiving increasing attention in the field.
The main idea is encoding polynomial constraints as
propositional constraints which can (hopefully) be efficiently managed
by using state-of-the-art SAT solvers.
We have recently developed an algorithm for solving
constraints in finite (small) domains of
coefficients which are appropriate for termination tools.
This algorithm benefits from the use of a specialized representation of
the elements in the domain and the corresponding polynomials
which permits using efficient arithmetics and constraint propagation techniques.
In this paper we discuss these approaches, compare them
from an experimental point of view, and point to possible improvements.
Keywords
Polynomial orderings, program analysis, term rewriting, termination.