Pith Number

pith:RXAS6DMQ

pith:2026:RXAS6DMQOTQGDYXDK4ACVYBZP2

not attested not anchored not stored refs resolved

String Solving with Stabilization and Transducers (Technical Report)

David Chocholat\'y, Juraj S\'i\v{c}, Luk\'a\v{s} Hol\'ik, Michal \v{S}ed\'y, Ond\v{r}ej Leng\'al, Vojt\v{e}ch Havlena

Generalizing stabilization to transducers handles relational string constraints efficiently by reducing costly length operations.

arxiv:2605.14872 v1 · 2026-05-14 · cs.FL · cs.LO

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{RXAS6DMQOTQGDYXDK4ACVYBZP2}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

Implemented on top of Z3-Noodler, our method vastly outperforms existing solvers on benchmarks with relational constraints. It solves more instances and runs orders of magnitude faster.

C2weakest assumption

That the transducer encoding and length-constraint reductions preserve soundness and completeness while the new heuristics do not miss solutions on realistic inputs.

C3one line summary

Generalization of Z3-Noodler's stabilization method to transducers enables efficient solving of relational string constraints and outperforms prior solvers by solving more instances orders of magnitude faster.

References

50 extracted · 50 resolved · 0 Pith anchors

[1] SMT-COMP QF Strings, 2024 (2024),https://smt-comp.github.io/2024/ results/qf_strings-single-query/,https://smt-comp.github.io/2024/ results/qf_strings-single-query/ 2024

[2] SMT-COMP QF Strings, 2025 (2025),https://smt-comp.github.io/2025/ results/qf_slia-single-query/,https://smt-comp.github.io/2025/ results/qf_slia-single-query/ 2025

[3] In: Co- hen, A., Vechev, M.T 2017 · doi:10.1145/3062341.3062384

[4] In: Biere, A., Bloem, R 2014

[5] Springer (2014).https://doi.org/10.1007/978-3-319-08867-9_10,https: //doi.org/10.1007/978-3-319-08867-9_10 2014 · doi:10.1007/978-3-319-08867-9_10

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-17T23:38:56.128972Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

8dc12f0d9074e061e2e357002ae0397e9eb8a094fd3240d9be7eebdd38d5d63c

Aliases

arxiv: 2605.14872 · arxiv_version: 2605.14872v1 · doi: 10.48550/arxiv.2605.14872 · pith_short_12: RXAS6DMQOTQG · pith_short_16: RXAS6DMQOTQGDYXD · pith_short_8: RXAS6DMQ

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/RXAS6DMQOTQGDYXDK4ACVYBZP2 \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 8dc12f0d9074e061e2e357002ae0397e9eb8a094fd3240d9be7eebdd38d5d63c

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "3edf737b6692d6606490efebca69e094719558473d506c52da64198f492468eb",
    "cross_cats_sorted": [
      "cs.LO"
    ],
    "license": "http://creativecommons.org/licenses/by-nc-nd/4.0/",
    "primary_cat": "cs.FL",
    "submitted_at": "2026-05-14T14:18:40Z",
    "title_canon_sha256": "8c99d8e841989361a953f85a175fc46e65b1861a08f7dc915050269a79d10d24"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.14872",
    "kind": "arxiv",
    "version": 1
  }
}