Layout Decomposition via Boolean Satisfiability

Multiple patterning lithography (MPL) has been introduced in the integrated circuits manufacturing industry to enhance feature density as the technology node advances. A crucial step of MPL is assigning layout features to different masks, namely layout decomposition. Exact algorithms like integer linear programming (ILP) can solve layout decomposition to optimality but lacks scalability for very dense patterns. Approximation algorithms (e.g., linear programming, semi-definite programming) and heuristics (e.g., Exact-Cover) are capable of handling large cases but can only get inferior solutions. In this paper, we propose a new exact algorithm that tackles layout decomposition by solving a series of boolean satisfiability instances. Our algorithm can preserve optimality and achieve more than 4× speedup compared to ILP. In addition, we provide an approximation algorithm by reformulating the layout decomposition to a bilevel optimization problem. Experiments show that our approximation algorithm can attain higher solution quality compared to SDP and heuristics within faster convergence.