A Decision Procedure for String Logic with Equations, Regular Membership and Length Constraints

TL;DR

This paper introduces a decision procedure for a fragment of string logic involving equations, regular membership, and length constraints, which is proven to be decidable and terminates for formulas with limited variable occurrences.

Contribution

The paper presents a decidability result and a semi-decision procedure for string logic with specific constraints, addressing non-termination issues in previous algorithms.

Findings

Decidability proven for formulas with variables occurring at most twice.

Algorithm terminates for the specified fragment.

Worst-case factorial time complexity established.

Abstract

In this paper, we consider the satisfiability problem for string logic with equations, regular membership and Presburger constraints over length functions. The difficulty comes from multiple occurrences of string variables making state-of-the-art algorithms non-terminating. Our main contribution is to show that the satisfiability problem in a fragment where no string variable occurs more than twice in an equation is decidable. In particular, we propose a semi-decision procedure for arbitrary string formulae with word equations, regular membership and length functions. The essence of our procedure is an algorithm to enumerate an equivalent set of solvable disjuncts for the formula. We further show that the algorithm always terminates for the aforementioned decidable fragment. Finally, we provide a complexity analysis of our decision procedure to prove that it runs, in the worst case, in factorial time.