An Application of SAT Solvers in Integer Programming Games

Integer programming games (IPGs) are well-known in game-theoretic literature [7, 26]. They arise when every player is restricted to choosing discrete strategies and are useful for modeling a plethora of scenarios from domains such as transportation, communication, cybersecurity, etc [10, 15, 27]. While they provide substantial modeling flexibility, they are known to be difficult to solve. It is well-known that deciding whether or not an IPG admits a pure Nash equilibria, a popular solution concept for IPGs, is ${\mathrm{\Sigma }}_2^p$-complete [8]. This poses severe computational challenges and makes solving for large-scale IPGs intractable.

However, recent works have introduced new class of solution concepts for IPGs called locally optimal integer solutions (LOIS) that are more relaxed than PNEs and computationally tractable even for large-scale IPGs [25]. In fact, [25] show that deciding whether IPGs admit LOIS is NP-complete, which means that they can be solved by commercially available mathematical solvers that support integer programming and scale well across large IPG instances. With this relaxed notion of LOIS, many large-scale IPGs that specifically arise in many critical domains, including cybersecurity, become tractable. In particular, in an attacker-defender scenario where there are a large number of cyber infrastructures to be considered with a limited attack/defense budget for both attackers and defenders, the resulting IPG is not readily solvable for large instances using PNE but can indeed be solved using LOIS [25]. Furthermore, a bilevel IPG with a leader-follower structure can also be solved by embedding the LOIS optimality conditions of the follower in the leader’s program to obtain a single integer program. This allows us to solve an important class of cybersecurity games played on graphs, i.e. graph interdiction games, where a defender and an attacker strategically choose nodes to protect and infect while considering the propagation dynamics of the attack on the graph [3]. Despite the scalability of LOIS, they are not without limitations. The most important being that while LOI solutions scale well for lower orders (LOIS-1), higher-order LOI solutions, which are qualitatively better, are time-consuming to calculate due to increased complexity.

SAT solvers that solve the boolean satisfiability problem are known to be effective for solving NP-complete problems from various domains including planning, formal verification, cybersecurity, transportation, etc. [2, 20]. Decades of advances in SAT solving techniques, coupled with rigorous optimizations in commercially available SAT solvers make them attractive for solving any large-scale NP-complete problem. Furthermore, the extension of SAT called MaxSAT [28] adds further modeling flexibility to the SAT language, making it possible to perform an optimization over the number of true clauses. Despite these powerful modeling and solving capabilities, SAT solvers are underutilized for game-theoretic applications and have not been previously considered for solving IPGs.

In this paper, we show that it is possible to utilize modern SAT solvers to solve for LOI solutions for IPGs using straightforward encodings. In particular, we highlight the fact that modern SAT solvers can scale incredibly well in comparison to traditional mathematical optimizers in certain game-theoretic applications. We apply our methods in two cybersecurity games of interest: a) a critical node game first introduced by [15] where attacker and defender simultaneously choose which infrastructures to attack/defend, and b) a bilevel graph interdiction game with constrained propagation dynamics where defender chooses central nodes to defend followed by the attacker choosing their initial targets to spread infection.

Throughout the rest of this paper, we follow the conventions and definitions used by [25].

With definition 1 in place, the pure Nash equilibrium (PNE) of an IPG is defined as:

Since PNE is computationally prohibitive due to them being in ${\mathrm{\Sigma }}_2^p$, [25] introduce the notion of m-order integer neighborhood and subsequently locally optimal integer solution as follows:

By using definition 4, optimality conditions for LOIS can be obtained for a single program as follows:

Finally, using definition 5, the joint optimality condition for a LOIS-m solution for an IPG is defined as:

In simpler terms, a LOIS-m solution for an IPG is defined such that no single player, by unilaterally deviating in their m-order integer neighborhood, can obtain better payoffs (or lower costs) while remaining feasible. In this way, LOIS-m basically offers a direct adaptation of the concept of local equilibria in continuous-strategy games to IPGs. Similarly, when the discrete strategy-set of each player is binary (and the payoff is a logical formula defined over the joint strategy), it is easy to see that LOIS-m for unconstrained IPG in such cases translates to the notion of local equilibria for boolean games. In this regard, LOIS-m is actually a generalization of existing local solution concepts from boolean games.

