Scholarlink

<p>We propose a new automata-based algorithm for solving string constraints that tightly integrates reasoning about equations and regular constraints. Exchanging information between the two allows an efficient pruning of generated combinatorial cases. The algorithm is based on a novel language-based characterization of satisfiability of word equations with regular constraints. Namely, satisfiability of an equation is implied by its <i>stability</i>: the concatenation of the regular languages constraining variables on the left-hand side equals the concatenation of the languages on the right-hand side. It is complete for the chain-free string constraints. We experimentally show that our prototype implementation is competitive with the best string solvers and even superior on difficult examples.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Word equations in synergy with regular constraints (extended version)

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年5月21日

查看全文
  • František Blahoudek,
  • Yu-Fang Chen,
  • David Chocholatý,
  • Vojtěch Havlena,
  • Lukáš Holík,
  • Ondřej Lengál,
  • Juraj Síč

摘要

We propose a new automata-based algorithm for solving string constraints that tightly integrates reasoning about equations and regular constraints. Exchanging information between the two allows an efficient pruning of generated combinatorial cases. The algorithm is based on a novel language-based characterization of satisfiability of word equations with regular constraints. Namely, satisfiability of an equation is implied by its stability: the concatenation of the regular languages constraining variables on the left-hand side equals the concatenation of the languages on the right-hand side. It is complete for the chain-free string constraints. We experimentally show that our prototype implementation is competitive with the best string solvers and even superior on difficult examples.