'''Logic optimization''' is a process of finding an equivalent representation of the specified [[logic circuit]] under one or more specified constraints. This process is a part of a [[logic synthesis]] applied in [[digital electronics]] and [[integrated circuit design]].
Line 53 ⟶ 54:
=== Optimal multi-level methods ===
Methods whichthat find optimal circuit representations of Boolean functions are often referred to as "''exact synthesis"'' in the literature. Due to the computational complexity, exact synthesis is tractable only for small Boolean functions. Recent approaches map the optimization problem to a [[Satisfiability|Boolean satisfiability]] problem.<ref>{{cite web |last1=Haaswijk |first1=Winston |title=SAT-Based Exact Synthesis: Encodings, Topology Families, and Parallelism |url=https://si2.epfl.ch/~demichel/publications/archive/2020/winston-exact.pdf |website=EPFL |access-date=7 December 2022}}</ref><ref>{{cite web |last1=Haaswijk |first1=Winston |title=SAT-Based Exact Synthesis for Multi-Level Logic Networks |url=https://si2.epfl.ch/~demichel/graduates/theses/winston.pdf |website=EPFL |access-date=7 December 2022}}</ref> This allows finding optimal circuit representations using a [[SAT solver]].