Document Open Access Logo

Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability (Short Paper)

Authors Sami Cherif , Heythem Sattoutah , Chu-Min Li , Corinne Lucet , Laure Brisoux-Devendeville

PDF
Thumbnail PDF

File

LIPIcs.CP.2024.34.pdf
  • Filesize: 0.67 MB
  • 11 pages

Document Identifiers

Author Details

Sami Cherif
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Heythem Sattoutah
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Chu-Min Li
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Corinne Lucet
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Laure Brisoux-Devendeville
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Cite AsGet BibTex

Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville. Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability (Short Paper). In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 34:1-34:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.34

Abstract

This paper explores the application of Maximum Satisfiability (Max-SAT) to the complex problem of conference session scheduling, with a particular focus on minimizing working-group conflicts within the context of the ROADEF conference, the largest French-speaking event aimed at bringing together researchers from various fields such as combinatorial optimization and operational research. A Max-SAT model is introduced then enhanced with new variables, and solved through state-of-the-art solvers. The results of applying our formulation to data from ROADEF demonstrate its ability to effectively compute session schedules, while enabling to reduce the number of conflicts and the maximum number of parallel sessions compared to the handmade solutions proposed by the organizing committees. These findings underscore the potential of Max-SAT as a valuable tool for optimizing conference scheduling processes, offering a systematic and efficient solution that ensures a smoother and more productive experience for attendees and organizers alike.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Planning and scheduling
  • Computing methodologies → Logic programming and answer set programming
