Instance pool.

This supporting table describes the instances used for our experiments with Glucose 4.1. The instance bivium-40–200-0s0–0x92fc13b11169afbb2ef11a684d9fe9a19e743cd6aa5ce23fb5–19 was abbreviated by bivium-40–200 in the table. The column SAT/UNSAT indicates whether the instance is satisfiable (SAT) or unsatisfiable (UNSAT). Note that extending an instance with a set preserves the satisfiability of the instance. The column cen denotes the number of censored data points of each instance during the Glucose 4.1 trials, i. e., , where cenj is the censoring indicator introduced in Eq (2). The columns Ztime and ptime report the results of the t-test for CPU time as described in Section 4. Similarly, the columns Zconfl and pconfl report the results of the t-test for the number of conflicts as described in Section 4. In both cases, a negative value of the test statistic Z signifies a positive effect for the mean of the extended instances. All values were rounded to two places. The values “—” in the table denote the two instances where complications in the t-test for the censored number of conflict data occurred. The table itself can be found on the following pages in landscape mode. (CSV)