-------------------------------------------------------------------------------- TigerDisp | Metric Dumps -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- Contents -------------------------------------------------------------------------------- 1. Introduction 2. Default Format -------------------------------------------------------------------------------- 1. Introduction -------------------------------------------------------------------------------- The TigerDisp application takes metric dumps from solvers and display the data in a meaningful way. TigerDisp can be easily modified to use a variety of different metrics and the format of the metric dumps can be adjusted by users. -------------------------------------------------------------------------------- 2. Default Format -------------------------------------------------------------------------------- By default, TigerDisp expects dump files to be in the following format: DECISION_DEPTH_0 TOTAL_IMPLICATIONS_0 NEW_IMPLICATIONS_0 HISTOGRAM_OF_LEARNT_CLAUSES_0 DECISION_DEPTH_1 TOTAL_IMPLICATIONS_1 NEW_IMPLICATIONS_1 HISTOGRAM_OF_LEARNT_CLAUSES_1 DECISION_DEPTH_2 TOTAL_IMPLICATIONS_2 NEW_IMPLICATIONS_2 HISTOGRAM_OF_LEARNT_CLAUSES_2 ... Every two lines represents the metrics from a different iteration of the solution process. Each metric is space-delimited. The decision depth, total number of implications and number of new implications are non-negative integer values. The histogram is a space-delimited integer histogram whose least bucket contains the number of learnt clauses of length <= 2^0 and whose greatest bucket contains the number of learnt clauses of length <= 2^13. Each bucket increases by a power of 2. For example, if a file begins with 0 0 45 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 45 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 30 32 1 0 0 0 4 0 0 0 0 0 0 0 0 0 then we know that at iteration 0 we have a decision depth of 0, 0 total implications, 45 new implications and no learnt clauses of any size. At iteration 1 we have a decision depth of 1, 45 total implications, 0 new implications and no learnt clauses of any size. At iteration 2 we have a decision depth of 0, 30 total implications, 32 new implications and 1 learnt clause of length 2^0 and 4 learnt clauses of length <= 2^3.