Document Open Access Logo

An Application of SAT Solvers in Integer Programming Games

Authors Pravesh Koirala , Aditya Shrey, Forrest Laine

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.19.pdf
  • Filesize: 0.75 MB
  • 12 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.19.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Algorithmic game theory and mechanism design
  • Security and privacy → Network security
Keywords
  • Game Theory
  • Integer Programming Games
  • SAT Solvers
  • Local Solutions
  • Graph Games

Metrics

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

Abstract

Integer programming games (IPGs) are a popular game-theoretic tool to model an array of games where each player has a discrete strategy set. These games arise in important domains such as economics, transportation, cybersecurity, etc., but solving them is non-trivial as it is known that checking for the existence of pure Nash equilibria in an IPG is Σ₂^p-complete. Recent works have proposed a class of relaxed solution concepts for IPGs called locally optimal integer solutions (LOIS) and shown it to be an efficient alternative for pure Nash equilibria. While LOIS are significantly simpler to compute, they still do not scale when solved using traditional mathematical solvers, especially when high-quality solutions are desired. In this paper, we apply commercially available SAT solvers to find LOIS in IPGs. We investigate efficient encodings for a cybersecurity game and compare solution times when using SAT solvers vs mathematical program solvers. We also investigate the application of SAT solvers in graph games using a graph interdiction example and compare against the obtained LOI solutions against existing heuristics-based solutions. Our results indicate that with appropriate encodings, large-scale IPGs can be solved much more efficiently using SAT solvers. We also show that SAT solvers can be applied to graph games in conjunction with LOIS for obtaining high-quality solutions. Our results emphasize the potential of SAT solvers combined with LOIS to solve significant game theory problems.

Cite As Get BibTex

Pravesh Koirala, Aditya Shrey, and Forrest Laine. An Application of SAT Solvers in Integer Programming Games. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 19:1-19:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.19

Author Details

Pravesh Koirala
  • Department of Computer Science, Vanderbilt University, Nashville, TN, USA
Aditya Shrey
  • Department of Computer Science, Vanderbilt University, Nashville, TN, USA
Forrest Laine
  • Department of Computer Science, Vanderbilt University, Nashville, TN, USA

Supplementary Materials

