We present, to our knowledge, the first mixed integer program (MIP) formulations for finding Nash equilibria in games (specifically, two-player normal form games). We study different design dimensions of search algorithms that are based on those formulations. Our MIP Nash algorithm outperforms Lemke-Howson but not Porter-Nudelman-Shoham (PNS) on GAMUT data. We argue why experiments should also be conducted on games with equilibria with medium-sized supports only, and present a methodology for generating such games. On such games MIP Nash drastically outperforms PNS but not Lemke-Howson. Certain MIP Nash formulations also yield anytime algorithms for epsilon-equilibrium, with provable bounds. Another advantage of MIP Nash is that it can be used to find an optimal equilibrium (according to various objectives). The prior algorithms can be extended to that setting, but they are orders of magnitude slower.