Communications of the ACM

Our second method uses γ- to initialize local search solvers. Such solvers search a space of complete variable assignments, typically following gradients to minimize an objective function such as the number of violated constraints, with occasional random steps. They are thus sensitive to their starting points. Optionally, we can start at the assignment given by γ- (randomly initializing variables pertaining to s+). We can also optionally redo this initialization on some fraction of random restarts.

Problem simplification. Next, we considered three pre-processing techniques that can simplify station repacking problems. First, we added the option to run the arc consistency algorithm, repeatedly pruning values from each station’s domain that are incompatible with every channel on a neighboring station’s domain.

Second, we enabled elimination of unconstrained stations. A station s is unconstrained if, given any feasible assignment of all of the other stations in S \ s, there always exists some way of feasibly repacking s. Unconstrained stations can be removed without changing a problem’s satisfiability status. Various algorithms exist for identifying unconstrained stations; we determine this choice via a parameter. (All such stations can be found via a reduction to the polytime problem of eliminating variables in a binary Constraint Satisfaction Problems (CSP); 3 various sound but incomplete heuristics run more quickly but identify progressively fewer unconstrained stations.)

Third, the interference graph induced by a problem may
consist of multiple connected components; we can optionally
run a linear-time procedure to separate them into distinct
SAT problems. We only need to solve the component to which
s+ belongs: γ - supplies feasible assignments for all others.
Arc consistency and unconstrained station removal can
then create three kinds of clauses: ( 1) ∨d∈D(s) xs,d ∀s ∈ S (each
station is assigned at least one channel); ( 2) ¬xs,c ∨ ¬xs,c′ ∀s ∈
S, ∀c, c′ ≠ c ∈ D(s) (each station is assigned at most one chan-
nel); ( 3) ¬xs,c ∨ ¬xs′,c′ ∀{(s, c), (s′, c′)} ∈ I (interference con-
straints are respected). Note that ( 2) is optional: if a station is
assigned more than one channel, we can simply pick one
channel to assign it from among these channels arbitrarily.
We thus created a parameter indicating whether to include
these constraints. In the end, a SAT encoding of a problem
involving all stations at a clearing target of 36 involved 73 187
variables and 2 917 866 clauses.

Selecting solvers. Perhaps the most important top-level parameter determines which SAT solver to run. (Of course, each such solver will have its own (deep) parameter space; other parameters will describe design dimensions orthogonal to the choice of solver, as we will discuss in what follows.) The SAT community has developed a very wide variety of solvers and made them publicly available (see e.g., Järvisalo et al. 19). In principle, we would have made it possible to choose every solver that offered even reasonable performance. However, doing so would have been too costly from the perspective of software integration and (especially) reliability testing. We thus conducted initial algorithm configuration experiments (see Section 3. 2) on 20 state-of-the-art SAT solvers, drawn mainly from SAT solver competition entries collected in AClib. 18 We illustrate the performance of their default configurations as shown in Figure 2; most improved at least somewhat from their default configurations as a result of algorithm configuration. We identified two solvers that ended up with the strongest post-configuration performance—one complete and one based on local search—both of which have been shown in the literature to adapt well to a wide range of SAT domains via large and flexible parameter spaces. Our first solver was clasp, 12 an open-source solver based on conflict-driven nogood learning ( 98 parameters). Our second was the open-source SATenstein framework, 22 which allows arbitrary composition of design elements taken from a wide range of high-performance stochastic local search solvers ( 90 parameters), including DCCA and gNovelty+ (of which three solvers in our set are variants).

Using the previous solution. While adapting clasp and SATenstein to station repacking data yielded substantial performance improvements, neither reached a point sufficient for deployment in the real auction. To do better, it was necessary to leverage specific properties of the incentive auction problem. Rather than committing to specific speedups, we exposed a wide variety of possibilities via further parameters. We began by considering two methods for taking advantage of the existence of a partial assignment γ -. The first method checks whether a simple transformation of γ- is enough to yield a satisfiable repacking. Specifically, we construct a small SAT problem in which the stations to be repacked are s+ and all stations Γ(s+) ⊆ S neighboring s+ in the interference graph, fixing all other stations S \ Γ(s+) to their assignments in γ -. Any solution to this reduced problem must be a feasible repacking; however, if the reduced problem is infeasible we cannot conclude anything. However (depending on the value of a parameter), we can keep searching: unfixing all stations that neighbor a station in Γ(s+), etc.

Figure 2. Empirical Cumulative Density Function (ECDF) of runtimes for default configurations of MIP and SAT solvers and for SATFC

2. 3. 1. The curves show fraction of instances solved (y axis) within different amounts of time (x axis; note the log scale). The legend is ordered by percentage of problems solved before the cutoff. The histogram indicates density of SAT and UNSAT instances binned by their (fastest) runtimes; unsatisfiable instances constituted fewer than 1% of solved instances.

SATFC 2. 3. 1

Gnovelty+PCL CSCCSat2014

DCCA Minisat_HACK_999ED_CSSC PicoSAT Solver43 Riss3g Riss3gExt Clasp Riss427 Lingeling Yalsat Gnovelty+GCwa Gnovelty+GCa SparrowToRiss Forl-nodrup Cryptominisat Spear Gurobi Satenstein CPLEX ProbSAT SAT UNSAT TIMEOUT