Keywords
  • Maximum Satisfiability
  • Scheduling
  • Modeling

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. BDDs for Pseudo-Boolean Constraints - Revisited. In Karem A. Sakallah and Laurent Simon, editors, 14th International Conference on Theory and Applications of Satisfiability Testing - SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, volume 6695 of Lecture Notes in Computer Science, pages 61-75. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_7.
  2. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artif. Intell., 196:77-105, 2013. URL: https://doi.org/10.1016/J.ARTINT.2013.01.002.
  3. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality Networks and Their Applications. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 167-180. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_18.
  4. Roberto Javier Asín Achá and Robert Nieuwenhuis. Curriculum-based course timetabling with SAT and MaxSAT. Ann. Oper. Res., 218(1):71-91, 2014. URL: https://doi.org/10.1007/S10479-012-1081-X.
  5. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. MaxSAT Evaluation 2018: New Developments and Detailed Results. J. Satisf. Boolean Model. Comput., 11(1):99-131, 2019. URL: https://doi.org/10.3233/SAT190119.
  6. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 929-991. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201008.
  7. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified Core-Guided MaxSAT Solving. In Brigitte Pientka and Cesare Tinelli, editors, Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, volume 14132 of Lecture Notes in Computer Science, pages 1-22. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_1.
  8. Jeremias Berg, Antti Hyttinen, and Matti Järvisalo. Applications of MaxSAT in Data Analysis. In Daniel Le Berre and Matti Järvisalo, editors, Proceedings of Pragmatics of SAT 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of SAT 2018, Oxford, UK, July 7, 2018, volume 59 of EPiC Series in Computing, pages 50-64. EasyChair, 2018. URL: https://doi.org/10.29007/3QKH.
  9. A. Biere, M. Heule, and H. van Maaren. Handbook of Satisfiability: Second Edition. Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://books.google.fr/books?id=dUAvEAAAQBAJ.
  10. Miquel Bofill, Marc Garcia, Josep Suy, and Mateu Villaret. MaxSAT-Based Scheduling of B2B Meetings. In Laurent Michel, editor, Integration of AI and OR Techniques in Constraint Programming - 12th International Conference, CPAIOR 2015, Barcelona, Spain, May 18-22, 2015, Proceedings, volume 9075 of Lecture Notes in Computer Science, pages 65-73. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-18008-3_5.
  11. Mohamed Sami Cherif, Djamal Habet, and André Abramé. Understanding the power of max-sat resolution through up-resilience. Artif. Intell., 289:103397, 2020. URL: https://doi.org/10.1016/J.ARTINT.2020.103397.
  12. Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville. ROADEF_SCHEDULING. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:7083377094f69163d37d30b77d740c72c562139d;origin=https://github.com/satoutahhaithem/ROADEF_SCHEDULING;visit=swh:1:snp:c34fc60c52e7d5289f8e1c049ce6ba5e0adc48d2;anchor=swh:1:rev:92a1a45786ba37797dda7d78f7d02347f6f2a0a8 (visited on 2024-08-16). URL: https://github.com/satoutahhaithem/ROADEF_SCHEDULING.
  13. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, volume 6876 of Lecture Notes in Computer Science, pages 225-239. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  14. Emir Demirovic and Nysret Musliu. MaxSAT-based large neighborhood search for high school timetabling. Comput. Oper. Res., 78:172-180, 2017. URL: https://doi.org/10.1016/J.COR.2016.08.004.
  15. Emir Demirovic, Nysret Musliu, and Felix Winter. Modeling and solving staff scheduling with partial weighted maxSAT. Ann. Oper. Res., 275(1):79-99, 2019. URL: https://doi.org/10.1007/S10479-017-2693-Y.
  16. Niklas Eén and Niklas Sörensson. Translating Pseudo-Boolean Constraints into SAT. J. Satisf. Boolean Model. Comput., 2(1-4):1-26, 2006. URL: https://doi.org/10.3233/SAT190014.
  17. Alexey Ignatiev, António Morgado, and João Marques-Silva. PySAT: A Python Toolkit for Prototyping with SAT Oracles. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  18. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an Efficient MaxSAT Solver. J. Satisf. Boolean Model. Comput., 11(1):53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  19. Gerold Jäger, Sharlee Climer, and Weixiong Zhang. The complete parsimony haplotype inference problem and algorithms based on integer programming, branch-and-bound and Boolean satisfiability. J. Discrete Algorithms, 37:68-83, 2016. URL: https://doi.org/10.1016/J.JDA.2016.06.001.
  20. Alexandre Lemos, Filipe Gouveia, Pedro T. Monteiro, and Inês Lynce. Iterative Train Scheduling under Disruption with Maximum Satisfiability. J. Artif. Intell. Res., 79:1047-1090, 2024. URL: https://doi.org/10.1613/JAIR.1.14924.
  21. Chu Min Li and Felip Manyà. MaxSAT, Hard and Soft Constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 903-927. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201007.
  22. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining clause learning and branch and bound for maxsat. In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs, pages 38:1-38:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CP.2021.38.
  23. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Boosting branch-and-bound MaxSAT solvers with clause learning. AI Commun., 35(2):131-151, 2022. URL: https://doi.org/10.3233/AIC-210178.
  24. Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, and Wenxin Yu. Maximum Satisfiability Formulation for Optimal Scheduling in Overloaded Real-Time Systems. In Abhaya C. Nayak and Alok Sharma, editors, PRICAI 2019: Trends in Artificial Intelligence - 16th Pacific Rim International Conference on Artificial Intelligence, Cuvu, Yanuca Island, Fiji, August 26-30, 2019, Proceedings, Part I, volume 11670 of Lecture Notes in Computer Science, pages 618-631. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29908-8_49.
  25. Hratch Mangassarian, Andreas G. Veneris, and Farid N. Najm. Maximum circuit activity estimation using pseudo-boolean satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 31(2):271-284, 2012. URL: https://doi.org/10.1109/TCAD.2011.2169259.
  26. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-WBO: A Modular MaxSAT Solver. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 438-445. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_33.
  27. António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints An Int. J., 18(4):478-534, 2013. URL: https://doi.org/10.1007/S10601-013-9146-2.
  28. Laurent Perron and Frédéric Didier. Cp-sat. URL: https://developers.google.com/optimization/cp/cp_solver/.
  29. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Proofs and Certificates for Max-SAT. J. Artif. Intell. Res., 75:1373-1400, 2022. URL: https://doi.org/10.1613/JAIR.1.13811.
  30. Olivier Roussel and Vasco M. Manquinho. Pseudo-Boolean and Cardinality Constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1087-1129. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201012.
  31. Ahmad Shabani and Bijan Alizadeh. PMTP: A MAX-SAT-Based Approach to Detect Hardware Trojan Using Propagation of Maximum Transition Probability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 39(1):25-33, 2020. URL: https://doi.org/10.1109/TCAD.2018.2889663.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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