DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2024.14

Cooking String-Integer Conversions with Noodles

Authors: Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract

We propose a method for efficient handling string constraints with string-integer conversions. It extends the recently introduced stabilization-based procedure for solving string (dis)equations with regular and length constraints. Our approach is to translate the conversions into a linear integer arithmetic formula, together with regular constraints and word equations. We have integrated it into the string solver Z3-Noodler, and our experiments show that it is competitive and on some established benchmarks even several orders of magnitude faster than the state of the art.

Cite as

Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Cooking String-Integer Conversions with Noodles. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{havlena_et_al:LIPIcs.SAT.2024.14,
  author =	{Havlena, Vojt\v{e}ch and Hol{\'\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and S{\'\i}\v{c}, Juraj},
  title =	{{Cooking String-Integer Conversions with Noodles}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.14},
  URN =		{urn:nbn:de:0030-drops-205365},
  doi =		{10.4230/LIPIcs.SAT.2024.14},
  annote =	{Keywords: string solving, string conversions, SMT solving}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.2

Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation

Authors: Vojtěch Havlena and Ondřej Lengál

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

This paper provides several optimizations of the rank-based approach for complementing Büchi automata. We start with Schewe’s theoretically optimal construction and develop a set of techniques for pruning its state space that are key to obtaining small complement automata in practice. In particular, the reductions (except one) have the property that they preserve (at least some) so-called super-tight runs, which are runs whose ranking is as tight as possible. Our evaluation on a large benchmark shows that the optimizations indeed significantly help the rank-based approach and that, in a large number of cases, the obtained complement is the smallest from those produced by state-of-the-art tools for Büchi complementation.

Cite as

Vojtěch Havlena and Ondřej Lengál. Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 2:1-2:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{havlena_et_al:LIPIcs.CONCUR.2021.2,
  author =	{Havlena, Vojt\v{e}ch and Leng\'{a}l, Ond\v{r}ej},
  title =	{{Reducing (To) the Ranks: Efficient Rank-Based B\"{u}chi Automata Complementation}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{2:1--2:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.2},
  URN =		{urn:nbn:de:0030-drops-143799},
  doi =		{10.4230/LIPIcs.CONCUR.2021.2},
  annote =	{Keywords: B\"{u}chi automata, rank-based complementation, super-tight runs}
}

Search Results

Documents authored by Lengál, Ondřej

Cooking String-Integer Conversions with Noodles

Abstract

Cite as

Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation

Abstract

Cite as

Thanks for your feedback!

Could not send message