Search Results

Documents authored by Lagniez, Jean-Marie

Document
DOI: 10.4230/LIPIcs.CP.2025.38
Reducing Quantum Circuit Synthesis to #SAT

Authors: Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Quantum circuit synthesis is the task of decomposing a given quantum operator into a sequence of elementary quantum gates. Since the finite target gate set cannot exactly implement any given operator, approximation is often necessary. Model counting, or #SAT, has recently been demonstrated as a promising new approach for tackling core problems in quantum circuit analysis. In this work, we show for the first time that the universal quantum circuit synthesis problem can be reduced to maximum model counting. We formulate a #SAT encoding for exact and approximate depth-optimal quantum circuit synthesis into the Clifford+T gate set. We evaluate our method with an open-source implementation that uses the maximum model counter d4Max as a backend. For this purpose, we extended d4Max with support for complex and negative weights to represent amplitudes. Experimental results show that existing classical tools have potential for the quantum circuit synthesis problem.
Cite as

Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman. Reducing Quantum Circuit Synthesis to #SAT. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zak_et_al:LIPIcs.CP.2025.38,
  author =	{Zak, Dekel and Mei, Jingyi and Lagniez, Jean-Marie and Laarman, Alfons},
  title =	{{Reducing Quantum Circuit Synthesis to #SAT}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{38:1--38:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.38},
  URN =		{urn:nbn:de:0030-drops-238997},
  doi =		{10.4230/LIPIcs.CP.2025.38},
  annote =	{Keywords: Maximum weighted model counting, quantum circuit synthesis}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.21
Dynamic Blocked Clause Elimination for Projected Model Counting

Authors: Jean-Marie Lagniez, Pierre Marquis, and Armin Biere

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X . Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.
Cite as

Jean-Marie Lagniez, Pierre Marquis, and Armin Biere. Dynamic Blocked Clause Elimination for Projected Model Counting. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lagniez_et_al:LIPIcs.SAT.2024.21,
  author =	{Lagniez, Jean-Marie and Marquis, Pierre and Biere, Armin},
  title =	{{Dynamic Blocked Clause Elimination for Projected Model Counting}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.21},
  URN =		{urn:nbn:de:0030-drops-205430},
  doi =		{10.4230/LIPIcs.SAT.2024.21},
  annote =	{Keywords: Projected model counting, blocked clause elimination, propositional logic}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.28
A New Exact Solver for (Weighted) Max#SAT

Authors: Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
We present and evaluate d4Max, an exact approach for solving the Weighted Max#SAT problem. The Max#SAT problem extends the model counting problem (#SAT) by considering a tripartition of the variables {X, Y, Z}, and consists in maximizing over X the number of assignments to Y that can be extended to a solution with some assignment to Z. The Weighted Max#SAT problem is an extension of the Max#SAT problem with weights associated on each interpretation. We test and compare our approach with other state-of-the-art solvers on the challenging task in probabilistic inference of finding the marginal maximum a posteriori probability (MMAP) of a given subset of the variables in a Bayesian network and on exist-random quantified SSAT benchmarks. The results clearly show the overall superiority of d4Max in term of speed and number of instances solved. Moreover, we experimentally show that, in general, d4Max is able to quickly spot a solution that is close to optimal, thereby opening the door to an efficient anytime approach.
Cite as

Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli. A New Exact Solver for (Weighted) Max#SAT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{audemard_et_al:LIPIcs.SAT.2022.28,
  author =	{Audemard, Gilles and Lagniez, Jean-Marie and Miceli, Marie},
  title =	{{A New Exact Solver for (Weighted) Max#SAT}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.28},
  URN =		{urn:nbn:de:0030-drops-167022},
  doi =		{10.4230/LIPIcs.SAT.2022.28},
  annote =	{Keywords: Max#SAT, EMaj-SAT, Weighted Projected Model Counting, SSAT}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact