New algorithms for approximate Nash equilibria in bimatrix games

We consider the problem of computing additively approximate Nash equilibria in non-cooperative two-player games. We provide a new polynomial time algorithm that achieves an approximation guarantee of 0.36392. We first provide a simpler algorithm, that achieves a 0.38197-approximation, which is exactly the same factor as the algorithm of Daskalakis, Mehta and Papadimitriou. This algorithm is then tuned, improving the approximation error to 0.36392. Our method is relatively fast and simple, as it requires solving only one linear program and it is based on using the solution of an auxiliary zero-sum game as a starting point. Finally we also exhibit a simple reduction that allows us to compute approximate equilibria for multi-player games by using algorithms for two-player games.     

Pure Nash equilibria in player-specific and weighted congestion games

Unlike standard congestion games, weighted congestion games and congestion games with player-specific delay functions do not necessarily possess pure Nash equilibria. It is known, however, that there exist pure equilibria for both of these variants in the case of singleton congestion games, i.e., if the players’ strategy spaces contain only sets of cardinality one. In this paper, we investigate how far such a property on the players’ strategy spaces guaranteeing the existence of pure equilibria can be extended. We show that both weighted and player-specific congestion games admit pure equilibria in the case of matroid congestion games, i.e., if the strategy space of each player consists of the bases of a matroid on the set of resources. We also show that the matroid property is the maximal property that guarantees pure equilibria without taking into account how the strategy spaces of different players are interweaved.     

Establishing Nash equilibria of strategic games: a multistart Fuzzy Adaptive Simulated Annealing approach

This paper's proposal is to show some significant results obtained by the application of the optimization algorithm known as Fuzzy Adaptive Simulated Annealing (Fuzzy ASA) to the task of finding all Nash equilibria of normal form games. To that end, a special version of Fuzzy ASA, that utilizes space-filling curves to find good seeds, is applied to several well-known strategic games, showing its effectiveness in obtaining all Nash equilibria in all cases. The results are compared to previous work that also used computational intelligence techniques in order to solve the same problem but could not find all equilibria in all tests. Game theory is a very important subject, modeling interactions between generic agents, and Nash equilibrium represents a powerful concept portraying situations in which joint strategies are optimal in the sense that no player can benefit from changing her/his strategy while the other players do not change their strategies as well. So, new techniques are always welcome, mainly those that can find the whole set of solutions for a given strategic game.     

Extending the notion of rationality of selfish agents: Second Order Nash equilibria

Motivated by the increasing interest of the Computer Science community in the study and understanding of non-cooperative systems, we present a novel model for formalizing the rational behavior of agents with a more farsighted view of the consequences of their actions. This approach yields a framework creating new equilibria, which we call Second Order equilibria, starting from a ground set of traditional ones. By applying our approach to pure Nash equilibria, we define the set of Second Order pure Nash equilibria and present their applications to the Prisoner’s Dilemma game, to an instance of Braess’s Paradox in the Wardrop model and to the KP model with identical machines.     

On the complexity of constrained Nash equilibria in graphical games

A widely accepted rational behavior for non-cooperative players is based on the notion of Nash equilibrium. Although the existence of a Nash equilibrium is guaranteed in the mixed framework (i.e., when players select their actions in a randomized manner) in many real-world applications the existence of “any” equilibrium is not enough. Rather, it is often desirable to single out equilibria satisfying some additional requirements (in order, for instance, to guarantee a minimum payoff to certain players), which we call constrained Nash equilibria.In this paper, a formal framework for specifying these kinds of requirement is introduced and investigated in the context of graphical games, where a player p may directly be interested in some of the other players only, called the neighbors of p. This setting is very useful for modeling large population games, where typically each player does not directly depend on all the players, and representing her utility function extensively is either inconvenient or infeasible.Based on this framework, the complexity of deciding the existence and of computing constrained equilibria is then investigated, in the light of evidencing how the intrinsic difficulty of these tasks is affected by the requirements prescribed at the equilibrium and by the structure of players’ interactions. The analysis is carried out for the setting of mixed strategies as well as for the setting of pure strategies, i.e., when players are forced to deterministically choose the action to perform. In particular, for this latter case, restrictions on players’ interactions and on constraints are identified, that make the computation of Nash equilibria an easy problem, for which polynomial and highly-parallelizable algorithms are presented.     

Nash equilibria in stabilizing systems

The objective of this paper is three-fold. First, we specify what it means for a fixed point of a stabilizing distributed system to be a Nash equilibrium. Second, we present methods that can be used to verify whether or not a given fixed point of a given stabilizing distributed system is a Nash equilibrium. Third, we argue that in a stabilizing distributed system, whose fixed points are all Nash equilibria, no process has an incentive to perturb its local state, after the system reaches one fixed point, in order to force the system to reach another fixed point where the perturbing process achieves a better gain. If the fixed points of a stabilizing distributed system are all Nash equilibria, then we refer to the system as perturbation-proof. Otherwise, we refer to the system as perturbation-prone. We identify four natural classes of perturbation-(proof/prone) systems. We present system examples for three of these classes of systems, and show that the fourth class is empty.     

Worst-Case Nash Equilibria in Restricted Routing

We study the network routing problem with restricted and related links.There are parallel links with possibly different speeds,between a source and a sink.Also there are users,and each user has a traffic of some weight to assign to one of the links from a subset of all the links,named his/her allowable set.The users choosing the same link suffer the same delay,which is equal to the total weight assigned to that link over its speed.A state of the system is called a Nash equilibrium if no user can decrease his/her delay by unilaterally changing his/her link.To measure the performance degradation of the system due to the selfish behavior of all the users,Koutsoupias and Papadimitriou proposed the notion Price of Anarchy (denoted by PoA),which is the ratio of the maximum delay in the worst-case Nash equilibrium and in an optimal solution.The PoA for this restricted related model has been studied,and a linear lower bound was obtained.However in their bad instance,some users can only use extremely slow links.This is a little artificial and unlikely to appear in a real world.So in order to better understand this model,we introduce a parameter for the system,and prove a better Price of Anarchy in terms of the parameter.We also show an important application of our result in coordination mechanism design for task scheduling game.We propose a new coordination mechanism,Group-Makespan,for unrelated selfish task scheduling game with improved price of anarchy.     

Managed Agreement: Generalizing two fundamental distributed agreement problems

This paper presents a family of agreement problems called Managed Agreement, which is parameterized by the number of aristocrat nodes in the system; NBAC is a special case of this family when all nodes are aristocrats while Consensus is a special case of this family when there are no aristocrats. The paper also presents a parameterized family of failure detectors F(A) such that F(A) is the weakest failure detector class that enables solving Managed Agreement with a set A of aristocrats in an asynchronous environment.     

Proof movie — A proof with the Boyer-Moore prover

This paper uses the Boyer-Moore prover for developing a proof of correctness for the implementation of a very small compiler. The polished version of the proof is included as an appendix. The major intent of the paper is to describe the process of proving using an automatic theorem prover.This paper presents work done when the author was employed at the University of Kiel, Germany. The research was partially funded by the Commission of the European Communities (CEC) under the ESPRIT programme in the field of Basic Research Action proj. no. 3104, ProCoS: Provably Correct Systems     

Completeness of hyper-resolution via the semantics of disjunctive logic programs

We present a proof of completeness of hyper-resolution based on the fixpoint semantics of disjunctive logic programs. This shows that hyper-resolution can be studied from the point of view of logic programming.     

An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem

This paper describes the use of the Boyer-Moore theorem prover in mechanically generating a proof of Wilson's theorem: for any prime p, (p-1)! and p-1 are congruent modulo p. The input to the theorem prover consists of a sequence of three function definitions and forty-two propositions to be proved. The proofs generated by the system are based on a library of lemmas relating to list manipulation and number theory, including Fermat's theorem.     

状态无关主动队列管理算法博弈的Nash均衡

状态无关的主动队列管理算法处理分组时不区分分组所在的流的信息,因此在Internet中,它易于设计和部署。文中通过数学分析和仿真方法研究AQM博弈和Nash均衡存在性。假设业务流是Poisson分布的且用户可自由修改发送速率,因而有结论:Drop Tail、RED不能获得Nash均衡,CHOKe可以获得近似Nash均衡。依据判定条件,推导出一种与状态无关且具有效率的Nash均衡AQM算法。     

Solving generalized Nash equilibrium problems through stochastic global optimization

Generalized Nash equilibrium problems address extensions of the well-known standard Nash equilibrium concept, making it possible to model and study more general settings. The main difference lies in that they allow both objective functions and constraints of each player to depend on the strategies of other players. The study of such problems has numerous applications in many fields, including engineering, economics, or management science, for instance. In this work we introduce a solution algorithm based on the Fuzzy Adaptive Simulated Annealing global optimization method (Fuzzy ASA, for short), demonstrating that it is possible to transform the original task into a constrained global optimization problem, which can be solved, in principle, by any effective global optimization algorithm, but in this paper our main tool will be the cited paradigm (Fuzzy ASA). We believe that the main merit of the proposed approach is to offer a simpler alternative for solving this important class of problems, in a less restrictive way in the sense of not demanding very strong conditions on the defining functions. Several case studies are presented for the sake of exemplifying the proposal's efficacy.     

Cooperative network design: A Nash bargaining solution approach

The Network Design problem has received increasing attention in recent years. Previous works have addressed this problem considering almost exclusively networks designed by selfish users, which can be consistently suboptimal. This paper addresses the network design issue using cooperative game theory, which permits to study ways to enforce and sustain cooperation among users. Both the Nash bargaining solution and the Shapley value are widely applicable concepts for solving these games. However, the Shapley value presents several drawbacks in this context.For this reason, we solve the cooperative network design game using the Nash bargaining solution (NBS) concept. More specifically, we extend the NBS approach to the case of multiple players and give an explicit expression for users’ cost allocations. We further provide a distributed algorithm for computing the Nash bargaining solution. Then, we compare the NBS to the Shapley value and the Nash equilibrium solution in several network scenarios, including real ISP topologies, showing its advantages and appealing properties in terms of cost allocation to users and computation time to obtain the solution.Numerical results demonstrate that the proposed Nash bargaining solution approach permits to allocate costs fairly to users in a reasonable computation time, thus representing a very effective framework for the design of efficient and stable networks.     

The structure and complexity of Nash equilibria for a selfish routing game

In this work, we study the combinatorial structure and the computational complexity of Nash equilibria for a certain game that models selfish routing over a network consisting of m$m$ parallel links. We assume a collection of n$n$ users, each employing a mixed strategy, which is a probability distribution over links, to control the routing of her own traffic. In a Nash equilibrium, each user selfishly routes her traffic on those links that minimize her expected latency cost, given the network congestion caused by the other users. The social cost of a Nash equilibrium is the expectation, over all random choices of the users, of the maximum, over all links, latency through a link.     

On Protocols for the Automated Discovery of Theorems in Elementary Geometry

In this paper we consider the problem of dealing automatically with arbitrary geometric statements (including, in particular, those that are generally false) aiming to find complementary hypotheses for the statements to become true. Our approach proceeds within the framework of computational algebraic geometry. First we argue and propose a plausible protocol for automatic discovery, and then we present some algorithmic criteria, as well as the meaning (regarding the algebraic geometry of the varieties involved in the given statement), for the protocol success/failure. A detailed collection of examples in also included. Last author supported by grant “Algoritmos en Geometría Algebraica de Curvas y Superficies” (MTM2008-04699-C03-03) from the Spanish MICINN.     

A pragmatic approach to resolution-based theorem proving

Resolution theory offers a simple, complete method for proving theorems but is generally considered impractical. The theorems we are interested in proving arise in the analysis of programs and usually involve quantification. We have developed a system for proving these theorems using resolution, but have embedded in it a simplifier as the central component. The simplifier is an integrated collection of algorithms for normalizing arithmetic, relational, and logical expressions. The knowledge in the simplifier is encoded in procedures, rather than as axioms or rules. We use the simplifier to prove certain theorems, reduce the clutter in theorems, and reduce the cost of unification, Inherent in the normal form algorithms is the notion of strengthening (e.g., inferringa =b froma b ANDb a). We have incorporated the notion into the unification algorithm as well. The design of the system permits its use along a spectrum from pure resolution to resolution with interpretation of the arithmetic and relational operators. Strengthening is a heuristic that permits the movement along this spectrum. We call the approachi-resolution.i-resolution does not preserve completeness; it does define a means for approaching completeness efficiently and systematically. It thus attempts to provide a pragmatic approach to mechanical theorem proving.     

A mechanical proof of Quadratic Reciprocity

We describe the use of the Boyer-Moore theorem prover in mechanically generating a proof of the Law of Quadratic Reciprocity: for distinct odd primes p and q, the congruences x ² q (mod p) and x ² p (mod q) are either both solvable or both unsolvable, unless pq3 (mod 4). The proof is a formalization of an argument due to Eisenstein, based on a lemma of Gauss. The input to the theorem prover consists of nine function definitions, thirty conjectures, and various hints for proving them. The proofs are derived from a library of lemmas that includes Fermat's Theorem and the Gauss Lemma.