Understanding the dynamic behaviour of modern DPLL SAT solvers through visual analysis

Cameron Brien, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 TIGER DISP 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 TIGER DISP 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 runtime based on a quantitative analysis of its own dynamic behaviour.

Original languageEnglish (US)
Title of host publicationProceedings of Formal Methods in Computer Aided Design, FMCAD 2006
Pages49-50
Number of pages2
DOIs
StatePublished - Dec 1 2006
EventFormal Methods in Computer Aided Design, FMCAD 2006 - San Jose, CA, United States
Duration: Nov 12 2006Nov 16 2006

Publication series

NameProceedings of Formal Methods in Computer Aided Design, FMCAD 2006

Other

OtherFormal Methods in Computer Aided Design, FMCAD 2006
CountryUnited States
CitySan Jose, CA
Period11/12/0611/16/06

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Understanding the dynamic behaviour of modern DPLL SAT solvers through visual analysis'. Together they form a unique fingerprint.

  • Cite this

    Brien, C., & Malik, S. (2006). Understanding the dynamic behaviour of modern DPLL SAT solvers through visual analysis. In Proceedings of Formal Methods in Computer Aided Design, FMCAD 2006 (pp. 49-50). [4021008] (Proceedings of Formal Methods in Computer Aided Design, FMCAD 2006). https://doi.org/10.1109/FMCAD.2006.35