"Linear circuit size upper and lower bounds"
(St. Petersburg Department of Steklov Institute of Mathematics)
Monday, April 13th, 2015, 2:00 pm
EBU3B, Room 4258
In the first part of the talk, we will show how SAT-solvers can help to prove stronger upper bounds on the boolean circuit complexity. Roughly, the main idea is that circuits for some functions are naturally built from blocks of constant size. E.g., the well-known circuit that computes the binary representation of the sum of $n$ input bits is built from $n$ full adders and has size $5n$. One can then state the question "whether there exist a block of smaller size computing the same function" in terms of CNF-
SAT and then ask SAT-solvers to verify this. Using this simple approach we managed to improve the upper bound for the above mentioned function to $4.5n$. This, in particular, implies that any symmetric function has circuit size at most $4.5n+o(n)$. We will also present improved upper bounds for some other symmetric functions.
In the second part we will present much simpler proofs of currently best known lower bounds on boolean circuit complexity. These are 3n-o(n) for the full binary basis [Blum, 1984] and 5n-o(n) for the binary basis where parity and its complement are excluded [Iwama, Morizumi, 2002]. The properties of the functions under consideration allow us to prove the stated lower bounds with almost no case analysis.