SAT-Based Generation of Optimum Circuits

Generating size-optimum implementations of combinational circuits is known to be a \(\Sigma_2^P\)-complete problem, notwithstanding implementation constraints. For example, producing an optimum two-level (sum-of-products) form is as complex as designing an optimum multi-level circuit implementation. As a result, the practical synthesis complexity is double-exponential. In this talk, the ways of solving the problem of finding optimum multilevel circuit implementation using SAT and PBO will be presented. It will be shown how flexible this procedure is and how can it be customized to meet different implementation constraints and, on the other hand, how can it be easily extended to support new (emerging) technologies. Finally, applications where having optimum circuit implementations is vital will be presented.

Recording