Cooking string-integer conversions with noodles

DOI10.4230/LIPICS.SAT.2024.14MaRDI QIDQ6864430zbMATH OpenFDO

Authors Vojtěch Havlena, Lukáš Holik, Ondřej Lengál, Juraj Síč

Publication date 3 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.SAT.2024.14

zbMATH Keywords

SMT solvingstring conversionsstring solving

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites work

• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• A decision procedure for string logic with quadratic equations, regular expressions and length constraints
• A decision procedure for string to code point conversion
• A symbolic algorithm for the case-split rule in string constraint solving
• An SMT solver for regular expressions and linear arithmetic over string length
• Chain-free string constraints
• Logic and p-recognizable sets of integers
• Makanin's algorithm for word equations-two improvements and a generalization
• On solving word equations using SAT
• String theories involving regular membership predicates: from practice to theory and back
• Word equations in synergy with regular constraints

Cited in

(1)

• Word equations with length constraints via weak arithmetics and matrix reachability problems

This page was built for publication: Cooking string-integer conversions with noodles

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6864430)