Chapter 11. Exploiting Runtime Variation in Complete Solvers

It has become well know over time that the performance of backtrack-style complete SAT solvers can vary dramatically depending on “little” details of the heuristics used, such as the way one selects the next variable to branch on and in what order the possible values are assigned to the variable. Extreme variations can result even from simple tie breaking mechanisms necessarily employed in all SAT solvers. The discovery of this extreme runtime variation has been both a stumbling block and an opportunity. This chapter focuses on providing an understanding of this intriguing phenomenon, particularly in terms of the so-called heavy tailed nature of the runtime distributions of systematic SAT solvers. It describes a simple formal model based on expensive mistakes to explain runtime distributions seen in practice, and discusses randomization and restart strategies that can be used to effectively overcome the negative impact of heavy tailed behavior. Finally, the chapter discusses the notion of backdoor variables, which explain the unexpectedly short runs one also often sees in practice.

Stochastic model for the CheY-P molarity in the neighbourhood of E. coli flagella motors

Escherichia coli serves as prototype for the study of peritrichous enteric bacteria that perform runs and tumbles alternately. Bacteria run forward as a result of the counterclockwise (CCW) rotation of their flagella bundle, which is located rearward, and perform tumbles when at least one of their flagella rotates clockwise (CW), moving away from the bundle. The flagella are hooked to molecular rotary motors of nanometric diameter able to make transitions between CCW and CW rotations that last up to one hundredth of a second. At the same time, flagella move or rotate the bacteria’s body microscopically during lapses that range between a tenth and ten seconds. We assume that the transitions between CCW and CW rotations occur solely by fluctuations of CheY-P molarity in the presence of two threshold values, and that a veto rule selects the run or tumble motions. We present Langevin equations for the CheY-P molarity in the vicinity of each molecular motor. This model allows to obtain the run- or tumble-time distribution as a linear combination of decreasing exponentials that is a function of the steady molarity of CheY-P in the neighbourhood of the molecular motor, which fits experimental data. In turn, if the internal signaling system is unstimulated, we show that the runtime distributions reach power-law behaviour, a characteristic of self-organized systems, in some time range and, afterwards, exponential cutoff. In addition, our model explains without any fitting parameters the ultrasensitivity of the flagella motors as a function of the steady state of CheY-P molarity. In addition, we show that the tumble bias for peritrichous bacterium has a similar sigmoid-shape to the CW bias, although shifted to lower concentrations when the flagella number increases. Thus, the increment in the flagella number allows lower operational values for each motor increasing amplification and robustness of the chemotatic signaling pathway.

Neural Networks for Predicting Algorithm Runtime Distributions

Many state-of-the-art algorithms for solving hard combinatorial problems in artificial intelligence (AI) include elements of stochasticity that lead to high variations in runtime, even for a fixed problem instance. Knowledge about the resulting runtime distributions (RTDs) of algorithms on given problem instances can be exploited in various meta-algorithmic procedures, such as algorithm selection, portfolios, and randomized restarts. Previous work has shown that machine learning can be used to individually predict mean, median and variance of RTDs. To establish a new state-of-the-art in predicting RTDs, we demonstrate that the parameters of an RTD should be learned jointly and that neural networks can do this well by directly optimizing the likelihood of an RTD given runtime observations. In an empirical study involving five algorithms for SAT solving and AI planning, we show that neural networks predict the true RTDs of unseen instances better than previous methods, and can even do so when only few runtime observations are available per training instance.

Using sequential runtime distributions for the parallel speedup prediction of SAT local search

This paper presents a detailed analysis of the scalability and parallelization of local search algorithms for the Satisfiability problem. We propose a framework to estimate the parallel performance of a given algorithm by analyzing the runtime behavior of its sequential version. Indeed, by approximating the runtime distribution of the sequential process with statistical methods, the runtime behavior of the parallel process can be predicted by a model based on order statistics. We apply this approach to study the parallel performance of two SAT local search solvers, namely Sparrow and CCASAT, and compare the predicted performances to the results of an actual experimentation on parallel hardware up to 384 cores. We show that the model is accurate and predicts performance close to the empirical data. Moreover, as we study different types of instances (random and crafted), we observe that the local search solvers exhibit different behaviors and that their runtime distributions can be approximated by two types of distributions: exponential (shifted and non-shifted) and lognormal.