Computing lexicographically safe Nash equilibria in finite two-person games with tight game forms given by oracles

In 1975 the first author proved that every finite tight two-person game form g is Nash-solvable, that is, for every payoffs u and w of two players the obtained normal form game (g;u,w) has a Nash equilibrium (NE) in pure strategies. Several proofs of this theorem were obtained later. Here we strengthen the result and give a new proof, which is shorter than previous ones. We show that game (g;u,w) has two types of NE, realized by a lexicographically safe (lexsafe) strategy of one player and some special best response of the other. The proof is constructive, we obtain a polynomial algorithm computing these lexsafe NE. This is trivial when game form g is given explicitly. Yet, in applications g is frequently realized by an oracle O such that size of g is exponential in the size |O| of O. We assume that game form g=g(O) generated by O is tight and that an arbitrary ±1 game (g;u⁰,w⁰) (in which payoffs u⁰ and w⁰ are zero-sum and take only values ±1) can be solved in time polynomial in |O|. These assumptions allow us to compute two (one for each player) lexsafe NE in time polynomial in |O|. These NE may coincide. We consider four types of oracles known in the literature and show that all four satisfy the above assumptions.