References

  1. Tobias Achterberg. Scip: solving constraint integer programs. Mathematical Programming Computation, 1:1-41, 2009. URL: https://doi.org/10.1007/S12532-008-0001-1.
  2. Sahel Alouneh, Sa’ed Abed, Mohammad H Al Shayeji, and Raed Mesleh. A comprehensive study and analysis on sat-solvers: advances, usages and achievements. Artificial Intelligence Review, 52:2575-2601, 2019. URL: https://doi.org/10.1007/S10462-018-9628-0.
  3. Andrea Baggio, Margarida Carvalho, Andrea Lodi, and Andrea Tramontani. Multilevel approaches for the critical node problem. Operations Research, 69(2):486-508, 2021. URL: https://doi.org/10.1287/OPRE.2020.2014.
  4. Elise Bonzon, Marie-Christine Lagasquie-Schiex, Jérôme Lang, and Bruno Zanuttini. Boolean games revisited. In ECAI, volume 141, pages 265-269, 2006. URL: http://www.booksonline.iospress.nl/Content/View.aspx?piid=1688.
  5. Haitze J Broersma and Cornelis Hoede. Path graphs. Journal of graph theory, 13(4):427-444, 1989. URL: https://doi.org/10.1002/JGT.3190130406.
  6. Margarida Carvalho, Gabriele Dragotto, Andrea Lodi, and Sriram Sankaranarayanan. The cut-and-play algorithm: Computing nash equilibria via outer approximations. arXiv preprint arXiv:2111.05726, 2021. URL: https://arxiv.org/abs/2111.05726.
  7. Margarida Carvalho, Gabriele Dragotto, Andrea Lodi, and Sriram Sankaranarayanan. Integer programming games: a gentle computational overview. In Tutorials in Operations Research: Advancing the Frontiers of OR/MS: From Methodologies to Applications, pages 31-51. INFORMS, 2023. Google Scholar
  8. Margarida Carvalho, Andrea Lodi, and João P Pedroso. Computing equilibria for integer programming games. European Journal of Operational Research, 303(3):1057-1070, 2022. URL: https://doi.org/10.1016/J.EJOR.2022.03.048.
  9. Vincent Conitzer and Tuomas Sandholm. A technique for reducing normal-form games to compute a nash equilibrium. In Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, pages 537-544, 2006. URL: https://doi.org/10.1145/1160633.1160731.
  10. Tobias Crönert and Stefan Minner. Location selection for hydrogen fuel stations under emerging provider competition. Transportation Research Part C: Emerging Technologies, 133:103426, 2021. Google Scholar
  11. Tobias Crönert and Stefan Minner. Equilibrium identification and selection in finite games. Operations Research, 72(2):816-831, 2024. URL: https://doi.org/10.1287/OPRE.2022.2413.
  12. Sofie De Clercq, Kim Bauters, Steven Schockaert, Mihail Mihaylov, Ann Nowé, and Martine De Cock. Exact and heuristic methods for solving boolean games. Autonomous agents and multi-agent systems, 31:66-106, 2017. URL: https://doi.org/10.1007/S10458-015-9313-5.
  13. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  14. Paramita Dey, Subhayan Bhattacharya, and Sarbani Roy. A survey on the role of centrality as seed nodes for information propagation in large scale network. ACM/IMS Transactions on Data Science, 2(3):1-25, 2021. URL: https://doi.org/10.1145/3465374.
  15. Gabriele Dragotto, Amine Boukhtouta, Andrea Lodi, and Mehdi Taobane. The critical node game. Journal of Combinatorial Optimization, 47(5):74, 2024. URL: https://doi.org/10.1007/S10878-024-01173-3.
  16. Gabriele Dragotto and Rosario Scatamacchia. The zero regrets algorithm: Optimizing over pure nash equilibria via integer programming. INFORMS Journal on Computing, 35(5):1143-1160, 2023. URL: https://doi.org/10.1287/IJOC.2022.0282.
  17. Paul E Dunne and Michael Wooldridge. Towards tractable boolean games. In Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems-Volume 2, pages 939-946, 2012. URL: http://dl.acm.org/citation.cfm?id=2343831.
  18. Niklas Eén, Alexander Legg, Nina Narodytska, and Leonid Ryzhyk. Sat-based strategy extraction in reachability games. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 29(1), 2015. Google Scholar
  19. Severino V Gervacio. Cycle graphs. In Graph Theory Singapore 1983: Proceedings of the First Southeast Asian Graph Theory Colloquium, held in Singapore May 10-28, 1983, pages 279-293. Springer, 1984. Google Scholar
  20. Weiwei Gong and Xu Zhou. A survey of sat solver. In AIP Conference Proceedings, volume 1836(1). AIP Publishing, 2017. Google Scholar
  21. Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2024. URL: https://www.gurobi.com.
  22. Paul Harrenstein, Wiebe van der Hoek, John-Jules Meyer, and Cees Witteveen. Boolean games. In Proceedings of the 8th Conference on Theoretical Aspects of Rationality and Knowledge, pages 287-298, 2001. Google Scholar
  23. Keijo Heljanko, Misa Keinänen, Martin Lange, and Ilkka Niemelä. Solving parity games by a reduction to sat. Journal of Computer and System Sciences, 78(2):430-440, 2012. URL: https://doi.org/10.1016/J.JCSS.2011.05.004.
  24. Qi Huangfu and JA Julian Hall. Parallelizing the dual revised simplex method. Mathematical Programming Computation, 10(1):119-142, 2018. URL: https://doi.org/10.1007/S12532-017-0130-5.
  25. Pravesh Koirala, Mel Krusniak, and Forrest Laine. Locally optimal solutions for integer programming games. arXiv preprint arXiv:2503.20918, 2025. URL: https://doi.org/10.48550/arXiv.2503.20918.
  26. Matthias Köppe, Christopher Thomas Ryan, and Maurice Queyranne. Rational generating functions and integer programming games. Operations research, 59(6):1445-1460, 2011. URL: https://doi.org/10.1287/OPRE.1110.0964.
  27. Alejandro Lamas and Philippe Chevalier. Joint dynamic pricing and lot-sizing under competition. European Journal of Operational Research, 266(3):864-876, 2018. URL: https://doi.org/10.1016/J.EJOR.2017.10.026.
  28. Chu Min Li and Felip Manya. Maxsat, hard and soft constraints. In Handbook of satisfiability, pages 903-927. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201007.
  29. Javier Maass, Vincent Mousseau, and Anaëlle Wilczynski. A hotelling-downs game for strategic candidacy with binary issues. In Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, pages 2076-2084, 2023. URL: https://doi.org/10.5555/3545946.3598881.
  30. Tomasz P Michalak, Karthik V Aadithya, Piotr L Szczepanski, Balaraman Ravindran, and Nicholas R Jennings. Efficient computation of the shapley value for game-theoretic network centrality. Journal of Artificial Intelligence Research, 46:607-650, 2013. URL: https://doi.org/10.1613/JAIR.3806.
  31. Adel Nabli, Margarida Carvalho, and Pierre Hosteins. Complexity of the multilevel critical node problem. Journal of Computer and System Sciences, 127:122-145, 2022. URL: https://doi.org/10.1016/J.JCSS.2022.02.004.
  32. Simone Sagratella. Computing all solutions of nash equilibrium problems with discrete strategy sets. SIAM Journal on Optimization, 26(4):2190-2218, 2016. URL: https://doi.org/10.1137/15M1052445.
  33. Simone Sagratella, Marcel Schmidt, and Nathan Sudermann-Merx. The noncooperative fixed charge transportation problem. European Journal of Operational Research, 284(1):373-382, 2020. URL: https://doi.org/10.1016/J.EJOR.2019.12.024.
  34. Stefan Schwarze and Oliver Stein. A branch-and-prune algorithm for discrete nash equilibrium problems. Computational Optimization and Applications, 86(2):491-519, 2023. URL: https://doi.org/10.1007/S10589-023-00500-4.
  35. Nils Timm, Josua Botha, and Steven Jordaan. Max-sat-based synthesis of optimal and nash equilibrium strategies for multi-agent systems. Science of Computer Programming, 228:102946, 2023. URL: https://doi.org/10.1016/J.SCICO.2023.102946.
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