Topology-Based Exact Synthesis for Majority Inverter Graph

SAT-based exact synthesis has important applications in logic optimization problems, and its scalability and computational speed greatly affect the optimization results. In the paper, a new topological constraint using the list of levels of inputs of each gate is introduced and accelerates the exact synthesis. Such topological constraints can reduce the search space by structure enumeration. By our new partition of the synthesis problem, we can maintain a good balance between runtime on a single satisfiability problem and the number of satisfiability problems. When compared to the fence-based method and the partial DAG based method, our methodology demonstrates a considerable reduction in runtime of 24.5% and 5.7%, respectively. Furthermore, our implementation can extend the scalability of SAT-based exact synthesis.