Home // International Journal On Advances in Intelligent Systems, volume 6, numbers 3 and 4, 2013 // View article
Authors:
Nicolas Courtois
Theodosis Mourouzis
Daniel Hulme
Keywords: Linear Algebra, Fast Matrix Multiplication, Complex Numbers, quaternions, Strassen’s algorithm, Multiplicative Complexity, Asynchronous Circuits, Logic Minimization, Automated Theorem Provers, Block Ciphers, CTC2, PRESENT, GOST, SAT solvers
Abstract:
Two very important NP-hard problems in the area of computational complexity are the problems of Matrix Multiplication (MM) and Circuit Optimization. Solving particular cases of such problems yield to improvements in many other problems as they are core sub-routines implemented in many other algorithms. However, obtaining optimal solutions is an intractable problem since the space to explore for each problem is exponentially large. All suggested methodologies rely on wellchosen heuristics, selected according to the topology of the specific problem. Such heuristics may yield to efficient and acceptable solutions but they do not guarantee that no better can be done. In this paper, we suggest a general framework for obtaining solutions to such problems. We have developed a 2-step methodology, where in the first place we describe algebraically the problem and then we convert it to a SAT-CNF problem, which we solve using SAT-solvers. By running the same procedure for different values of k we can obtain optimal solutions and prove that no better can be done. We decrease the k until ”UNSAT” is obtained. Using the suitable encoding step for each problem we have been able to obtain exact and optimal solutions for different problems which are sufficiently small, allowing us to solve them on an average PC. We have been able to prove the exact number of multiplications needed for multiplying two non-square matrices of sufficiently small dimensions, as well as obtaining optimal representations with respect to meaningful metrics for several S-boxes used in prominent ultra-lightweight ciphers such as GOST, PRESENT and CTC2.
Pages: 165 to 176
Copyright: Copyright (c) to authors, 2013. Used with permission.
Publication date: December 31, 2013
Published in: journal
ISSN: 1942-2679