On Solving String Equations via Powers and Parikh Images

TL;DR

This paper introduces a novel approach for solving complex string equations by combining power operators, generalized Parikh images, and equality decomposition, extending the capabilities of existing methods.

Contribution

It presents a new methodology that enhances the solving of string equations, including challenging SMT inputs, by integrating multiple advanced techniques.

Findings

Successfully solves complex string equations

Extends the applicability of string solving methods

Handles less common SMT string inputs

Abstract

We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition. Using these methods allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.