  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.
