Computed circuit complexity of decision problems
Yes, this is a natural idea and people have thought about it. In short, the problem is that even the state-of-the-art SAT/QBF-solvers allow to find very small circuits only (with about 10&ndash;12 gates), not to say about proving that there is no small circuit. Some references:


Ryan Williams, Applying practice to theory (2008): 


  Our knowledge of Boolean circuit complexity is quite poor. &lt;…>  One good reason why we don’t know much about the true power of circuits is that we don’t have many examples of minimum circuits. We don’t know, for example, what an optimal circuit for $3 \times 3$ Boolean matrix multiplication looks like.
  
  One good reason why we don’t know much about the true power of circuits is that we don’t have many examples of minimum circuits. We don’t know, for example, what an optimal circuit for $3 \times 3$ Boolean matrix multiplication looks like. &lt;…> Might we benefit from an Encyclopedia of Minimum Circuits? For example, what do the smallest Boolean circuits for $10 \times 10$ Boolean matrix multiplication look like? Are they regular in structure? It is likely that the answers would give valuable insight into the complexity of the problem. The best algorithms we know of reduce the problem to matrix multiplication over a ring, which is then solved by a highly regular, recursive construction (such as Strassen’s [Str69]). Even if the cataloged circuits are not truly minimal but close to that, concrete examples for small inputs could be useful for theoreticians to mine for inspiration, or perhaps for computers to mine for patterns via machine learning techniques. The power of small examples cannot be underestimated.
  
  Experiments with QBF solvers have not yet revealed significant new insight. So far, they have discovered one fact: the optimal size circuit for $2 \times 2$ Boolean matrix multiplication is the obvious one. Well, duh. What about the $3 \times 3$ case? This is already difficult! The sKizzo QBF solver [Ben05] can prove that there is no circuit for $3 
\times 3$ that has 10 gates, but nothing beyond that. Even when we restrict the gates to have fan-in two, the solver crashes on larger instances.


Together with Evgeny Demenkov, Arist Kojevnikov, and Grigory Yaroslavtsev we managed to use SAT-solvers to improve upper bounds on the circuit size of symmetric functions. Details can be found in the following two papers: Finding Efficient Circuits Using SAT-solvers (2009), New Upper Bounds on the Boolean Circuit Complexity of Symmetric Functions (2010). Still, we do not know the exact circuit complexity for many elementary functions: for example, $2.5n \le C(MOD_3) \le 3n$, $2n \le C(AND,OR,XOR) \le 2.5n$.



Exercises 477&ndash;481 in Section 7.2.2.2: Satisfiability of TAOCP Volume 4 by Don Knuth (2015) discuss ways of finding optimal circuits with the help of SAT solvers. From the solution to exercise 481:


  It’s true for $n \le 5$. Here’s a 12-step computation when $n=6$ and $a=0$, found in 2014 by Armin Biere: &lt;…> The case $n=6$ and $a \neq 0$, which lies tantalizingly close to the limits of today’s solvers, is still unknown.