A Constraint Solving Approach to Parikh Images of Regular Languages
summary
Presents a constraint-solving reframing of Parikh-image extraction: build PC calculus and a standalone tool Catra tool* that ties to the Princess SMT engine, encodes each automaton transition with a fresh flow variable, prunes transitions by solving linear equalities, enforces connectivity lazily and uses case splitting to shrink products before materializing them. Evaluated on Ostrich+–generated benchmarks, it strictly outperforms Verma et al. and Janků/Turoňová, beats nuXmv for realistic timeouts (<60 s) and when plugged into Ostrich+ solves the most Unsat QF_SLIA instances at SMT‑COMP 2023.
AI-written summary · about
chapters (14)
- 0:00String constraint solving intro
- 1:04Substring and length constraints
- 2:27Parikh automata and registers
- 3:50Product computation problem
- 4:54Pruning automata terms
- 5:39Catra framework intro
- 6:20Automata pruning example
- 8:29Pruning via linear equations
- 9:34Case splitting transitions
- 10:39Lazy connectivity constraints
- 11:20Final product and results
- 12:03Benchmarking solvers
- 13:31Approach summary
- 13:52Q&A
related talks
20mA Uniform Framework for Handling Position Constraints in String Solving
24mSolving String Constraints with Regex-Dependent Functions through Transducers wi
49mAn Introduction to Constraint Programming
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
35mA Peek Inside SAT Solvers
33mSolving constraints during type inference
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
28mScimitar: Functional Programs as Optimization Problems