aspeed: solver scheduling via answer set programming

DOI10.1017/S1471068414000015MaRDI QIDQ4592974zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Holger H. Hoos, Roland Kaminski, Marius Lindauer, Torsten Schaub

Publication date 9 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.1024

zbMATH Keywords

answer set programmingalgorithm schedulesportfolio-based solving

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic programming (68N17)

Abstract: 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.

Recommendations

• scientific article; zbMATH DE number 6261538
• claspfolio2: Advances in Algorithm Selection for Answer Set Programming
• Industrial-size scheduling with ASP+CP
• SATzilla: portfolio-based algorithm selection for SAT
• Applying machine learning techniques to ASP solving

Cites work

• scientific article; zbMATH DE number 5914356 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A self-adaptive multi-engine solver for quantified Boolean formulas
• Algorithm portfolios
• Compiling finite linear CSP into SAT
• Conflict-driven answer set solving: from theory to practice
• Hierarchical Hardness Models for SAT
• Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems
• Knowledge Representation, Reasoning and Declarative Problem Solving
• Learning dynamic algorithm portfolios
• Paramils: an automatic algorithm configuration framework
• Principles and practice of constraint programming. 18th international conference, CP 2012, Québec City, QC, Canada, October 8--12, 2012. Proceedings
• SATzilla: portfolio-based algorithm selection for SAT
• Unsatisfiability-based optimization in clasp

Cited in

(10)

• Multi-level Algorithm Selection for ASP
• Why CP portfolio solvers are (under)utilized? Issues and challenges
• scientific article; zbMATH DE number 6261538 (Why is no real title available?)
• Selecting algorithms for large berth allocation problems
• aspeed
• Parallel Logic Programming: A Sequel
• A review of literature on parallel constraint solving
• The algorithm selection competitions 2015 and 2017
• Optimal scheduling for exposed datapath architectures with buffered processing units by ASP
• Parallel composition of scheduling solvers

Describes a project that uses

Uses Software

• Paramils
• SATzilla
• Potassco
• irace
• Sugar
• SMAC

This page was built for publication: aspeed: solver scheduling via answer set programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4592974)