Abstract:  In nanoscale integrated circuit design, redundant via insertion is a common technique to alleviate the yield loss caused by via failure. In this paper, the optimal redundant via insertion problem is converted to a maximum satisfiability (Max SAT) problem, and the optimal solution is obtained by using a complete solver. Since the Max SAT problem is NP-hard, two techniques are used in this paper to reduce the difficulty of finding solutions. One is the pre-selection, which reduces the size of the problem by identifying the redundant vias that do not conflict with other vias as partial solutions. The other is problem partitioning, which divides the original problem into several sub-problems with respect to the connected components to reduce the solution complexity. The paper also proves that these two methods can guarantee the optimality of the solution. Finally, the algorithm experiments on the benchmarks of the detailed routing competition of the International Symposium on Physical Design (ISPD) 2019. The optimality of the algorithm ensures that the insertion rate is maximized while resolving insertion conflicts, and the insertion rate of redundant vias is 67%-87% of all insertable vias.