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
10–1 10–2 0.0
0.1
0.2
0.3
0.4
0.5
0.6
0.7
0.8
0.9
1.0
100 101 102
Runtime (s)
Fra
c
t
i
on
o
f
i
ns
t
an
c
e
s