Boolean circuits is arguably the most natural model for computing Boolean functions. Despite intensive research, for many functions, we still do not know what optimal circuits look like. In this paper, we discuss how SAT-solvers can be used for constructing optimal circuits for functions on moderate number of variables. We first discuss why this problem is important and then indicate the current frontiers: what can and cannot be found by state-of-The-Art SAT-solvers, and for what functions we are interested in finding efficient circuits.