SAT-based Circuit Local Improvement
This work addresses the optimization challenge of exact circuit size for researchers in computational complexity and circuit design, though it is incremental as it builds on existing SAT-based methods.
The paper tackles the problem of reducing circuit size by applying a local search heuristic that checks subcircuits for potential improvements using SAT solvers, resulting in new upper bounds for symmetric functions and the ability to automatically rediscover decades-old bounds in seconds.
Finding exact circuit size is a notorious optimization problem in practice. Whereas modern computers and algorithmic techniques allow to find a circuit of size seven in blink of an eye, it may take more than a week to search for a circuit of size thirteen. One of the reasons of this behavior is that the search space is enormous: the number of circuits of size $s$ is $s^{Θ(s)}$, the number of Boolean functions on $n$ variables is $2^{2^n}$. In this paper, we explore the following natural heuristic idea for decreasing the size of a given circuit: go through all its subcircuits of moderate size and check whether any of them can be improved by reducing to SAT. This may be viewed as a local search approach: we search for a smaller circuit in a ball around a given circuit. Through this approach, we prove new upper bounds on the circuit size of various symmetric functions. We also demonstrate that some upper bounds that were proved by hand decades ago, nowadays can be found automatically in a few seconds.