Boolean matching of function vectors with strengthened learning

Boolean matching for multiple-output functions determines whether two given (in)completely-specified function vectors can be identical to each other under permutation and/or negation of their inputs and outputs. Despite its importance in design rectification, technology mapping, and other logic synthesis applications, there is no much direct study on this subject due to its generality and consequent computational complexity. This paper extends our prior Boolean matching decision procedure BooM to consider multiple-output functions. Through conflict-driven learning and partial assignment reduction, Boolean matching in the most general setting can still be accomplishable even when all other techniques lose their foundation and become unapplicable. Experiments demonstrate the indispensable power of strengthened learning for practical applications.