Program Specialization as a Tool for Solving Word Equations

TL;DR

This paper introduces a novel approach to solving word equations by specializing interpreters through program specialization techniques, enabling the construction of solution sets and satisfiability testing beyond existing SMT-solvers.

Contribution

It presents a new method of using program specialization to generate witnesses for word equations, extending the capabilities of existing solvers.

Findings

Specialized interpreters can construct solution sets for certain classes of word equations.

The approach provides a syntactic criterion for satisfiability of equations.

It can solve some equations that are unsolvable by Z3str3 and CVC4.

Abstract

The paper focuses on the automatic generating of the witnesses for the word equation satisfiability problem by means of specializing an interpreter which tests whether a composition of variable substitutions of a given word equation system produces its solution. We specialize such an interpreter w.r.t. the equation system, while the substitutions are unknown. We show that several variants of such interpreters, when specialized using the basic unfold/fold specialization methods, are able to construct the whole solution sets for some classes of the word equations whose left- and right-hand sides share variables. We prove that the specialization process wrt the constructed interpreters gives a simple syntactic criterion of the satisfiability of the equations considered, and show that the suggested approach can solve some equations not solvable by Z3str3 and CVC4, the widely-used SMT-solvers.