ABSTRACT. In 'The Art of Computer Programming', Knuth benchmarked 10 encoding techniques for computing the chromatic number of the queen’s graph: the minimum number of colors needed to color the squares of an $n \times n$ chessboard so that no two squares sharing a row, column, or diagonal receive the same color. In this paper, we extend his analysis much further by comparing thousands of encodings for the same problem, which allows us to identify additional factors that are important for solver performance. We obtain 1584 encodings for this problem by varying (a) the constraints that encode which color is assigned to each cell, (b) the constraints that forbid the same color appearing in a row, column, or diagonal line, and (c) the symmetry-breaking constraints. We find that the three most impactful encoding factors are (i) the choice of symmetry-breaking constraints, (ii) enabling so-called clique hints, and (iii) enforcing that each cell is assigned exactly one color through blocked clauses. Furthermore, while Knuth proposed clique hints as an advantage of the order encoding, we show in fact that they can be effectively employed for the one-hot encoding as well.

ABSTRACT. This talk highlights recent advances in the Global Benchmark Database (GBD), a unified infrastructure for benchmark and metadata management in NP-hard domains. These advances include canonical isomorphism-aware labeling, lightweight extensibility, and sustainable, data-driven benchmarking workflows for efficient comparative evaluation.

ABSTRACT. Solvers for NP-hard problems from areas such as automated reasoning or optimisation are complex systems in which many different components interact. The performance of these solvers is the result of an intricate interplay between implementation details, algorithmic concepts and heuristics. This, alongside the complexity of the problem instances to be solved, makes it challenging to assess the effect of a single idea on the overall performance of a given solver. It is therefore not only crucial, but also challenging to evaluate the performance impact of new ideas. Existing reliable evaluation methods require large sets of diverse benchmark instances and considerable amounts of computing resources. This makes empirical evaluation a bottleneck for solver development, as it is time-consuming and energy-intensive, often requiring several CPU years of computation to evaluate the impact of a single idea. In recent years, this bottleneck has led to the development of data-driven approaches that can dynamically select a smaller number of instances that provide sufficient statistical evidence to evaluate the relative performance of a given set of solvers. However, these methods are typically not easily accessible. In this work, we present a tool that implements these methods and makes them readily accessible to solver developers, thus enabling them to obtain swifter feedback on their ideas.

ABSTRACT. Benchmarking is a widely-used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in several competitions (such as the International Competition on Software Verification), and is used by several research groups worldwide to ensure reliable benchmarking.

ABSTRACT. Competitions are usually evaluated in terms of stand-alone performance, i.e. how much better a submission performs than others determines the winner. This does not tell us how much a submission complements the state of the art -- is it able to solve something that nothing else can solve, even though that may be only a small part of the overall benchmark? In this talk, I will present the results of a Shapley Value analysis to FLoC competitions, which does evaluate the contribution to the overall state of the art.

ABSTRACT. Iterative heuristic optimisation algorithms probabilistically search for good or near-optimal solutions under a limited evaluation budget, typically measured by the number of objective function evaluations. They are often applied when little or nothing is assumed about the objective function, for example, when derivatives are unavailable, evaluations are expensive or the landscape is accessible only through black-box queries. Many established algorithms exist [2], but they are understood to different degrees: for some, the role of individual operators and parameters has been studied extensively, whereas for others, the mechanisms underlying observed empirical behaviour remain comparatively less thoroughly understood from a theoretical perspective despite demonstrated practical success. Furthermore, algorithm performance can depend strongly on the exact configuration of operators and parameter settings. This ties with the No Free Lunch theorem, which states that without assumptions about problem structure, no optimisation algorithm performs universally better than any other according to any reasonable performance measure. Consequently, there is no universally best algorithm, and performance must generally be assessed empirically on finite sets of functions and under finite evaluation budgets. An algorithm may be viewed as a well-defined sequence of logical operations designed to solve a particular problem. Modular algorithms [6, 19] make this perspective explicit by allowing individual operators to be specified independently, thereby creating a combinatorial design space of configurations within a single algorithm family. This design space can be further extended through an algorithm’s parameters, including integer, continuous and categorical parameters. Such frameworks make it possible to investigate which operators and parameterisations are responsible for observed behavioural or performance differences. In recent years, the field of heuristic optimisation has seen an unfortunate proliferation of supposedly “novel” metaheuristics inspired by natural phenomena, ranging from animal behaviour to physical processes². These algorithms have received substantial criticism for lacking genuine algorithmic novelty and relying heavily on metaphorical descriptions [17]. They are often developed in an unstructured manner, with limited evidence regarding parameter effects or the distinct contribution of newly introduced operators [13, 8, 18, 5, 11, 1, 4]. Harmony Search (HS) [9] represents one such example and is commonly described through a musical metaphor involving harmony memory, harmony memory consideration, pitch adjustment and random selection. Previous work [20, 21] demonstrated that HS is a simplified special case from a broader well-established class of algorithms known as Evolution Strategies (ES) [16, 14, 15]. However, this result is not constructive and does not identify the specific ES configuration reproduced by HS. Establishing such correspondence is nontrivial because the parameterisations of the two algorithms cannot be mapped directly onto one another. Therefore, understanding the relationship between HS and ES requires an empirical procedure capable of identifying ES configurations whose behaviour most closely matches that of HS under controlled benchmarking conditions. Therefore, using established benchmarking practices [3] together with automated algorithm configuration techniques [12, 6], we investigate how to identify ES configurations and parameterisations that approximate different aspects of HS behaviour across benchmark functions, dimensionalities and evaluation budgets. To enable this analysis, we introduce a novel Modular Evolution Strategies (modES) framework for specifying ES algorithms through configurable operators and parameterisations. Performance evaluation is conducted using IOHprofiler [7], and experiments are performed on the BBOB benchmarking suite [10]. This case study highlights the role of computational benchmarking as more than a tool for ranking optimisation algorithms. Benchmarking may also provide a systematic basis for studying behavioural equivalence, identifying algorithmic redundancy and evaluating claims of novelty. By grounding comparisons between HS and ES within a reproducible modular framework, this work aims to make questions of algorithmic novelty, redundancy and behavioural similarity experimentally testable.

