用无缓存的GPU并行设计，加速复杂布尔代数表达式求解。
GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching
- 采用无缓存的自底向上枚举，避免传统缓存失效问题。
- 在大规模规格下速度超越旧方法数十倍，可处理更大表达式。
- 适合反混淆、编译优化等需高效求解定量表达式的场景。
从输入输出样例中合成混合布尔算术（MBA）表达式，是程序去混淆、编译优化、逆向工程和密码分析的核心任务。现有MBA求解器多基于CPU，对大规格或复杂目标扩展性差。近期的GPU加速方法虽提升速度，但依赖缓存等价候选结果；这一策略在MBA中失效，因候选输出为量化位向量，行为空间巨大。本文提出SIMBA（MBA合成），一种基于无缓存自底向上枚举的GPU加速求解器。SIMBA完全摒弃语言缓存，采用面向GPU的局部化并行枚举设计，显著提升计算效率。实验表明，SIMBA比现有工具快得多，能处理更大规格，解决旧方法无法应对的表达式规模。该成果确立了无缓存GPU合成在定量领域中的可行性与可扩展性，为缓存依赖架构提供了有力替代方案。
原文摘要 · Abstract (English)
Synthesizing Mixed-Boolean Arithmetic (MBA) expressions from input-output examples is central to program deobfuscation and also useful for compiler optimization, reverse engineering, and cryptanalysis. Existing MBA synthesizers are typically CPU-based and scale poorly on large specifications or complex targets. Recent GPU-accelerated synthesis methods achieve large speedups in qualitative settings, but they depend on caching observationally equivalent candidates; this strategy breaks down for MBA because candidate outputs are quantitative bitvectors and the behavioral space is enormous. We present SIMBA (Synthesis of Mixed-Boolean Arithmetic), a GPU-accelerated MBA synthesizer built around cache-free bottom-up enumeration. SIMBA avoids language caches entirely and uses a GPU-oriented enumeration design that keeps work local and highly parallel. In experiments, SIMBA is substantially faster than prior MBA synthesis tools, handles larger specifications, and reaches expression sizes that existing methods fail to solve. These results establish cache-free GPU synthesis as a practical and scalable approach for quantitative domains, and identify it as a strong alternative to cache-centric designs.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。