TigerDisp

Coming soon: A new version of TigerDisp will be made available for download this November. It will make use of Java Swing and, as such, be independent of the Processing environment. This platform change will provide users with a faster and more versatile tool. If you would like to receive an email with download/make instructions when the tool is posted, please let us know.

TigerDisp is 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 learnt 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.

The tool has been developed by Cameron Brien and Professor Sharad Malik with the help of Zhaohui Fu and Yinlei Yu. All are members of the Boolean Satisfiability Research Group at Princeton University.

Here, you can find TigerDisp source, documentation, sample metric dumps and screenshots. We encourage you download our tool and try it on the sample metric dumps provided, or on dumps from your own solvers. We have also posted our first paper on TigerDisp.

Contact the TigerDisp developers for comments and suggestions.