A Direct Equivalence-Testing Algorithm for SLRs.

In this paper we study the recently introduced switch-list representations (SLRs) of Boolean functions. An SLR is a compressed truth table representation of a Boolean function: we only store the function value of the first row, and a list of switches (Boolean vectors whose function value differs from the value of the preceding vector). The paper (Čepek and Chromý 2020) systematically studies the properties of SLRs and among other results gives polynomial time algorithms for all standard queries investigated in the Knowledge Compilation Map (Darwiche and Marquis 2002). In particular, the equivalence query (EQ) is implemented in (Čepek and Chromý 2020) by first compiling both input SLRs into OBDDs and then running the EQ query on the constructed OBDDs. In this short note we present an algorithm that answers the EQ query directly by manipulating the input SLRs (hence eliminating the compilation step into OBDD) which improves the time complexity of the procedure.