用数据驱动方法自动学习字符串求解器的分割策略，提升求解效率。
Learning Splitting Heuristics for Parallel String Solvers
- 将分割原子选择建模为学习任务，结合公式特征与运行时动态数据
- 在Z3seq和Z3str4中应用后，求解公式数和平均耗时均优于人工设计策略
- 适合需要高效处理复杂字符串约束的程序验证与安全分析场景
字符串约束求解器对理解字符串操作程序至关重要。然而，许多实际字符串约束是不可判定的，真实应用场景中的复杂约束常超出当前求解器的能力。多核架构的发展为并行求解提供了可能。关键的并行求解方法是“立方-征服”（cube-and-conquer），其分割启发式质量直接影响搜索空间划分效果。但手工设计启发式代价高，且往往次优。本文提出一种数据驱动方法，自动生成分割启发式。将分割原子选择问题建模为学习任务，利用输入公式的特征及求解过程中的动态数据。我们在两个主流字符串求解器Z3seq和Z3str4中实现该方法，结果表明，学习得到的启发式在求解公式数量和平均求解时间上均优于人工设计的启发式。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。