Rule-based Word Equation Solving

We present a transformation-system-based technique in the framework of string solving, by reformulating a classical combinatorics on words result, the Lemma of Levi. We further enrich the induced rules by simplification steps based on results from the combinatorial theory of word equations, as well as by the addition of linear length constraints. This transformation-system approach cannot solve all equations efficiently by itself. To improve the efficiency of our transformation-system approach we integrate existing successful string solvers, which are called based on several heuristics. The experimental evaluation we performed shows that integrating our technique as an inprocessing step improves in general the performance of existing solvers.

Authors

• Joel D. Day
• Mitja Kulczynski
• Florin Manea
• Dirk Nowotka
• Danny Bøgsted Poulsen

Keywords

• Software engineering
• Heuristic
• Linear Constraints
• Theory Of Equations
• Benchmark
• Set Of Equations
• Search Space
• New Variables
• Transformation System
• R Function
• Inference Rules
• Benchmark Set
• Minimal Solution
• Regularization Constraint
• Word equations
• String Solving
• transition system
• Smt-solver