Learning Splitting Heuristics for Parallel String Solvers
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Longest Common Substring in Longest Common Subsequence's Solution Service: A Novel Hyper-Heuristic
The Longest Common Subsequence (LCS) is the problem of finding a subsequence among a set of strings that has two properties of being common to all and is the longest. The LCS has applications in computational biology and…
Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)
This paper proposes a Graph Neural Network-guided algorithm for solving word equations, based on the well-known Nielsen transformation for splitting equations. The algorithm iteratively rewrites the first terms of each s…
Decision MakingGraph Neural NetworkProximal Iteratively Reweighted Algorithm with Multiple Splitting for Nonconvex Sparsity Optimization
This paper proposes the Proximal Iteratively REweighted (PIRE) algorithm for solving a general problem, which involves a large body of nonconvex sparse and structured sparse related problems. Comparing with previous iter…
Optimization by Parallel Quasi-Quantum Annealing with Gradient-Based Sampling
Learning-based methods have gained attention as general-purpose solvers due to their ability to automatically learn problem-specific heuristics, reducing the need for manually crafted heuristics. However, these methods o…
Combinatorial OptimizationBayesian Synchronous Grammar Induction
We present a novel method for inducing synchronous context free grammars (SCFGs) from a corpus of parallel string pairs. SCFGs can model equivalence between strings in terms of substitutions, insertions and deletions, an…
Machine TranslationTranslation