cs.AIJun 9, 2026

Learning Splitting Heuristics for Parallel String Solvers

Authors: Chenhao GaoPeisen Yao

Abstract

String constraint solvers are crucial for reasoning about string-manipulating programs. However, many practical string constraints are undecidable, and real-world applications often present complex constraints that challenge current solvers. The rise of multi-core architectures offers an opportunity for parallel solving. A key parallel solving method is \emph{cube-and-conquer}, in which the quality of splitting heuristics is critical to effectively dividing the search space. Unfortunately, manually designing the heuristics is labor-intensive, and handcrafted heuristics are often sub-optimal. This paper introduces a data-driven approach to automatically generating splitting heuristics. We frame the problem of selecting a splitting atom as a learning task, using features from input formulas and dynamic data from solver execution. We implement this approach in two popular string solvers, Z3seq and Z3str4, demonstrating that the learned heuristics outperform manually designed ones in the number of solved formulas and the average solving time.

Explore similar work

CardsList
  1. Learning How to Cube

    May 15, 2026Ferhat Erata, Sam Kouteili, Thanos Typaldos +4SatisfiabilityNeuro-Symbolic Framework

  2. DiBS: Diffusion-Informed Branch Selection

    Jun 2, 2026Bo Liu, Yuan Xie, Yuan Gao +4Puzzle