GPUs are widely used to solve computationally intensive but highly parallelizable problems in machine learning. Program synthesis can also be computationally intensive, but prior work in GPU-accelerated program synthesis has been limited. We are only aware of one piece of related work which was done concurrently with our work, and focuses on regular expression synthesis.

Our goal is to synthesize a minimal-depth Boolean circuit that matches a provided truth table. Bottom-up enumeration — constructing larger circuits by combining smaller ones — is a natural fit for parallelization, because this work is easily divided between threads. We would also like to use observational equivalence (OE) reduction: if we create a new circuit whose truth table is identical to a previously enumerated circuit, the two are equivalent for our purposes, so we can discard the new circuit. Boolean circuits have a small output domain, so this would prune the search space significantly. However, OE reduction is more difficult to parallelize than enumeration, because it requires coordination between threads.

We present PEBBLES, a Boolean circuit synthesizer which uses compact wait-free data structures to parallelize bottom-up enumeration with OE reduction. We implemented single-threaded, multithreaded, and GPU-accelerated variants of PEBBLES, with the GPU achieving a 38x speedup over a single CPU core. On the SyGuS Cryptographic Circuit benchmarks, even our single-threaded variant is 7–7,000x faster than CVC5, the prior state of the art.