2026-08-06T04:25:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23753 2025-11-12T13:00:10Z ddc:004 open_access

An Application of SAT Solvers in Integer Programming Games Koirala, Pravesh Shrey, Aditya Laine, Forrest Game Theory Integer Programming Games SAT Solvers Local Solutions Graph Games 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pravesh Koirala and Aditya Shrey and Forrest Laine 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.19 urn:nbn:de:0030-drops-237534 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.19 eng https://creativecommons.org/licenses/by/4.0/legalcode