Chapter 12. Automated Configuration and Selection of SAT Solvers

2021 ◽  
Author(s):  
Holger H. Hoos ◽  
Frank Hutter ◽  
Kevin Leyton-Brown
Keyword(s):  
Research And Development ◽  
State Of The Art ◽  
Sat Solving ◽  
Sat Solvers ◽  
Effective Application ◽  
Automated Algorithm ◽  
Fertile Ground ◽  
Algorithm Configuration ◽  
Algorithmic Approaches ◽  
Selection Of

This chapter provides an introduction to the automated configuration and selection of SAT algorithms and gives an overview of the most prominent approaches. Since the early 2000s, these so-called meta-algorithmic approaches have played a major role in advancing the state of the art in SAT solving, giving rise to new ways of using and evaluating SAT solvers. At the same time, SAT has proven to be particularly fertile ground for research and development in the area of automated configuration and selection, and methods developed there have meanwhile achieved impact far beyond SAT, across a broad range of computationally challenging problems. Conceptually more complex approaches that go beyond “pure” algorithm configuration and selection are also discussed, along with some open challenges related to meta-algorithmic approaches, such as automated algorithm configuration and selection, to the tools based on these approaches, and to their effective application.

scholarly journals Boosting the Performance of SLS and CDCL Solvers by Preprocessor Tuning

10.29007/28ww ◽  
2018 ◽  
Author(s):  
Adrian Balint ◽  
Norbert Manthey
Keyword(s):  
State Of The Art ◽  
Performance Gain ◽  
Sat Solvers ◽  
Automated Algorithm ◽  
Algorithm Configuration ◽  
Art Performance ◽  
Preprocessing Technique

Preprocessing techniques are crucial for SAT solvers when it comes to reaching state-of-the-art performance as it was shown by the results of the last SAT Competitions. Theusefulness of a preprocessing technique depends highly on its own parameters, on the in-stances on which it is applied and on the used solver. In this paper we first give an extendedanalysis of the performance gain reached by using different preprocessing techniques in-dividually in combination with CDCL solvers on application instances and SLS solverson crafted instances. Further, we provide an analysis of combinations of preprocessingtechniques by means of automated algorithm configuration, where we search for optimalpreprocessor configurations for different scenarios. Our results show that the performanceof CDCL and especially of SLS solvers can be further improved when using appropriatepreprocessor configurations. The solvers augmented with the best found preprocessingconfigurations outperform the original solvers on the instances from the SAT Challenge2012, achieving new state-of-the-art results.

scholarly journals Dolius: A Distributed Parallel SAT Solving Framework

10.29007/hvqt ◽  
2018 ◽  
Author(s):  
Gilles Audemard ◽  
Benoît Hoessen ◽  
Saïd Jabbour ◽  
Cédric Piette
Keyword(s):  
Shared Memory ◽  
State Of The Art ◽  
Divide And Conquer ◽  
Sat Solving ◽  
Sat Solvers ◽  
Sat Solver

Over the years, parallel SAT solving becomes more and more important. However, most of state-of-the-art parallel SAT solvers are portfolio-based ones. They aim at running several times the same solver with different parameters. In this paper, we propose a tool called Dolius, mainly based on the divide and conquer paradigm. In contrast to most current parallel efficient engines, Dolius does not need shared memory, can be distributed, and scales well when a large number of computing units is available. Furthermore, our tool contains an API allowing to plug any SAT solver in a simple way.

scholarly journals Automated Algorithm Selection: Survey and Perspectives

2019 ◽  
Vol 27 (1) ◽  
pp. 3-45 ◽  
Author(s):  
Pascal Kerschke ◽  
Holger H. Hoos ◽  
Frank Neumann ◽  
Heike Trautmann
Keyword(s):  
State Of The Art ◽  
Combinatorial Problems ◽  
The State ◽  
Problem Instance ◽  
Ai Planning ◽  
Algorithm Selection ◽  
Automated Algorithm ◽  
Continuous Problems ◽  
Algorithm Configuration ◽  
The One

