GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching
Gabriel Bathie, Baptiste Mouillon, Nathana\"el Fijalkow

TL;DR
This paper introduces SIMBA, a GPU-based, cache-free method for synthesizing Mixed-Boolean Arithmetic expressions that outperforms prior CPU and GPU approaches in speed and scalability.
Contribution
The paper presents a novel cache-free, GPU-accelerated synthesis approach for MBA expressions, enabling larger and more complex specifications to be solved efficiently.
Findings
SIMBA is significantly faster than previous tools.
It can handle larger specifications and expression sizes.
It demonstrates the effectiveness of cache-free GPU synthesis in quantitative domains.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