CNG is a cybersecurity game first introduced by [15]. The following description of CNG is derived from the same and we refer readers to the original text for any missing details. The CNG is played over a set of $V$ critical nodes representing sensitive digital infrastructures with the decision variables $x_i\in \{0,1\},{\alpha }_i\in \{0,1\}\forall i\in V$ indicating respectively the defender and attacker’s choice with $x_i=1$ for defender defending the node $i$ (and zero otherwise), and ${\alpha }_i=1$ for the attacker attacking the target (and zero otherwise). Both players have limited budget and there are strategic interactions between their choices. The complete 2-player CNG is specified as a simultaneous, non-cooperative, and complete-information game comprised of the programs $(P_A,P_D)$ such that the attacker solves:

and the defender solves:

The functions $f^a:{\mathbb{Z}}^{2|V|}\mapsto ℝ,f^d:{\mathbb{Z}}^{2|V|}\mapsto ℝ$ are the payoffs of the attacker and the defender respectively. Each attack or defend choice has a cost represented by the vectors $a\in {\mathbb{Z}}_{+}^{|V|},d\in {\mathbb{Z}}_{+}^{|V|}$. The total budget for attacker / defender, respectively, is $A\in {\mathbb{Z}}_{+},D\in {\mathbb{Z}}_{+}$ and $p_i^d\in {\mathbb{Z}}_{+}$, $p_i^a\in {\mathbb{Z}}_{+}$ denote the criticality of node $i$ for respectively, the defender and the attacker. This formulation varies slightly from the original, as it restricts the costs, criticality, and budget to be integers instead of reals. But as we show later, our encoding scheme can be suitably modified to account for real costs, criticality, and budget as well. The variables $0\le \delta ,\eta ,ϵ,\gamma \le 1$ are then chosen as real-valued scalar parameters of a CNG with . The full payoff functions for attacker and defender are described in detail in appendix A

We now describe the bilevel graph interdiction game with two players attacker and the defender, with the defender as the leader. The following description of the game is a simplified version of the trilevel game introduced in [31] but with a constrained propagation dynamics. The game is played over an undirected graph $G=(V,E)$ where each node $v\in V$ is a critical digital infrastructure and each edge $(v_1,v_2)\in E$ represents a network connection between $v_1,v_2$. The objective of the defender (which moves first) is to choose $n_D\in {\mathbb{Z}}_{+}$ nodes to protect, followed by the attacker that chooses $n_A\in {\mathbb{Z}}_{+}$ nodes to infect with malware. We assume a constrained propagation model where an attacked node can propagate the malware to undefended nodes at a distance of at most $r$ before being detected, making them unsafe, with the distance between a node $a$ and $b$ being defined as the number of edges in the shortest path between $a$ and $b$. Figure 1 further explains the setup. The full formulation of the problem and its equivalent reduction to a maxSAT form is provided in Appendix B.

In this study, we showed that by using local solution concepts like the LOIS, it is possible to solve for IPGs using SAT solvers in both simultaneous and sequential discrete-strategy games. In particular, we note that the encodings required for solving these games are straightforward and are supported out-of-the-box by most commercially available SAT solvers. We also showed that these SAT solvers may be more efficient in terms of solution time when compared against state-of-the-art mathematical solvers like Gurobi, and the game theory community should definitely consider these solvers for large-scale discrete games as an alternative to mathematical program solvers. Finally, we also showed that in graph games, maxSAT solvers in conjunction with LOI solutions can provide better quality solutions with respect to heuristic-based solutions, even for tricky problem instances.

We note the following limitations of our study. First and foremost, only local solution concepts like LOIS remain solvable by SAT solvers. Similarly, games with non-linear objectives or constraints that are not encodable by binary circuits may not be possible to solve. In the bilevel graph interdiction example, although we were able to solve for moderate graph instances, we found scaling it to large graph sizes challenging. Future work seeking to expand this line of research should focus on global solution concepts (or higher-order LOI solutions) for IPGs using SAT and finding novel ways to scale graph games when solved using MaxSAT.