aspeed: ASP-based Solver Scheduling

Overview

Although Boolean Constraint Technology has made tremendous progress over the last decade, leading to industrial strength applications in SAT and related areas such as ASP, PB, and even CP, it suffers from a great sensitivity to search configuration. This problems was impressively counterbalanced at the 2011 SAT Competition by the rather simple approach of ppfolio relying on a handmade, uniform and unordered solver schedule. Inspired by this, we take advantage of the modeling and solving capacities of 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. Interestingly, our simple approach matches the performance of much more sophisticated ones, such as satzilla and 3S. Also, its high customizability made it easy to generate even parallel schedules for multi-core machines.

News

Usage 1.0

Benchmark Sets

Literature