SATFC : SAT-based Feasibility Checker

News

Abstract

SATFC is an algorithm based on propositional satisfiability (SAT) to solve the station repacking problem that arise in spectrum "incentive auctions".

People

• Alexandre Fréchette,  Ph.D. student, University of British Columbia.
• Neil Newman,  M.Sc. student, University of British Columbia.
• Kevin Leyton-Brown,  Professor, University of British Columbia.

Software

• The FCC's official release of SATFC can be found here.
• Newer, unofficial releases SATFC and the reverse auction simulator can be found here.

Data

• Our Station Repacking Problems Benchmark contains 10,000 CNFs from experiments described in Deep Optimization for Spectrum Repacking. See also accompanying files with problem information here and here.
• Additional benchmarks (new as of 2021) have been released! These problems come from experiments in the paper "Incentive Auction Design Alternatives: A Simulation Study" and are described in an Appendix to the Proceedings of the 2020 SAT Competition here.
  • Feasibility Checker contains 10,000 CNFs from experiments on alternate feasibility checkers. See also accompanying files with problem information here.
  • Multiple Stages contains 10,000 CNFs from experiments on multiple stage auctions. See also accompanying files with problem information here.
  • Scoring Rules contains 10,000 CNFs from experiments on scoring rules. See also accompanying files with problem information here.

Papers

• Alexandre Fréchette, Neil Newman, Kevin Leyton-Brown
  Solving the Station Packing Problem
  In Association for the Advancement of Artificial Intelligence (AAAI), 2016.
  [pdf]