Closed shnarazk closed 6 years ago
911be34
# 2017-08-28T18:25 mios-1.4.1 ; mios 1.4.1 alpha on regression15 branch
"mios-1.4.1", 1, 100, 0.69
"mios-1.4.1", 2, 125, 1.16
"mios-1.4.1", 3, 150, 2.06
"mios-1.4.1", 4, 175, 5.23
"mios-1.4.1", 5, 200, 12.58
"mios-1.4.1", 6, 225, 41.78
"mios-1.4.1", 7, 250, 87.10
"mios-1.4.1", 8, "een", 4.59
"mios-1.4.1", 9, "bmc", 3.37
"mios-1.4.1", 10, "38b", 18.21
# 2017-08-30T10:02 mios-1.4.1-recycle ; mios 1.4.1 #clause-recycle
"mios-1.4.1-recycle", 1, 100, 0.71
"mios-1.4.1-recycle", 2, 125, 1.14
"mios-1.4.1-recycle", 3, 150, 2.00
"mios-1.4.1-recycle", 4, 175, 5.19
"mios-1.4.1-recycle", 5, 200, 12.39
"mios-1.4.1-recycle", 6, 225, 40.89
"mios-1.4.1-recycle", 7, 250, 84.95
"mios-1.4.1-recycle", 8, "een", 4.62
"mios-1.4.1-recycle", 9, "bmc", 3.02
"mios-1.4.1-recycle", 10, "38b", 18.40
f30e3a0
mios-1.4.1-recycle --stat -X test/data/38bits_10.dimacs.cnf
# disable the relaxation above
NumOfBackjump: 95935, NumOfRestart: 15, NumOfRecycle: 72605, NumOfPossibleRecycle: 13208
# enable
NumOfBackjump: 95935, NumOfRestart: 15, NumOfRecycle: 4309, NumOfPossibleRecycle: 70743
a15eb4a
# 2017-08-30T11:37 mios 1.4.1
"mios-1.4.1", 1, 200, 12.67
"mios-1.4.1", 2, 225, 41.70
"mios-1.4.1", 3, 250, 87.11
"mios-1.4.1", 4, "een", 4.57
"mios-1.4.1", 5, "bmc", 2.92
"mios-1.4.1", 6, "38b", 18.47
# 2017-08-31T10:46 mios 1.4.1 #clause-recycle
"mios-1.4.1-recycle", 1, 200, 12.25
"mios-1.4.1-recycle", 2, 225, 40.69
"mios-1.4.1-recycle", 3, 250, 84.63
"mios-1.4.1-recycle", 4, "een", 5.13
"mios-1.4.1-recycle", 5, "bmc", 3.26
"mios-1.4.1-recycle", 6, "38b", 18.92
on smithi
# p='', t=1260 on smithi @ 2017-08-31T10:57:22+09:00
# 2017-08-29T16:43 mios-1.4.1 ; mios 1.4.1
"mios-1.4.1", 1, 75, 0.71
"mios-1.4.1", 2, 100, 0.98
"mios-1.4.1", 3, 125, 1.58
"mios-1.4.1", 4, 150, 2.31
"mios-1.4.1", 5, 175, 4.75
"mios-1.4.1", 6, 200, 10.33
"mios-1.4.1", 7, 225, 33.36
"mios-1.4.1", 8, 250, 70.58
"mios-1.4.1", 9, "een", 4.06
"mios-1.4.1", 10, "bmc", 2.17
"mios-1.4.1", 11, "38b", 11.40
# 2017-08-30T11:08 mios-1.4.1-recycle-911be ; mios 1.4.1 #clause-recycle
"mios-1.4.1-recycle-911be", 1, 75, 0.72
"mios-1.4.1-recycle-911be", 2, 100, 1.09
"mios-1.4.1-recycle-911be", 3, 125, 1.51
"mios-1.4.1-recycle-911be", 4, 150, 2.23
"mios-1.4.1-recycle-911be", 5, 175, 4.59
"mios-1.4.1-recycle-911be", 6, 200, 10.16
"mios-1.4.1-recycle-911be", 7, 225, 32.04
"mios-1.4.1-recycle-911be", 8, 250, 66.44
"mios-1.4.1-recycle-911be", 9, "een", 4.09
"mios-1.4.1-recycle-911be", 10, "bmc", 2.15
"mios-1.4.1-recycle-911be", 11, "38b", 11.37
# 2017-08-31T10:56 mios-1.4.1-recycle ; mios 1.4.1 #clause-recycle
"mios-1.4.1-recycle", 1, 75, 0.70
"mios-1.4.1-recycle", 2, 100, 1.05
"mios-1.4.1-recycle", 3, 125, 1.55
"mios-1.4.1-recycle", 4, 150, 2.32
"mios-1.4.1-recycle", 5, 175, 4.59
"mios-1.4.1-recycle", 6, 200, 10.02
"mios-1.4.1-recycle", 7, 225, 31.95
"mios-1.4.1-recycle", 8, 250, 65.83
"mios-1.4.1-recycle", 9, "een", 4.06
"mios-1.4.1-recycle", 10, "bmc", 2.18
"mios-1.4.1-recycle", 11, "38b", 11.21
reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
bool operator () (CRef x, CRef y) {
// Main criteria... Like in MiniSat we keep all binary clauses
if(ca[x].size()> 2 && ca[y].size()==2) return 1;
if(ca[y].size()>2 && ca[x].size()==2) return 0;
if(ca[x].size()==2 && ca[y].size()==2) return 0;
// Second one based on literal block distance
if(ca[x].lbd()> ca[y].lbd()) return 1;
if(ca[x].lbd()< ca[y].lbd()) return 0;
// Finally we can use old activity or size, we choose the last one
return ca[x].activity() < ca[y].activity();
//return x->size() < y->size();
//return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
}
I couldn't imagine the above from the paper. 👎
branches