@inproceedings{JarvisaloKKK:SAT2012,
 author = {Matti J\"arvisalo and Petteri Kaski 
	and Mikko Koivisto and Janne H. Korhonen},
 title  = {Finding Efficient Circuits for Ensemble Computation},
 editor = {Alessandro Cimatti and Roberto Sebastiani},
 booktitle = {Proceedings of the 15th International Conference on 
	Theory and Applications of Satisfiability Testing (SAT 2012)},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 volume = {7317},
 pages  = {369--382},
 year   = {2012},
}

Abstract:

Given a Boolean function as input, a fundamental problem is to find
a Boolean circuit with the least number of elementary gates (AND, OR, NOT)
that computes the function. The problem generalises naturally to the setting of
multiple Boolean functions: find the smallest Boolean circuit that computes all the
functions simultaneously. We study an NP-complete variant of this problem titled
Ensemble Computation and, especially, its relationship to the Boolean satisfiability
(SAT) problem from both the theoretical and practical perspectives, under the
two monotone circuit classes: OR-circuits and SUM-circuits. Our main result
relates the existence of nontrivial algorithms for CNF-SAT with the problem of
rewriting in subquadratic time a given OR-circuit to a SUM-circuit. Furthermore,
by developing a SAT encoding for the ensemble computation problem and by
employing state-of-the-art SAT solvers, we search for concrete instances that
would witness a substantial separation between the size of optimal OR-circuits
and optimal SUM-circuits. Our encoding allows for exhaustively checking all
small witness candidates. Searching over larger witness candidates presents an
interesting challenge for current SAT solver technology.