GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching
SIMBA is a GPU-accelerated MBA synthesizer using cache-free bottom-up enumeration to scale beyond prior CPU and cache-based GPU tools. It achieves substantial speedups, handles larger specifications, and solves expression sizes existing methods cannot.
Published 2026Paris Poster Session 3 · Thu, Dec 10, 12:30 PM–2:30 PM local time · Paris Poster HallarXiv ↗OpenReview ↗
Only vote on papers you've read. Sign in with GitHub to vote.
SIMBA replaces cache-dependent synthesis with a cache-free, GPU-oriented local enumeration that substantially outperforms CPU tools on complex MBA targets, though the evaluation offers no ablation, baseline counts, or proof of scalability beyond bitvector arenas.
Abstract
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.