DROPS

Document

DOI: 10.4230/LIPIcs.CP.2026.11

Solving the Multiple Constant Multiplication Problem with Constraint Programming

Authors: Théo Cantaloube, Xiao Peng, Christine Solnon, and Anastasia Volkova

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract

The Multiple Constant Multiplication (MCM) problem arises in many applications such as, for example, digital signal processing or deep neural network inference. Given a set T of target constants, the goal of MCM is to find the most efficient way for multiplying an input number with every constant in T, where multiplications are realized through bit-shifts and additions, and where intermediate results may be shared to produce different target constants. In this paper, we first introduce a basic Constraint Programming (CP) model to solve MCM. Then, we introduce symmetry breaking rules and a global constraint to ensure them. We experimentally evaluate our approach on a widely used benchmark extracted from a collection of digital filter designs. We show that the basic CP model is competitive with state-of-the-art Integer Linear Programming (ILP) and SAT models, and that the addition of our global symmetry breaking constraint allows us to clearly outperform all other existing approaches on the considered benchmark.

Cite as

Théo Cantaloube, Xiao Peng, Christine Solnon, and Anastasia Volkova. Solving the Multiple Constant Multiplication Problem with Constraint Programming. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{cantaloube_et_al:LIPIcs.CP.2026.11,
  author =	{Cantaloube, Th\'{e}o and Peng, Xiao and Solnon, Christine and Volkova, Anastasia},
  title =	{{Solving the Multiple Constant Multiplication Problem with Constraint Programming}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.11},
  URN =		{urn:nbn:de:0030-drops-266448},
  doi =		{10.4230/LIPIcs.CP.2026.11},
  annote =	{Keywords: Constraint Programming, Multiple Constant Multiplication, Hardware Optimization}
}

Document

DOI: 10.4230/LIPIcs.ITP.2022.6

Dandelion: Certified Approximations of Elementary Functions

Authors: Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract

Elementary function operations such as sin and exp cannot in general be computed exactly on today’s digital computers, and thus have to be approximated. The standard approximations in library functions typically provide only a limited set of precisions, and are too inefficient for many applications. Polynomial approximations that are customized to a limited input domain and output accuracy can provide superior performance. In fact, the Remez algorithm computes the best possible approximation for a given polynomial degree, but has so far not been formally verified. This paper presents Dandelion, an automated certificate checker for polynomial approximations of elementary functions computed with Remez-like algorithms that is fully verified in the HOL4 theorem prover. Dandelion checks whether the difference between a polynomial approximation and its target reference elementary function remains below a given error bound for all inputs in a given constraint. By extracting a verified binary with the CakeML compiler, Dandelion can validate certificates within a reasonable time, fully automating previous manually verified approximations.

Cite as

Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin. Dandelion: Certified Approximations of Elementary Functions. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ITP.2022.6,
  author =	{Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste},
  title =	{{Dandelion: Certified Approximations of Elementary Functions}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.6},
  URN =		{urn:nbn:de:0030-drops-167155},
  doi =		{10.4230/LIPIcs.ITP.2022.6},
  annote =	{Keywords: elementary functions, approximation, certificate checking}
}

Search Results

Documents authored by Volkova, Anastasia

Solving the Multiple Constant Multiplication Problem with Constraint Programming

Abstract

Cite as

Dandelion: Certified Approximations of Elementary Functions

Abstract

Cite as

Thanks for your feedback!

Could not send message