You are looking at a specific version 20200506:134544 of this paper. See the latest version.

Paper 2020/530

Determining the Multiplicative Complexity of Boolean Functions using SAT

Mathias Soeken

Abstract

We present a constructive SAT-based algorithm to determine the multiplicative complexity of a Boolean function, i.e., the smallest number of AND gates in any logic network that consists of 2-input AND gates, 2-input XOR gates, and inverters. In order to speed-up solving time, we make use of several symmetry breaking constraints; these exploit properties of XAGs that may be useful beyond the proposed SAT-based algorithm. We further propose a heuristic post-optimization algorithm to reduce the number of XOR gates once the optimum number of AND gates has been obtained, which also makes use of SAT solvers. Our algorithm is capable to find all optimum XAGs for representatives of all 5-input affine-equivalent classes, and for a set of frequently occurring 6-input functions.

Metadata
Available format(s)
PDF
Publication info
Preprint.
Keywords
multiplicative complexitylogic synthesisXOR AND graphsSAT solvers
Contact author(s)
mathias soeken @ outlook com
History
2020-05-06: received
Short URL
https://ia.cr/2020/530
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.