SAT-based Circuit Local Improvement

TL;DR

This paper introduces a SAT-based local search method for circuit size optimization, enabling automatic discovery of improved upper bounds for symmetric functions and demonstrating significant speedups over manual proofs.

Contribution

It presents a novel SAT-based local improvement technique for circuit optimization, automating and accelerating the process of finding upper bounds for circuit sizes.

Findings

Automated discovery of upper bounds for symmetric functions.

Significant speedup compared to manual proof methods.

Effective local search approach for circuit size reduction.

Abstract

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^{\Theta(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.