[Software] Optimising Constant Matrix Multiplication Circuits is NP-complete
Description
This is the Lean 4 code used to mechanically verify the proof of NP-completeness for the Constant Matrix Multiplication (CMM) problem. The project is under active development under https://gitlab.uni-kassel.de/uk025743/leancmm. The original paper "Optimising Constant Matrix Multiplication Circuits is NP-complete" was presented at the Formal Methods in Computer-Aided Design (FMCAD) conference in 2026, Graz, Austria.
Abstract
Multiplication by constants is a fundamental operation in many practical applications, ranging from digital signal processing and numerical algorithms to the evaluation of artificial neural networks. This concept extends to multiplication by multiple constants and to multiplying a constant matrix with a vector of variables. In hardware implementations, costly multipliers are commonly replaced by sequences of shift and add/subtract operations tailored to the target constants. Prior work has approached this optimisation using declarative methods such as Boolean Satisfiability (SAT), whose worst-case runtime is exponential, but the computational complexity of the problem has remained open. In this paper we study the computational complexity of the Constant Matrix Multiplication (CMM) problem, which is concerned with the implementation of the multiplication of a fixed matrix by a vector of variables using shift-add operations instead of general multipliers. Given the matrix as a set of target vectors and a bound on the number of operations, the task is to determine whether all targets can be generated by a straight-line program with bounded length over a restricted set of shift-add instructions. We show that CMM is NP-complete, and that NP-hardness already holds for matrices with entries in {0, 1}. This demonstrates that the complexity of CMM arises not only from the coefficient bit widths but also from the structural properties of the matrix. We also formalise CMM and mechanise the hardness proof in Lean, providing a machine-checked verification of the result.
Multiplication by constants is a fundamental operation in many practical applications, ranging from digital signal processing and numerical algorithms to the evaluation of artificial neural networks. This concept extends to multiplication by multiple constants and to multiplying a constant matrix with a vector of variables. In hardware implementations, costly multipliers are commonly replaced by sequences of shift and add/subtract operations tailored to the target constants. Prior work has approached this optimisation using declarative methods such as Boolean Satisfiability (SAT), whose worst-case runtime is exponential, but the computational complexity of the problem has remained open. In this paper we study the computational complexity of the Constant Matrix Multiplication (CMM) problem, which is concerned with the implementation of the multiplication of a fixed matrix by a vector of variables using shift-add operations instead of general multipliers. Given the matrix as a set of target vectors and a bound on the number of operations, the task is to determine whether all targets can be generated by a straight-line program with bounded length over a restricted set of shift-add instructions. We show that CMM is NP-complete, and that NP-hardness already holds for matrices with entries in {0, 1}. This demonstrates that the complexity of CMM arises not only from the coefficient bit widths but also from the structural properties of the matrix. We also formalise CMM and mechanise the hardness proof in Lean, providing a machine-checked verification of the result.
Metadata
License
Except where otherwised noted, this item's license is described as GNU GENERAL PUBLIC LICENSE