It has long been observed that for practically any computational problem that has been intensely studied, different instances are best solved using different algorithms. This is particularly pronounced for computationally hard problems, where in most cases, no single algorithm defines the state of the art; instead, there is a set of algorithms with complementary strengths. This performance complementarity can be exploited in various ways, one of which is based on the idea of selecting, from a set of given algorithms, for each problem instance to be solved the one expected to perform best. The task of automatically selecting an algorithm from a given set is known as the per-instance algorithm selection problem and has been intensely studied over the past 15 years, leading to major improvements in the state of the art in solving a growing number of discrete combinatorial problems, including propositional satisfiability and AI planning. Per-instance algorithm selection also shows much promise for boosting performance in solving continuous and mixed discrete/continuous optimisation problems. This survey provides an overview of research in automated algorithm selection, ranging from early and seminal works to recent and promising application areas. Different from earlier work, it covers applications to discrete and continuous problems, and discusses algorithm selection in context with conceptually related approaches, such as algorithm configuration, scheduling, or portfolio selection. Since informative and cheaply computable problem instance features provide the basis for effective per-instance algorithm selection systems, we also provide an overview of such features for discrete and continuous problems. Finally, we provide perspectives on future work in the area and discuss a number of open research challenges.

scholarly journals AutoFolio: An Automatically Configured Algorithm Selector

2015 ◽  
Vol 53 ◽  
pp. 745-778 ◽  
Author(s):  
Marius Lindauer ◽  
Holger H. Hoos ◽  
Frank Hutter ◽  
Torsten Schaub
Keyword(s):  
State Of The Art ◽  
Machine Learning Techniques ◽  
Problem Instance ◽  
Algorithm Selection ◽  
The Core ◽  
Automated Algorithm ◽  
Learning Techniques ◽  
Algorithm Configuration ◽  
Optimal Values ◽  
The One

Algorithm selection (AS) techniques -- which involve choosing from a set of algorithms the one expected to solve a given problem instance most efficiently -- have substantially improved the state of the art in solving many prominent AI problems, such as SAT, CSP, ASP, MAXSAT and QBF. Although several AS procedures have been introduced, not too surprisingly, none of them dominates all others across all AS scenarios. Furthermore, these procedures have parameters whose optimal values vary across AS scenarios. This holds specifically for the machine learning techniques that form the core of current AS procedures, and for their hyperparameters. Therefore, to successfully apply AS to new problems, algorithms and benchmark sets, two questions need to be answered: (i) how to select an AS approach and (ii) how to set its parameters effectively. We address both of these problems simultaneously by using automated algorithm configuration. Specifically, we demonstrate that we can automatically configure claspfolio 2, which implements a large variety of different AS approaches and their respective parameters in a single, highly-parameterized algorithm framework. Our approach, dubbed AutoFolio, allows researchers and practitioners across a broad range of applications to exploit the combined power of many different AS methods. We demonstrate AutoFolio can significantly improve the performance of claspfolio 2 on 8 out of the 13 scenarios from the Algorithm Selection Library, leads to new state-of-the-art algorithm selectors for 7 of these scenarios, and matches state-of-the-art performance (statistically) on all other scenarios. Compared to the best single algorithm for each AS scenario, AutoFolio achieves average speedup factors between 1.3 and 15.4.

scholarly journals Guiding CDCL SAT Search via Random Exploration amid Conflict Depression

2020 ◽  
Vol 34 (02) ◽  
pp. 1428-1435
Author(s):  
Md Solimul Chowdhury ◽  
Martin Müller ◽  
Jia You
Keyword(s):  
Variable Selection ◽  
State Of The Art ◽  
Fast Rate ◽  
Empirical Evaluation ◽  
Sat Solving ◽  
Sat Solvers ◽  
Exploration Strategy ◽  
Clause Learning ◽  
Strong Performance ◽  
Performance Gains

The efficiency of Conflict Driven Clause Learning (CDCL) SAT solving depends crucially on finding conflicts at a fast rate. State-of-the-art CDCL branching heuristics such as VSIDS, CHB and LRB conform to this goal. We take a closer look at the way in which conflicts are generated over the course of a CDCL SAT search. Our study of the VSIDS branching heuristic shows that conflicts are typically generated in short bursts, followed by what we call a conflict depression phase in which the search fails to generate any conflicts in a span of decisions. The lack of conflict indicates that the variables that are currently ranked highest by the branching heuristic fail to generate conflicts. Based on this analysis, we propose an exploration strategy, called expSAT, which randomly samples variable selection sequences in order to learn an updated heuristic from the generated conflicts. The goal is to escape from conflict depressions expeditiously. The branching heuristic deployed in expSAT combines these updates with the standard VSIDS activity scores. An extensive empirical evaluation with four state-of-the-art CDCL SAT solvers demonstrates good-to-strong performance gains with the expSAT approach.

scholarly journals Pitfalls and Best Practices in Algorithm Configuration

