SAT-based Circuit Local Improvement
  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. We report the results of experiments with various
symmetric functions.
