Abstract
This talk will discuss the FCC’s “incentive auction”, which proposes to give television broadcasters an opportunity to sell their broadcast rights, to repack remaining broadcasters into a smaller block of spectrum, and to resell the freed airwaves to telecom companies. The stakes for this auction are huge—projected tens of billions of dollars in revenue for the government—justifying the design of a special-purpose descending-price auction mechanism, which I’ll discuss. An inner-loop problem in this mechanism is determining whether a given set of broadcasters can be repacked into a smaller block of spectrum while respecting radio interference constraints. This is an instance of a (worst-case intractable) graph coloring problem; however, stations’ broadcast locations and interference constraints are all known in advance. Early efforts to solve this problem considered mixed-integer programming formulations, but were unable to reliably solve realistic, national-scale problem instances. We advocate instead for the use of a SAT encoding, paired with a wide range of techniques: constraint graph decomposition; novel caching mechanisms that allow reuse of partial solutions from related, solved problems; algorithm configuration; algorithm portfolios; and the marriage of local-search and complete solver strategies. We show that our approach solves virtually all of a set of problems derived from auction simulations within the short time budget required in practice.