Incremental learning approach and SAT model for boolean matching with don’t cares

In this paper, we will propose an incremental learning approach to solve Boolean matching for incompletely specified functions. This approach can incrementally analyze current feasible partial mappings, detect and eliminate redundant manipulations in a proactive way. A new type of signature exploiting single variable symmetries is also given to reduce the searching space. Moreover, a SAT model of Boolean matching will be proposed to handle large Boolean functions. Through the utilization of these novel mechanisms, a drastic improvement on the performance of our Boolean matching algorithms are achieved. The experimental results demonstrate the effectiveness and efficiency of the proposed learning-based and SAT-based Boolean matching algorithms on many large benchmarking circuits.