Determining Affine and Extended Affine Equivalence of Boolean Functions with SAT

by Luis Moraes and Rakesh Verma presented by Luis Moraes for the 11th Pragmatics of SAT International workshop (http://www.pragmaticsofsat.org/2020/)

Many cryptographically desirable properties of Boolean functions are preserved by affine and extended affine equivalence. Thus, being able to determine equivalence between Boolean functions efficiently is useful in cryptography. We present an encoding of affine and extended affine equivalence into SAT. We experiment with different encodings and demonstrate how implicit constraints affect performance. In addition, we draw parallels between known algorithms and these encodings.