2019 ◽  
Vol 64 ◽  
pp. 861-893 ◽  
Author(s):  
Katharina Eggensperger ◽  
Marius Lindauer ◽  
Frank Hutter
Keyword(s):  
Best Practices ◽  
High Performance ◽  
State Of The Art ◽  
Parameter Tuning ◽  
Propositional Satisfiability ◽  
Ai Planning ◽  
Practical Applications ◽  
Automated Algorithm ◽  
Algorithm Configuration ◽  
Satisfiability Solving

Good parameter settings are crucial to achieve high performance in many areas of artificial intelligence (AI), such as propositional satisfiability solving, AI planning, scheduling, and machine learning (in particular deep learning). Automated algorithm configuration methods have recently received much attention in the AI community since they replace tedious, irreproducible and error-prone manual parameter tuning and can lead to new state-of-the-art performance. However, practical applications of algorithm configuration are prone to several (often subtle) pitfalls in the experimental design that can render the procedure ineffective. We identify several common issues and propose best practices for avoiding them. As one possibility for automatically handling as many of these as possible, we also propose a tool called GenericWrapper4AC.

scholarly journals Greybox Algorithm Configuration

2021 ◽  
Author(s):  
Marie Anastacio
Keyword(s):  
State Of The Art ◽  
Automated Algorithm ◽  
Wide Range ◽  
Algorithm Configuration ◽  
Improve Algorithm ◽  
The Difference ◽  
Problem Instances ◽  
The Right ◽  
Parameter Values ◽  
Configuration Problem

The performance of state-of-the-art algorithms is highly dependent on their parameter values, and choosing the right configuration can make the difference between solving a problem in a few minutes or hours. Automated algorithm configurators have shown their efficiency on a wide range of applications. However, they still encounter limitations when confronted to a large number of parameters to tune or long algorithm running time. We believe that there is untapped knowledge that can be gathered from the elements of the configuration problem, such as the default value in the configuration space, the source code of the algorithm, and the distribution of the problem instances at hand. We aim at utilising this knowledge to improve algorithm configurators.

Report on the 4th Joint Workshop on Bibliometric-Enhanced Information Retrieval and Natural Language Processing for Digital Libraries at SIGIR 2019

2019 ◽  
Vol 53 (2) ◽  
pp. 3-10
Author(s):  
Muthu Kumar Chandrasekaran ◽  
Philipp Mayr
Keyword(s):  
Information Retrieval ◽  
Natural Language Processing ◽  
Natural Language ◽  
Research And Development ◽  
Language Processing ◽  
Digital Libraries ◽  
State Of The Art ◽  
Shared Task ◽  
Processing Information ◽  
Joint Workshop

The 4 th joint BIRNDL workshop was held at the 42nd ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR 2019) in Paris, France. BIRNDL 2019 intended to stimulate IR researchers and digital library professionals to elaborate on new approaches in natural language processing, information retrieval, scientometrics, and recommendation techniques that can advance the state-of-the-art in scholarly document understanding, analysis, and retrieval at scale. The workshop incorporated different paper sessions and the 5 th edition of the CL-SciSumm Shared Task.

Interpreting testing and assessment: A state-of-the-art review

2021 ◽  
pp. 026553222110361
Author(s):  
Chao Han
Keyword(s):  
State Of The Art ◽  
Professional Certification ◽  
Automatic Assessment ◽  
Prospective Students ◽  
Assessment Practice ◽  
High Stakes ◽  
Future Directions ◽  
Assessment Tasks ◽  
Interpreter Education ◽  
Selection Of

Over the past decade, testing and assessing spoken-language interpreting has garnered an increasing amount of attention from stakeholders in interpreter education, professional certification, and interpreting research. This is because in these fields assessment results provide a critical evidential basis for high-stakes decisions, such as the selection of prospective students, the certification of interpreters, and the confirmation/refutation of research hypotheses. However, few reviews exist providing a comprehensive mapping of relevant practice and research. The present article therefore aims to offer a state-of-the-art review, summarizing the existing literature and discovering potential lacunae. In particular, the article first provides an overview of interpreting ability/competence and relevant research, followed by main testing and assessment practice (e.g., assessment tasks, assessment criteria, scoring methods, specificities of scoring operationalization), with a focus on operational diversity and psychometric properties. Second, the review describes a limited yet steadily growing body of empirical research that examines rater-mediated interpreting assessment, and casts light on automatic assessment as an emerging research topic. Third, the review discusses epistemological, psychometric, and practical challenges facing interpreting testers. Finally, it identifies future directions that could address the challenges arising from fast-changing pedagogical, educational, and professional landscapes.

Sign in / Sign up

Export Citation Format

Share Document