TODO for 1.4.2

[shnarazk]

• LBD implementation Implement LBD again (4.1.2) #36
• Quick restart based on Luby or 'Glucose restart'
• Removed Clause Management (GC) merge clause-recycler into WIP-for-1.4.2 #34
• performance boost

branches

• WIP-for-1.2.0
• lbd2
• quick restart

[shnarazk]

[shnarazk]

clause recycle

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

[shnarazk]

f30e3a0

• use real (allocated) length of clause
• loose reuse condition; use a larger clause

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

[shnarazk]

Adopt for Glucose source instead of Glucose paper !!

    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. 👎