ABSTRACT. In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such as C, C++, and Java. Many of the used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIB is based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIB defines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. This paper presents version 1.0 of the SV-LIB format, including its design goals, the syntax, and informal semantics. Formal semantics and further extensions to concurrency are planned for future versions. In this talk we will explore what SV-LIB is and how benchmarks for it can be easily generated from higher-level languages like C.

ABSTRACT. Hard subgraph-finding problems occur frequently across a wide range of applications, and there are many solvers dedicated to finding exact solutions for these problems. Unfortunately, the various communities that develop and use these algorithms do not share the strong history and careful blend of theory, engineering, science, and general paranoia that we've accumulated over the past thirty years in the constraint solving, Boolean satisfiability, and automated reasoning communities. This talk will share some of the horrors I have witnessed whilst working on solvers for problems like maximum common subgraph, subgraph isomorphism, and maximum (weighted) clique. Highlights will include buggy solvers, excessive parameter tuning, hard-coding parameters based upon instance filenames, badly-generated random benchmark sets, badly-generated non-random benchmark sets, reuse of good benchmark instances from other problems in a way that makes them bad, moving goalposts, multiplying other people's runtimes by mysterious scaling factors rather than re-running experiments, and entire systems built on top of not understanding the theory correctly. I will also talk about my ongoing efforts to fix these practices, and speculate as to why this has been a dismal failure.

ABSTRACT. Apart from continuously developing novel heuristics for MaxSAT local search solvers, substantial work has focused on maximizing the performance from choosing and tuning existing solvers. Most prior studies evaluate solvers primarily based on the solution quality obtained by the solvers at one or a small number of fixed time budgets. However, recent work has shown that anytime analysis can reveal significant differences in local search solvers across various problem instances and can also support algorithm configuration in discovering more effective parameter settings. While similar techniques have been widely explored in the domain of black-box optimization, we observe a notable gap in their application to constraint optimization and automated reasoning domains such as MaxSAT. In the talk, I plan to discuss both the opportunities and challenges of analyzing and exploiting anytime behavior in MaxSAT solvers, as well as potential extensions to broader pseudo-boolean optimization problems. In practice, I will start with examples of tuning the anytime performance of the MaxSAT solvers and extensions to dynamic algorithm selection.

ABSTRACT. High-performance SAT solvers are critical to many automated reasoning approaches today. However, most performance analysis and improvements to SAT solvers are software-centric, with a few exceptions. Thus, the potential for improving solver performance through hardware changes or hardware-aware programming remains largely untapped. To improve SAT solver performance through hardware-aware programming or hardware changes, the community needs better analysis of the impact of various hardware features and designs on SAT solving performance. To enable the collection and analysis of hardware performance metrics for SAT solving, we propose ArchSAT, a framework for collecting and analysing the effect of a variety of hardware metrics on SAT solving performance. We capture metrics from SAT solver runs that are relevant to hardware such as cache miss data, branch misprediction data, and overall runtime, using multiple profilers such as perf and Intel VTune. We also capture data relevant to SAT solving algorithms from the solver runs, such as time spent doing Boolean Constraint Propagation (BCP), number of removed clauses, and time spent doing inprocessing. ArchSAT then enables graphing these metrics against each other, enabling researchers to analyse how SAT solving behaviour correlates with hardware metrics. Overall, we believe ArchSAT will spur the development of hardware-aware techniques for SAT solving, and the discovery of benchmarks that illustrate solving patterns which are hard to run efficiently on current hardware. We hope it will also eventually spur the development of hardware accelerators for SAT solving (we intend to develop such accelerators as future work).

ABSTRACT. Benchmark selection is a crucial part of empirical evaluations in automated reasoning, and both in competitions and in papers it is crucial that benchmarks are selected in a fair and unbiased way. Moreover, given the costs of running large-scale empirical evaluations, it would be desirable to select benchmarks in such a way that their power to discriminate between solvers is maximized. Given the latter goal, it seems desirable to avoid selecting benchmarks that will just time out on all solvers, and prefer benchmarks that yield a mixture of lower running times, higher running times, and timeouts accross different solvers. This leads to the idea of letting a few reference solvers pick benchmarks in such a way that different running times are well represented among these benchmarks. However, choosing benchmarks in this way may inadvertly bias the benchmark selection in favor of the reference solvers, and hence this should not be done without carefully analyzing whether the method is statistically sound.