Analysing the empirical time complexity of high-performance algorithms for SAT and TSP

The time complexity of problems and algorithms, i.e., the scaling of the time required for solving a problem instance as a function of instance size, is of key interest in theoretical computer science and practical applications. In this context, the propositional satisfiability (SAT) and the travelling salesperson (TSP) are two of the most intensely studied problems, and it is generally believed that solving SAT or TSP requires exponential time in the worst case. In this work, we refine and extend a recent empirical scaling analysis approach and study the empirical scaling of the running times of several prominent, high-performance SAT and TSP algorithms. For SAT, we focus on random 3-SAT instances from the phase transition region, arguably the most prominent model for difficult SAT instances, and obtain interesting and surprising scaling results for both SLS- and DPLL-based solvers. Particularly, we find solid support for polynomial scaling for SLS-based solvers on phase-transition random 3-SAT instances. We also show that DPLL-based solvers scale exponentially and are faster by only a constant factor in solving satisfiable instances compared to unsatisfiable instances. We further report empirical scaling results for two classes of random 4-SAT instances to gain additional insights into the performance of state-of-the-art SAT solvers. For TSP, we concentrate on two-dimensional random uniform Euclidean (RUE) instances, and characterise the scaling of running time for complete and incomplete algorithms for finding optimal solutions. Our results indicate that the scaling of all these algorithms is consistent with or bounded from above by root-exponential models of the form a·b^(√n). We also explored the impact of automated algorithm configuration on the scaling of these algorithms. Since our approach is applicable beyond SAT and TSP, to enable its broad use, we designed Empirical Scaling Analyser (ESA), an automated tool that can be conveniently used to study empirical scaling of many types of algorithms. In particular, ESA presents scaling analysis results in the form of automatically generated, detailed technical reports. Many results reported in this thesis, including most tables and figures, were automatically generated by ESA and are only slightly modified to fit here.Science, Faculty ofComputer Science, Department ofGraduat