LIPIcs.CP.2024.37.pdf
- Filesize: 0.66 MB
- 11 pages
Document
Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries (Short Paper)
Authors
Markus Kirchweger 
,
Stefan Szeider
-
Part of:
Volume:
30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Principles and Practice of Constraint Programming (CP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-08-29
File
Document Identifiers
Author Details
Cite As Get BibTex
Markus Kirchweger and Stefan Szeider. Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries (Short Paper). In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 37:1-37:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.37
Abstract
Envy-freeness up to any good (EFX) is a key concept in Computational Social Choice for the fair division of indivisible goods, where no agent envies another’s allocation after removing any single item. A deeper understanding of EFX allocations is facilitated by exploring the rainbow cycle number (R_f(d)), the largest number of independent sets in a certain class of directed graphs. Upper bounds on R_f(d) provide guarantees to the feasibility of EFX allocations (Chaudhury et al., EC 2021). In this work, we precisely compute the numbers R_f(d) for small values of d, employing the SAT modulo Symmetries framework (Kirchweger and Szeider, CP 2021). SAT modulo Symmetries is tailored specifically for the constraint-based isomorph-free generation of combinatorial structures. We provide an efficient encoding for the rainbow cycle number, comparing eager and lazy approaches. To cope with the huge search space, we extend the encoding with invariant pruning, a new method that significantly speeds up computation.
Subject Classification
ACM Subject Classification
- Mathematics of computing → Extremal graph theory
- Software and its engineering → Constraint and logic languages
- Hardware → Theorem proving and SAT solving
- Mathematics of computing → Graph enumeration
Keywords
- EFX
- rainbow cycle number
- SAT modulo Symmetries
- combinatorial search
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Hannaneh Akrami, Bhaskar Ray Chaudhury, Jugal Garg, Kurt Mehlhorn, and Ruta Mehta. EFX allocations: Simplifications and improvements. CoRR, abs/2205.07638, 2022. URL: https://doi.org/10.48550/arXiv.2205.07638.
- Georgios Amanatidis, Evangelos Markakis, and Apostolos Ntokos. Multiple birds with one stone: Beating 1/2 for EFX and GMMS via envy cycle elimination. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 1790-1797. AAAI Press, 2020. URL: https://doi.org/10.1609/AAAI.V34I02.5545.
- Benjamin Aram Berendsohn, Simona Boyadzhiyska, and László Kozma. Fixed-point cycles and approximate EFX allocations. In 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume 241 of LIPIcs, pages 17:1-17:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.MFCS.2022.17.
- Ben Berger, Avi Cohen, Michal Feldman, and Amos Fiat. Almost full EFX exists for four agents. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, pages 4826-4833. AAAI Press, 2022. URL: https://doi.org/10.1609/AAAI.V36I5.20410.
- Ioannis Caragiannis, David Kurokawa, Hervé Moulin, Ariel D. Procaccia, Nisarg Shah, and Junxing Wang. The unreasonable fairness of maximum Nash welfare. ACM Trans. Economics and Comput., 7(3):12:1-12:32, 2019. URL: https://doi.org/10.1145/3355902.
- Bhaskar Ray Chaudhury, Jugal Garg, and Kurt Mehlhorn. EFX exists for three agents. J. ACM, 71(1):4:1-4:27, 2024. URL: https://doi.org/10.1145/3616009.
- Bhaskar Ray Chaudhury, Jugal Garg, Kurt Mehlhorn, Ruta Mehta, and Pranabendu Misra. Improving EFX guarantees through rainbow cycle number. In EC '21: The 22nd ACM Conference on Economics and Computation, Budapest, Hungary, July 18-23, 2021, pages 310-311. ACM, 2021. URL: https://doi.org/10.1145/3465456.3467605.
- Bhaskar Ray Chaudhury, Telikepalli Kavitha, Kurt Mehlhorn, and Alkmini Sgouritsa. A little charity guarantees almost envy-freeness. SIAM J. Comput., 50(4):1336-1358, 2021. URL: https://doi.org/10.1137/20M1359134.
- Michael Codish, Graeme Gange, Avraham Itzhakov, and Peter J. Stuckey. Breaking symmetries in graphs: The nauty way. In Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, volume 9892 of Lecture Notes in Computer Science, pages 157-172. Springer Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-44953-1_11.
- Michael Codish, Alice Miller, Patrick Prosser, and Peter J. Stuckey. Constraints for symmetry breaking in graph representation. Constraints, 24(1):1-24, 2019. URL: https://doi.org/10.1007/s10601-018-9294-5.
- Jo Devriendt, Bart Bogaerts, Broes De Cat, Marc Denecker, and Christopher Mears. Symmetry propagation: Improved dynamic symmetry breaking in SAT. In IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, Athens, Greece, November 7-9, 2012, pages 49-56. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/ICTAI.2012.16.
- Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: user propagators for CDCL. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 8:1-8:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.8.
- Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere. Certifying incremental SAT solving. In LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024, volume 100 of EPiC Series in Computing, pages 321-340. EasyChair, 2024. URL: https://doi.org/10.29007/PDCC.
- Marijn J. H. Heule. The DRAT format and DRAT-trim checker. CoRR, abs/1610.06229, 2016. URL: http://arxiv.org/abs/1610.06229.
- Marijn J. H. Heule. Optimal symmetry breaking for graph problems. Math. Comput. Sci., 13(4):533-548, 2019. URL: https://doi.org/10.1007/S11786-019-00397-5.
- Avraham Itzhakov and Michael Codish. Breaking symmetries with high dimensional graph invariants and their combination. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 20th International Conference, CPAIOR 2023, Nice, France, May 29 - June 1, 2023, Proceedings, volume 13884 of Lecture Notes in Computer Science, pages 133-149. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-33271-5_10.
- Shayan Chashm Jahan, Masoud Seddighin, Seyed Mohammad Seyed Javadi, and Mohammad Sharifi. Rainbow cycle number and EFX allocations: (almost) closing the gap. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 2572-2580. ijcai.org, 2023. URL: https://doi.org/10.24963/IJCAI.2023/286.
- Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. Co-certificate learning with SAT modulo symmetries. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 1944-1953. ijcai.org, 2023. URL: https://doi.org/10.24963/IJCAI.2023/216.
- Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. A SAT attack on Rota’s Basis Conjecture. In Theory and Applications of Satisfiability Testing - SAT 2022 - 25th International Conference, Haifa, Israel, August 2-5, 2022, Proceedings, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.4.
- Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. SAT-based generation of planar graphs. In Meena Mahajan and Friedrich Slivovsky, editors, The 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), July 04-08, 2023, Alghero, Italy, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.14.
- Markus Kirchweger and Stefan Szeider. SAT modulo symmetries for graph generation and enumeration. ACM Trans. Comput. Log., 25(3), 2024. URL: https://doi.org/10.1145/3670405.
-
Hans Kleine Büning and Theodor Lettman. Propositional logic: deduction and algorithms. Cambridge University Press, Cambridge, 1999.
- Tamás Mészáros and Raphael Steiner. Zero sum cycles in complete digraphs. Eur. J. Comb., 98:103399, 2021. URL: https://doi.org/10.1016/J.EJC.2021.103399.
- Hakan Metin, Souheib Baarir, Maximilien Colange, and Fabrice Kordon. CDCLSym: introducing effective symmetry breaking in SAT solving. In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, volume 10805 of Lecture Notes in Computer Science, pages 99-114. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89960-2_6.
- Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing - SAT 2014, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer Verlag, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.