GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching

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 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.