UR-70: Faster Inequivalence Testing Using Robustness

We propose a new method for quickly testing the inequivalence of two Boolean functions, when one function is represented as an ordered binary decision diagram (OBDD), and the other is represented in conjunctive normal form (CNF). Our approach is based on a notion of classifier robustness from the fields of explainable AI (XAI) and adversarial machine learning. In particular, we show that two Boolean functions that are very similar in terms of their truth values, can be very different in terms of their robustness, which in turn, provides a witness to their inequivalence. A more efficient approach to inequivalence testing has an impact on the development of more efficient model counters and knowledge compilers. In turn, such developments facilitate advances in explainable AI and adversarial ML.