Understanding the Dynamic Behaviour of Modern DPLL SAT Solvers through Visual Analysis

摘要

Despite the many recent improvements in the speed and robustness of DPLL-based SAT solvers, we still lack a thorough understanding of the working mechanisms and dynamic behaviour of these solvers at run-time. In this paper, we present TIGERDISP, a tool designed to allow researchers to visualize the dynamic behaviour of modern DPLL solvers in terms of time-dependent metrics such as decision depth, implications and learned conflict clauses. It is our belief that inferences about dynamic behaviour can be drawn more easily by visual analysis than by purely aggregate post-execution metrics such as total number of decisions/implications/conflicts. These inferences can then be validated through detailed quantitative analysis on larger sets of data. To this end, we have used TIGERDISP with the HAIFASAT and MINISAT solvers and have generated a few specific inferences about their relatively efficient and inefficient solving runs. We have then tested one of these inferences through quantitative analysis on a larger data set and have presented our findings in this paper. An important application of TIGERDISP would be in the development of a solver that employs adaptive algorithms. This is an area that has intrigued researchers in the past, but has not seen significant results for lack of a clear understanding as to what constitutes good progress during the run of a SAT solver. With better knowledge of dynamic behaviour, it is conceivable that an adaptive solver could be designed such that it switches between several competitive heuristics at run-time based on a quantitative analysis of its own dynamic behaviour.