Boosting Verification by Automatic Tuning of Decision Procedures

By Frank Hutter, Domagoj Babic, Holger H. Hoos, Alan J. Hu. 2007

165 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Industrial and Manufacturing Engineering, Software

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Industrial and Manufacturing Engineering

In Software

Citations in the corpus

Efficient Benchmarking of Hyperparameter Optimizers via Surrogates (2015, methodology): “Similar successes have been achieved by general algorithm configuration methods on a wide range of problems, such as tuning combinatorial problem solvers for Boolean satisfiability (Hutter et al. 2007) and mixed integer”
ParamILS: An Automatic Algorithm Configuration Framework (2014, methodology): “CALIBRA starts by evaluating each parameter conﬁguration in a full factorial design with two values per parameter.”
Parallel Algorithm Configuration (2012, methodology): “Indeed, the literature on algorithm configuration already contains examples of both the first [1, 4, 2, 3] and second [4, 5] forms of parallelization.”
Automated Algorithm Configuration and Parameter Tuning (2012, methodology): “…to approaches based on experimental design methods (see, e.g., Birattari et al, 2002; Balaprakash et al, 2007; Adenso-Diaz and Laguna, 2006), response-surface models (see, e.g., Jones et al, 1998; Bartz-Beielstein, 2006) or stochastic local search procedures (see, e.g., Hutter et al, 2007b, 2009a).”
Surrogate Benchmarks for Hyperparameter Optimization (2014, methodology): “In particular, we plan to support optimization across a set of problem instances, each of which can be described by a fixed-length vector of characteristics, and to assess the resulting surrogates for several problems that algorithm configuration has tackled successfully, such as propositional satis”
An Efficient Approach for Assessing Hyperparameter Importance (2014, background): “…led to substantial improvements of high-performance heuristic algorithms for a wide range of problems, including propositional satisfiability (Hutter et al., 2007; KhudaBukhsh et al., 2009), mixed integer programming (Hutter et al., 2009), answer set programming (Silverthorn et al., 2012)…”
Identifying Key Algorithm Parameters and Instance Features Using Forward Selection (2013, methodology): “We used exactly the same 26-dimensional parameter configuration space as in previous work [8].”
Automated configuration of algorithms for solving hard computational problems (2009, methodology): “In particular, we automatically constructed different instantiations of the SPEAR algorithm and thereby substantially improved the state of the art for two sets of SAT-encoded industrial verification problems (Hutter et al., 2007a).”
The irace package: Iterated racing for automatic algorithm configuration (2016, unknown): “[13, 14, 15] have used it extensively as a benchmark for testing automatic tuning tools.”
Algorithm runtime prediction: Methods & evaluation (2012, methodology): “For the industrial SAT solver SPEAR [3], we used the same parameter configuration space as in previous work [49].”
Sequential Model-Based Optimization for General Algorithm Configuration (2011, methodology): “Our own group has used PARAMILS to configure highly parameterized tree search [10] and local search solvers [11] for the propositional satisfiability problem (SAT), as well as several solvers for mixed integer programming (MIP), substantially advancing the state of the art for various types of insta”
Hydra: Automatically Configuring Algorithms for Portfolio-Based Selection (2010, unknown): “The first such technique is automated algorithm configuration (Gratch and Dejong 1992; Fukunaga 2002; Balaprakash, Birattari, and Stützle 2007; Hutter et al. 2007; 2009; Ansótegui, Sellmann, and Tierney 2009).”
Neurosymbolic Programming (2021, methodology): “For example, in the SAT community, there is work dating back to the mid 2000s that used machine learning to set the parameters of a SAT solver that control its internal heuristics (Hutter et al., 2007).”
Automated Configuration of Mixed Integer Programming Solvers (2010, methodology): “For this reason, in previous work we adopted the strategy to perform 10 independent parallel runs of FOCUSEDILS and use the result of the run with best training performance [16, 19].”
Efficient Benchmarking of Algorithm Configuration Procedures via Model-Based Surrogates (2017, background): “A is a parameterized target algorithm; – Θ is the parameter configuration space of A; – DΠ is a distribution over a set of instances Π; – κ <∞ is a cutoff time at which each run of A will be terminated; –”
Automatic Algorithm Configuration Based on Local Search (2007, methodology): “…applied to several solvers submitted to the 2007 SAT Competition, where it achieved a speedup of about an order of magnitude for SAPS on random instances and a 50-fold speedup for tuning a new state-of-the-art tree search algorithm on SAT-encoded software verification problems (Hutter et al. 2007).”
Hydra-MIP : Automated Algorithm Configuration and Selection for Mixed Integer Programming (2011, methodology): “Because a single run of a randomized configuration procedure might not yield a high-performing parameter configuration, it is common practice to perform multiple runs in parallel and to use the configuration that performs best on the training set [12, 14, 28, 13].”