Parallel SAT Sweeping on CNFs

Abstract

Detecting semantic literal equivalences in propositional satisfiability (SAT) instances is an essential ingredient for Combinational Equivalence Checking (CEC), i.e., determining whether two combinational circuits are equivalent. Recent works highlighted clausal SAT sweeping as a viable and efficient approach for detecting such semantic equivalences. We present a careful parallelization of SAT sweeping that scales to hundreds of cores and significantly accelerates the equivalence sweeping process. Furthermore, we demonstrate how this scalable sweeping can be integrated seamlessly in an existing massively parallel SAT solver as a means of scalable preprocessing for CEC inputs.