Modélisation et résolution de problèmes sous contraintes
De nombreuses tâches en intelligence artificielle, et plus généralement en informatique, nécessitent la résolution de problèmes difficiles d’un point de vue calculatoire.
L’axe « Contraintes » porte sur la modélisation et la résolution pratique de problèmes combinatoires sous contraintes. Deux formalismes sont principalement étudiés dans l’axe : SAT (Satisfiability Testing), où les variables sont booléennes et CSP (Constraint Satisfaction Problem) où les variables sont définies sur des domaines finis. Ces deux formalismes entrent dans le champ général de la programmation par contraintes (CP pour Constraint Programming). Parmi les problèmes étudiés figurent les problèmes de satisfaction (existence d’une solution), d’optimisation (recherche d’une « meilleure » solution), de comptage (calcul du nombre de solutions), d’énumération (des solutions). Les travaux réalisés dans l’axe vont de développements théoriques (étude de complexité, analyse de propriétés des langages et des algorithmes) jusqu’au développement de logiciels (appelés solveurs) permettant de résoudre en pratique les problèmes abordés.
Parmi les thèmes de recherche de l’axe « Contraintes », on trouve :
- le développement de langages généraux de modélisation et des outils associés
- la conception de mécanismes efficaces de parcours de l’espace de recherche
- la conception de mécanismes d’inférences et d’apprentissages au sein de solveurs
- la compilation en amont de problèmes combinatoires afin d’effectuer, a posteriori, de façon efficace, un ensemble de requêtes sur ces derniers.
Au sein de l’axe « Contraintes », le CRIL s’intéresse donc à différentes questions inter-corrélées qui vont de la représentation à la résolution de problèmes combinatoires. Des travaux portent sur l’extension de cadres existants et l’utilisation de techniques issues de SAT, CSP et de formalismes apparentés (pseudo-booléens, formules booléennes quantifiées) pour élargir les champs d’application. Par exemple, de nombreux outils développés dans l’axe sont utilisés pour traiter des problèmes fondamentaux pour l’IA explicable et robuste.
Le développement de solveurs open-source génériques et la résolution de problèmes réels (industriels) font également partie des activités conduites au sein de l’axe.
Membres permanents rattachés principalement à l'axe
| Audemard Gilles co-responsable | Professeur des universités |
| Boussemart Frédéric | Maître de conférences |
| Capelli Florent | Chaire de professeur junior |
| Chmeiss Assef | Maître de conférences |
| Grégoire Éric | Professeur des universités |
| Hemery Fred | Maître de conférences |
| Lagniez Jean-Marie co-responsable | Professeur des universités |
| Le Berre Daniel | Professeur des universités |
| Lecoutre Christophe | Professeur des universités |
| Mazure Bertrand | Professeur des universités |
| Mengel Stefan | Chargé de recherche CNRS |
| Parrain Anne | Maîtresse de conférences |
| Piette Cédric | Maître de conférences |
| Roussel Olivier | Maître de conférences |
| Tabary Sébastien | Maître de conférences |
| Wallon Romain | Maître de conférences |
Autres membres rattachés à l'axe
| Bouraoui Zied | Maître de conférences, habilité à diriger des recherches |
| Condotta Jean-François | Professeur des universités |
| Crowley Daniel | Doctorant |
| de Lima Tiago | Maître de conférences, habilité à diriger des recherches |
| Delorme Fabien | Ingénieur de recherche |
| D'halluin Cyrille | PAST |
| Ing David | Doctorant |
| Jabbour Saïd | Professeur des universités |
| Kemgue Alain Trésor | Ingénieur de recherche |
| Koriche Frédéric | Professeur des universités |
| Le Duc Anh | Doctorant |
| Lens Clément | Doctorant |
| Lonca Emmanuel | Ingénieur de recherche |
| Marquis Pierre | Professeur des universités |
| Paris Nicolas | PAST |
| Peltre Olivier | Postdoc |
| Saïs Lakhdar | Professeur des universités |
| Salhi Yakoub | Professeur des universités |
| Samy Modeliar Mouny | PRAG |
| Tahil Gökhan | Doctorant |
Thèses en cours
- New Optimization Techniques for Cross-Docking - Amna Altaf
- Prise en compte des courbes d'apprentissage dans l’équilibrage des chaînes d’assemblage en aéronautique - Duc Anh Le
- SAT-based Approaches for Formal Verification with B method - Daniel Crowley
Thèses soutenues :
Logiciels :
Projets récents :
Données issues de nos recherches :
Publications
Articles de revues internationales
2023 Johannes Fichte, Daniel Le Berre, Markus Hecher, Stefan Szeider, The Silent (R)evolution of SAT
in Communications of the ACM, vol. 66, n° 6, pp. 64-72, 2023.
2023 Emir Demirović, Katsumi Inoue, Jean-Marie Lagniez, Nicolas Schwind, Algorithms for partially robust team formation
in Autonomous Agents and Multi-Agent Systems, vol. 37, n° 2, pp. 22, 2023.
2023 Alexis de Colnet, Stefan Mengel, Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
in Journal of Artificial Intelligence Research, vol. 76, pp. 265-286, 2023.
2022 Xhevahire Tërnava, Johann Mortara, Philippe Collet, Daniel Le Berre, Identification and visualization of variability implementations in object-oriented variability-rich systems: a symmetry-based approach
in Automated Software Engineering, pp. 1-52, 2022.
2022 Stefan Mengel, No Efficient Disjunction or Conjunction of Switch-Lists
in Journal on Satisfiability, Boolean Modeling and Computation, vol. 13, n° 1, pp. 1-4, 2022.
2022 Amna Altaf, Adnen El Amraoui, Francois Delmotte, Christophe Lecoutre, Applications of Artificial Intelligence in Cross Docking: A Systematic Literature Review
in Journal of Computer Information Systems, vol. 63, n° 5, pp. 1-21, 2022.
2021 Stefan Mengel, Sebastian Skritek, Characterizing Tractability of Simple Well-Designed Pattern Trees with Projection
in Theory of Computing Systems, vol. 65, n° 1, pp. 3-41, 2021.
2021 Stefan Mengel, Antoine Amarilli, Pierre Bourhis, Matthias Niewerth, Constant-Delay Enumeration for Nondeterministic Document Spanners
in ACM Transactions on Database Systems, vol. 46, n° 1, pp. 1-30, 2021.
2020 Jean-Marie Lagniez, Emmanuel Lonca, Pierre Marquis, Definability for model counting
in Artificial Intelligence, vol. 281, pp. 103229, 2020.
2020 Gilles Audemard, Frédéric Boussemart, Christophe Lecoutre, Cédric Piette, Olivier Roussel, XCSP3 and its ecosystem
in Constraints Journal (Constraints), pp. 1-23, 2020.
2020 Stefan Mengel, Romain Wallon, Graph Width Measures for CNF-Encodings with Auxiliary Variables
in Journal of Artificial Intelligence Research, vol. 67, pp. 409-436, 2020.
2020 Said Jabbour, Nizar Mhadhbi, Badran Raddaoui, Lakhdar Saïs, SAT-based models for overlapping community detection in networks
in Computing, 2020.
2020 Michael Sioutis, Anastasia Paparrizou, Tomi Janhunen, On Neighbourhood Singleton-style Consistencies for Qualitative Spatial and Temporal Reasoning
in Information and Computation, 2020.
2019 Kahina Bouchama, Arnaud Lallouet, Mohammed Said Radjef, Lakhdar Saïs, Solving a Potential Clustering Game
in International Journal on Artificial Intelligence Tools, vol. 28, n° 02, pp. 1950006, 2019.
2019 Mike Behrisch, Miki Hermann, Stefan Mengel, Gernot Salzer, Minimal Distance of Propositional Models
in Theory of Computing Systems, vol. 63, n° 6, pp. 1131-1184, 2019.
2018 Éric Grégoire, Yacine Izza, Du Zhang, On Admissible Consensuses
in International Journal on Artificial Intelligence Tools (IJAIT), vol. 27, n° 1, pp. 1-20, 2018.
2018 Stefan Mengel, Lower bounds on the mim-width of some graph classes
in Discrete Applied Mathematics, vol. 248, pp. 28-32, 2018.
2018 Daniel Le Berre, Pascal Rapicault, Boolean-Based Dependency Management for the Eclipse Ecosystem
in International Journal on Artificial Intelligence Tools, vol. 27, n° 01, pp. 1840003, 2018.
2018 Saïd Jabbour, Jerry Lonlac, Lakhdar Saïs, Yakoub Salhi, Revisiting the Learned Clauses Database Reduction Strategies
in International Journal on Artificial Intelligence Tools, vol. 27, n° 08, pp. 1850033, 2018.
2018 Gilles Audemard, Laurent Simon, On the Glucose SAT solver
in International Journal on Artificial Intelligence Tools (IJAIT), vol. 27, n° 1, pp. 1-25, 2018.
2018 Éric Grégoire, Jean-Marie Lagniez, Du Zhang, Consensus-finding that preserves mutually conflicting hypothetical information from a same agent
in AI Communications, vol. 31, n° 3, pp. 303-317, 2018.
Articles de conférences internationales
2023 Amna Altaf, Adnen El Amraoui, Francois Delmotte, Christophe Lecoutre, Optimization of Temporary Storage in Cross Docking Facilities: A Mathematical Model
in 2023 7th International Conference on Automation, Control and Robots (ICACR), IEEE, pp. 147-150, 2023.
2023 Stefan Mengel, Bounds on BDD-Based Bucket Elimination
in 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, vol. 271, pp. 16:1--16:11, 2023.
2023 Jean-Marie Lagniez, Pierre Marquis, Boosting Definability Bipartition Computation Using SAT Witnesses
in The 18th European Conference on Logics in Artificial Intelligence (JELIA'23), Springer Nature Switzerland, vol. 14281, pp. 697-711, 2023.
2023 Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura, SAT-Based Method for Finding Attractors in Asynchronous Multi-Valued Networks
in 14th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS 2023), SCITEPRESS, 2023.
2023 Takehide Soh, Morgan Magnin, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura, SAF: SAT-based Attractor Finder in Asynchronous Automata Networks
in 21st International Conference on Computational Methods in Systems Biology (CMSB 2023), 2023.
2023 Gilles Audemard, Christophe Lecoutre, Charles Prud'Homme, Guiding Backtrack Search by Tracking Variables During Constraint Propagation
in International Conference on Principles and Practice of Constraint Programming (CP'23), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
2022 Gilles Audemard, Jean-Marie Lagniez, Marie Miceli, Olivier Roussel, Identifying Soft Cores in Propositional Formulae
in 14th International Conference on Agents and Artificial Intelligence, ICAART, 2022.
2022 Stefan Mengel, Changing Partitions in Rectangle Decision Lists
in 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), vol. 236, pp. 17:1--17:20, 2022.
2022 Frederic Koriche, Christophe Lecoutre, Anastasia Paparrizou, Hugues Wattez, Best Heuristic Identification for Constraint Satisfaction
in 31st International Joint Conference on Artificial Intelligence (IJCAI'22), International Joint Conferences on Artificial Intelligence Organization, pp. 1859-1865, 2022.
2022 Stefan Mengel, Alexis de Colnet, Lower Bounds on Intermediate Results in Bottom-Up Knowledge Compilation
in Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, vol. 36, pp. 5564-5572, 2022.
2022 Gilles Audemard, Jean-Marie Lagniez, Marie Miceli, A New Exact Solver for (Weighted) Max#SAT
in International Conference on Theory and Applications of Satisfiability Testing (SAT), 2022.
2022 Sonia Haddad-Vanier, Romain Wallon, Hugues Wattez, Exploring AI approaches to improve the resolution of unsplittable multicommodity flow problems in wireless networks
in 39th Spanish Conference on Statistics and Operation Research (SEIO'22), 2022.
2022 Alexis de Colnet, Pierre Marquis, On the Complexity of Enumerating Prime Implicants from Decision-DNNF Circuits
in Thirty-First International Joint Conference on Artificial Intelligence {IJCAI-22}, International Joint Conferences on Artificial Intelligence Organization, pp. 2583-2590, 2022.
2021 Stefan Mengel, Friedrich Slivovsky, Proof Complexity of Symbolic QBF Reasoning
in 24th International Conference Theory and Applications of Satisfiability Testing (SAT 2021), Springer International Publishing, vol. 12831, pp. 399-416, 2021.
2021 Ikram Nekkache, Said Jabbour, Lakhdar Sais, Nadjet Kamel, Towards a Compact SAT-Based Encoding of Itemset Mining Tasks
in Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 18th International Conference (CPAIOR 2021), Springer International Publishing, vol. 12735, pp. 163-178, 2021.
2021 Stefan Mengel, Alexis de Colnet, Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
in 24th International Conference Theory and Applications of Satisfiability Testing - SAT 2021, Springer International Publishing, vol. 12831, pp. 116-133, 2021.
2021 Nicolas Szczepanski, Gilles Audemard, Laetitia Jourdan, Christophe Lecoutre, Lucien Mousin, Nadarajen Veerapen, A hybrid CP/MOLS approach for multi-objective imbalanced classification
in GECCO '21: Genetic and Evolutionary Computation Conference, ACM, pp. 723-731, 2021.
2021 Daniel Le Berre, Romain Wallon, On Dedicated CDCL Strategies for PB Solvers
in 24th International Conference on Theory and Applications of Satisfiability Testing (SAT'21), pp. 315-331, 2021.
2021 Nicolas Schwind, Emir Demirović, Jean-Marie Lagniez, Katsumi Inoue, Partial Robustness in Team Formation: Bridging the Gap between Robustness and Resilience
in International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2021.
2021 Florent Capelli, Jean-Marie Lagniez, Pierre Marquis, Certifying Top-Down Decision-DNNF Compilers
in AAAI 2021 - 35th Conference on Artificial Intelligence, 2021.
2021 Alexis de Colnet, Stefan Mengel, A Compilation of Succinctness Results for Arithmetic Circuits
in 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, 2021.
2020 Alexis de Colnet, Stefan Mengel, Lower Bounds for Approximate Knowledge Compilation
in Twenty-Ninth International Joint Conference on Artificial Intelligence and Seventeenth Pacific Rim International Conference on Artificial Intelligence {IJCAI-PRICAI-20}, International Joint Conferences on Artificial Intelligence Organization, pp. 1834-1840, 2020.
2020 Daniel Le Berre, Pierre Marquis, Stefan Mengel, Romain Wallon, On Irrelevant Literals in Pseudo-Boolean Constraint Learning
in 29th International Joint Conference on Artificial Intelligence (IJCAI'20), International Joint Conferences on Artificial Intelligence Organization, pp. 1148-1154, 2020.
2020 Gilles Audemard, Loïc Paulevé, Laurent Simon, SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers
in SAT 2020, The 23rd International Conference on Theory and Applications of Satisfiability Testing, Springer, vol. 12178, pp. 107-113, 2020.
2020 Gilles Audemard, Christophe Lecoutre, Mehdi Maamar, Segmented Tables: an Efficient Modeling Tool for Constraint Reasoning
in 24th European Conference on Artificial Intelligence (ECAI'20), 2020.
2020 Gael Glorian, Jean-Marie Lagniez, Christophe Lecoutre, NACRE - A Nogood And Clause Reasoning Engine
in 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'23), pp. 249-259, 2020.
2020 Alexis de Colnet, A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
in Theory and Applications of Satisfiability Testing – SAT 2020, 2020.
2020 Quentin Cohen-Solal, Minimality of Combined Qualitative Constraint Networks
in ECAI 2020 - 24th European Conference on Artificial Intelligence, 2020.
2020 Zied Bouraoui, Jean-Marie Lagniez, Pierre Marquis, Valentin Montmirail, Consolidating Modal Knowledge Bases
in 24th European Conference on Artificial Intelligence (ECAI'20), 2020.
2020 Daniel Le Berre, Pierre Marquis, Romain Wallon, On Weakening Strategies for PB Solvers
in 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT'20), pp. 322-331, 2020.
2020 Anastasia Paparrizou, Hugues Wattez, Perturbing Branching Heuristics in Constraint Solving
in 26th International Conference on Principles and Practice of Constraint Programming (CP'20), vol. 12333,, 2020.
2020 Hugues Wattez, Frédéric Koriche, Christophe Lecoutre, Anastasia Paparrizou, Sébastien Tabary, Learning Variable Ordering Heuristics with Multi-Armed Bandits and Restarts
in ECAI 2020 - 24th European Conference on Artificial Intelligence, 2020.
2019 Cédric Piette, Eric Piette, Matthew Stephenson, Dennis Soemers, Cameron Browne, Ludii and XCSP: Playing and Solving Logic Puzzles
in IEEE Conferences on Games (COG'19), 2019.
2019 Michael Sioutis, Anastasia Paparrizou, Tomi Janhunen, On the Utility of Neighbourhood Singleton-Style Consistencies for Qualitative Constraint-Based Spatial and Temporal Reasoning.
in 26th International Symposium on Temporal Representation and Reasoning (TIME 2019), 2019.
2019 Hugues Wattez, Christophe Lecoutre, Anastasia Paparrizou, Sébastien Tabary, Refining Constraint Weighting
in ICTAI 2019: IEEE 31st International Conference on Tools with Artificial Intelligence, 2019.
2019 Florent Capelli, Stefan Mengel, Tractable QBF by Knowledge Compilation
in 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019), 2019.
2019 Gael Glorian, Jean-Marie Lagniez, Valentin Montmirail, Nicolas Szczepanski, An Incremental SAT-Based Approach for Graph Colouring Problem
in The 25th International Conference on Principles and Practice of Constraint Programming (CP'19), 2019.
2019 Gilles Audemard, Gael Glorian, Jean-Marie Lagniez, Valentin Montmirail, Nicolas Szczepanski, pFactory: A generic library for designing parallel solvers
in International Conference on Applied Computing (AC), 2019.
2019 Jean-Marie Lagniez, Pierre Marquis, A Recursive Algorithm for Projected Model Counting
in 33rd AAAI Conference on Artificial Intelligence (AAAI'19), 2019.
2019 Hélène Verhaeghe, Christophe Lecoutre, Pierre Schaus, Extending Compact-Diagram to Basic Smart Multi-Valued Variable Diagrams
in CPAIOR, Springer International Publishing, vol. 11494, pp. 581-598, 2019.
2019 Antoine Amarilli, Pierre Bourhis, Stefan Mengel, Matthias Niewerth, Enumeration on Trees with Tractable Combined Complexity and Efficient Updates
in PODS, ACM Press, pp. 89-103, 2019.
2019 Stefan Mengel, Romain Wallon, Revisiting Graph Width Measures for CNF-Encodings
in 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT'19), pp. 222-238, 2019.
2018 Minh Thanh Khong, Christophe Lecoutre, Pierre Schaus, Yves Deville, Soft-Regular with a Prefix-Size Violation Measure
in CPAIOR, Springer International Publishing, vol. 10848, pp. 333-343, 2018.
2018 Michael Lampis, Stefan Mengel, Valia Mitsou, QBF as an Alternative to Courcelle’s Theorem
in 21st International Conference on Theory and Applications of Satisfiability Testing – SAT 2018, pp. 235-252, 2018.
2018 Hélène Verhaeghe, Christophe Lecoutre, Pierre Schaus, Compact-MDD: Efficiently Filtering (s)MDD Constraints with Reversible Sparse Bit-sets
in Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}, International Joint Conferences on Artificial Intelligence Organization, pp. 1383-1389, 2018.
2018 Gael Glorian, Jean-Marie Lagniez, Valentin Montmirail, Michael Sioutis, An Incremental SAT-Based Approach to Reason Efficiently On Qualitative Constraint Network
in 24th International Conference on Principles and Practice of Constraint Programming (CP'18), Springer, pp. 160--178, 2018.
2018 Noureddine Aribi, Mehdi Maamar, Nadjib Lazaar, Yahia Lebbah, Samir Loudni, Multiple Fault Localization Using Constraint Programming and Pattern Mining
in IEEE 29th International Conference on Tools with Artificial Intelligence (ICTAI), IEEE, pp. 860-867, 2018.
2018 Gael Glorian, Jean-Marie Lagniez, Valentin Montmirail, Michael Sioutis, An Incremental SAT-Based Approach to Reason Efficiently on Qualitative Constraint Networks
in 24th International Conference on Principles and Practice of Constraint Programming (CP'18), pp. 160-178, 2018.
2018 Jean-Marie Lagniez, Pierre Marquis, Nicolas Szczepanski, DMC: A Distributed Model Counter
in 27th International Joint Conference on Artificial Intelligence (IJCAI'18), pp. 1331-1338, 2018.
2018 Daniel Le Berre, Pierre Marquis, Stefan Mengel, Romain Wallon, Pseudo-Boolean Constraints from a Knowledge Representation Perspective
in 27th International Joint Conference on Artificial Intelligence (IJCAI'18), International Joint Conferences on Artificial Intelligence Organization, pp. 1891-1897, 2018.
2018 Christian Bessiere, Nadjib Lazaar, Mehdi Maamar, User's Constraints in Itemset Mining
in CP 2018 - 24th International Conference on Principles and Practice of Constraint Programming, vol. 11008, pp. 537-553, 2018.
2018 Éric Grégoire, Yacine Izza, Jean-Marie Lagniez, Boosting MCSes enumeration
in 27th International Joint Conference on Artificial Intelligence (IJCAI'18), pp. 1309-1315, 2018.
2018 Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail, A SAT-Based Approach For PSPACE Modal Logics
in Principles of Knowledge Representation and Reasoning: Sixteenth International Conference, 2018.
2018 Abdelhamid Boudane, Saïd Jabbour, Badran Raddaoui, Lakhdar Saïs, Efficient SAT-based encodings of conditional cardinality constraints
in LPAR-22 2018: 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, EPiC Series in Computing, vol. 57, pp. 181 - 195, 2018.
2018 Said Jabbour, Nizar Mhadhbi, Badran Raddaoui, Lakhdar Saïs, Triangle-Driven Community Detection in Large Graphs Using Propositional Satisfiability
in 2018 IEEE 32nd International Conference on Advanced Information Networking and Applications (AINA), IEEE, pp. 437-444, 2018.
2018 Saïd Jabbour, Nizar Mhadhbi, Badran Raddaoui, Lakhdar Saïs, Detecting highly overlapping community structure by model-based maximal clique expansion
in BigData 2018: IEEE international conference on Big Data, IEEE Computer Society, pp. 1031 - 1036, 2018.
2018 Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail, An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem
in Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, pp. 1-18, 2018.
2018 Saïd Jabbour, Nizar Mhadhbi, Badran Raddaoui, Lakhdar Saïs, Pushing the envelope in overlapping communities detection
in IDA 2018: 17th international symposium on Intelligent Data Analysis, Springer, pp. 151 - 163, 2018.
Éditions d'actes de conférences et d'ouvrages
2018 Youssef Hamadi, Lakhdar Saïs, Handbook of Parallel Constraint Reasoning
Springer International Publishing, 2018.
Chapitres d'ouvrages
2021 Olivier Roussel, Vasco Manquinho, Pseudo-Boolean and Cardinality Constraints
in Handbook of Satisfiability, second edition, vol. 336, pp. 1087-1129, IOS Press, 2021.