Zhang Jianmin, Li Tiejun and Ma Kefan, National University of Defense Technology, China

Explaining the causes of infeasibility of Boolean formulas has practical applications in various fields. A small unsatisfiable subset can provide a succinct explanation of infeasibility and is valuable for applications, such as FPGA routing. The Boolean-based FPGA detailed routing formulation expresses the routing constraints as a Boolean function which is satisfiable if and only if the layout is routable. The unsatisfiable subformulas can help the FPGA routing tool to diagnose and eliminate the causes of unroutable. For this typical application, a resolutionbased local search algorithm to extract unsatisfiable subformulas is integrated into Booleanbased FPGA routing method. The fastest algorithm of deriving minimum unsatisfiable subformulas, called the branch-and-bound algorithm, is adopted to compare with the local search algorithm. On the standard FPGA routing benchmark, the results show that the local search algorithm outperforms the branch-and-bound algorithm on runtime. It is also concluded that the unsatisfiable subformulas play a very important role in FPGA routing real applications.

FPGA routing, Boolean satisfiability, unsatisfiable subformula, local search.