1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
rdb0.uip1_ranking_rel
(rdb0.act_ranking_rel/rdb0.last_touched_diff)
rdb0.prop_ranking_rel
(rdb0.props_made/rdb0_common.avg_props)
rdb0.last_touched_diff
(rdb0.glue/cl.glueHist_avg)
rdb0.glue
(rdb0.sum_props_made/cl.time_inside_solver)
((rdb0.sum_props_made/cl.time_inside_solver)/(rdb0.glue/rdb0_common.avg_glue))
(log2(cl.glue_before_minim)/(rdb0.sum_uip1_used/cl.time_inside_solver))
cl.orig_glue
(log2(cl.num_antecedents)/cl.num_total_lits_antecedents)
(cl.glueHist_longterm_avg/cl.glue_before_minim)
(rdb0.glue/rdb0_common.conflSizeHistLT_avg)
(rdb0.discounted_props_made/cl.numResolutionsHistLT_avg)
((rdb0.sum_uip1_used/cl.time_inside_solver)/rdb0.discounted_props_made)
(rdb0.glue/(rdb0.props_made/rdb0_common.avg_props))
((rdb0.sum_props_made/cl.time_inside_solver)/cl.num_total_lits_antecedents)
(rdb0.glue/cl.glueHistLT_avg)
(rdb0.prop_ranking_rel/(rdb0.uip1_used/rdb0_common.avg_uip1_used))
(cl.overlapHistLT_avg/cl.conflSizeHist_avg)
(cl.glueHistLT_avg/rdb0.uip1_used)
(rdb0.size/rdb0_common.avg_glue)
(rdb0.size/rdb0.sum_uip1_used)
rdb0.discounted_uip1_used
(cl.glueHistLT_avg/rdb0.discounted_props_made)
(rdb0.uip1_ranking_rel/rdb0_common.avg_uip1_used)
(cl.num_antecedents/(rdb0.discounted_uip1_used/rdb0_common.avg_uip1_used))
rdb0.sum_uip1_per_time_ranking_rel
rdb0.sum_props_per_time_ranking_rel
(cl.glueHist_avg/cl.atedecents_binRed)
#(cl.conflicts-rdb0.introduced_at_conflict)
#cl.atedecents_binRed
#rdb0.discounted_uip1_used3
#rdb0_common.num_vars
#cl.glueHist_avg
#rdb0.discounted_props_made3
#cl.num_antecedents
#rdb0_common.num_bin_irred_cls
#cl.trailDepthHistLT_avg
|
