With the growing scale and complexity of VLSI (Very Large Scale Integrated) chip designs

the FPGA (Field Programmable Gate Array) detailed routing process generally meets the congestion or unroutable problems during the FPGA implementation or prototype verification. The unsatisfiable subformulas can quickly diagnose the FPGA unroutable root cause

and accurately localize the critical nets. In order to accelerate the FPGA routing process

we have proposed a heuristic local search algorithm based on resolution refutation

to derive the unsatisfiable subformulas from the Boolean formulas. On the typical FPGA routing benchmarks

the local search algorithm has been compared to the two optimal minimum unsatisfiable subformula extraction algorithms. The experimental results show that the local search algorithm strongly outperforms the branch-bound algorithm and the greedy generic algorithm

and it also obtains the minimum unsatisfiable subformula. Furthermore

the unsatisfiable subformula plays an important role in FPGA routing

and it can improve the efficiency of design and verification of the VLSI chips.