A Uniform Framework for Handling Position Constraints in String Solving
summary
Introduces a decision procedure that avoids encoding to word equations and instead reduces position constraints to integer constraints extracted from the Parikh image of a polynomial‑size finite tag automaton, making general position solving NP‑complete and some common fragments PTime. Extends to a large flat fragment of ¬contains with NExpTime decidability, encodes constraints as linear integer arithmetic, and ships as a practical backend in Z3‑Noodler, yielding measurable benchmark improvements over prior automata‑based solvers.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 3:12Position constraints in string solving
- 6:23Tag automata and Parikh's theorem
- 8:09Length constraints with tag automata
- 9:54Simple disequalities with tag automata
- 12:23Complex disequalities with concatenation
- 14:29Not prefix/suffix/position constraints
- 14:49Not contains constraints challenges
- 16:58Decidability and complexity
- 17:41Experimental evaluation
- 18:24Future work and conclusion
- 18:50Q&A
related talks
19mA Constraint Solving Approach to Parikh Images of Regular Languages
24mSolving String Constraints with Regex-Dependent Functions through Transducers wi
15mInter-theory Dependency Analysis for SMT String Solvers
33mSolving constraints during type inference
19mSMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
01h 02mTheory and Control
35mA Peek Inside SAT Solvers
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration