loading...
Understanding the Dynamic Behavior of Modern DPLL SAT Solvers through Visual Analysis
San Jose, California, USA November 12-November 16
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.35Formal Methods in Computer Aided Desi ...
 This Article 
 
PURCHASE ARTICLE: $0
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Cameron Brien, Princeton University, USA
Sharad Malik, Princeton University, USA
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 runtime based on a quantitative analysis of its own dynamic behaviour.
Citation:
Cameron Brien, Sharad Malik, "Understanding the Dynamic Behavior of Modern DPLL SAT Solvers through Visual Analysis," fmcad, pp.49-50, Formal Methods in Computer Aided Design (FMCAD'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.