Finding Efficient Circuits Using SAT-Solvers

Abstract In this paper we report preliminary results of experiments with finding efficient circuits (over binary bases) using SAT-solvers. We present upper bounds for functions with constant number of inputs as well as general upper bounds that were found automatically. We focus mainly on MOD-functions. Besides theoretical interest, these functions are also interesting from a practical point of view as they are the core of the residue number system. In particular, we present a circuit of size 3 n + c over the full binary basis computing \({\rm MOD}_3^n\).

Authors

• Arist Kojevnikov
• Alexander S. Kulikov
• Grigory Yaroslavtsev

Keywords

No keywords are indexed for this paper.