  Although Boolean Constraint Technology has made tremendous progress over the
last decade, the efficacy of state-of-the-art solvers is known to vary
considerably across different types of problem instances and is known to depend
strongly on algorithm parameters. This problem was addressed by means of a
simple, yet effective approach using handmade, uniform and unordered schedules
of multiple solvers in ppfolio, which showed very impressive performance in the
2011 SAT Competition. Inspired by this, we take advantage of the modeling and
solving capacities of Answer Set Programming (ASP) to automatically determine
more refined, that is, non-uniform and ordered solver schedules from existing
benchmarking data. We begin by formulating the determination of such schedules
as multi-criteria optimization problems and provide corresponding ASP
encodings. The resulting encodings are easily customizable for different
settings and the computation of optimum schedules can mostly be done in the
blink of an eye, even when dealing with large runtime data sets stemming from
many solvers on hundreds to thousands of instances. Also, the fact that our
approach can be customized easily enabled us to swiftly adapt it to generate
parallel schedules for multi-processor machines.
