search

shnarazk / mios

A SAT solver written in Haskell.
https://gitlab.com/satisfiability01/mios/
GNU General Public License v3.0
39 stars 3 forks source link

sort clauses by size-lbd-activity #42

Closed shnarazk closed 7 years ago

shnarazk commented 7 years ago

ChangeLog:

baseline

# 2017-08-31T16:03 mios-1.4.1 ; mios 1.4.1
# p='', t=1260 on xingu @ 2017-09-01T11:36:08+09:00
"mios-1.4.1", 5, 200,    15.74
"mios-1.4.1", 6, 225,    42.32
"mios-1.4.1", 7, 250,    88.32
"mios-1.4.1", 8, "een",  4.57
"mios-1.4.1", 9, "bmc",  2.92
"mios-1.4.1", 10, "38b",         19.32

cactus2015-sr15m131

From Glucose 2.0, 2.1, 3.0 and 4.0 : 

struct reduceDB_lt { 
    ClauseAllocator& ca;
    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()); } 
    }

That's completely different 😠

shnarazk commented 7 years ago

2d6f556 including two completely wrong calculations :worried: 

#40noPhaseRestart #42SLA-ordering
# p='', t=1260 on xingu @ 2017-09-11T12:02:59+09:00
"mios-sla", 5, 200,      14.24
"mios-sla", 6, 225,      35.47
"mios-sla", 7, 250,      132.14
"mios-sla", 8, "een",    4.67
"mios-sla", 9, "bmc",    3.69
"mios-sla", 10, "38b",   5.54
shnarazk commented 7 years ago

cce009a4530b0b18c66abaa7429149657724e9fc commited at 2017-09-11T15:13 (probably this should be "mios-sla-2017-09-11-1.csv".)

# p='', t=1260 on xingu @ 2017-09-11T15:18:49+09:00
"mios-sla", 1, 200,      16.77
"mios-sla", 2, 225,      46.05
"mios-sla", 3, 250,      147.24
"mios-sla", 4, "een",    4.70
"mios-sla", 5, "bmc",    3.82
"mios-sla", 6, "38b",    24.27
shnarazk commented 7 years ago

373fe97 -- changed limit definition used in sortClauses

# p='', t=1260 on xingu @ 2017-09-11T20:08:54+09:00
"mios-sla", 5, 200,      12.73
"mios-sla", 6, 225,      33.61
"mios-sla", 7, 250,      145.78
"mios-sla", 8, "een",    5.04
"mios-sla", 9, "bmc",    3.24
"mios-sla", 10, "38b",   4.30
shnarazk commented 7 years ago

cactus2015-sr15m131

shnarazk commented 7 years ago

1583c31

cactus2015-sr15m131

shnarazk commented 7 years ago

c1b318b

cactus2015-sr15m131

shnarazk commented 7 years ago

f50e3bb

cactus2015-sr15m131

shnarazk commented 7 years ago

0a2db01

cactus2015-sr15m131

shnarazk commented 7 years ago

tweak on clause ordering

"mios-sla", 3, 200,      18.02
"mios-sla", 4, 225,      59.12
"mios-sla", 5, 250,      147.09
"mios-sla", 6, "een",    4.17
"mios-sla", 7, "bmc",    2.67
"mios-sla", 8, "38b",    55.99
"mios-sla", 3, 200,      18.48
"mios-sla", 4, 225,      56.99
"mios-sla", 5, 250,      192.02
"mios-sla", 6, "een",    4.18
"mios-sla", 7, "bmc",    2.70
"mios-sla", 8, "38b",    43.76
shnarazk commented 7 years ago 
"mios-sla", 1, 200,      19.46
"mios-sla", 2, 225,      50.11
"mios-sla", 3, 250,      192.74
"mios-sla", 4, "een",    4.17
"mios-sla", 5, "bmc",    2.68
"mios-sla", 6, "38b",    32.06

cactus2015-sr15m131

cactus2015-sr15m131-compare-sla

shnarazk commented 7 years ago

27563c4

# p='', t=1260 on smithi @ 2017-09-18T09:55:53+09:00
"mios-sla", 1, 200,      19.35
"mios-sla", 2, 225,      50.27
"mios-sla", 3, 250,      191.49
"mios-sla", 4, "een",    4.14
"mios-sla", 5, "bmc",    2.63
"mios-sla", 6, "38b",    31.09
shnarazk commented 7 years ago

cactus2015-sr15m131

shnarazk commented 7 years ago

case 1: true SLA

# p='', t=1260 on xingu @ 2017-10-01T14:06:16+09:00
"mios-sla", 1, 150,      2.02
"mios-sla", 2, 175,      6.07
"mios-sla", 3, 200,      18.32
"mios-sla", 4, 225,      51.04
"mios-sla", 5, 250,      223.88
"mios-sla", 6, "een",    5.49
"mios-sla", 7, "bmc",    3.23
"mios-sla", 8, "38b",    114.23

case 2: SSA

# p='', t=1260 on xingu @ 2017-10-01T14:14:33+09:00
"mios-sla", 1, 150,      2.04
"mios-sla", 2, 175,      6.24
"mios-sla", 3, 200,      17.93
"mios-sla", 4, 225,      45.91
"mios-sla", 5, 250,      156.70
"mios-sla", 6, "een",    5.07
"mios-sla", 7, "bmc",    3.13
"mios-sla", 8, "38b",    27.04

case 3: S(S+L)A

# p='', t=1260 on xingu @ 2017-10-01T13:59:31+09:00
"mios-sla", 1, 150,      2.07
"mios-sla", 2, 175,      6.26
"mios-sla", 3, 200,      18.00
"mios-sla", 4, 225,      46.08
"mios-sla", 5, 250,      156.97
"mios-sla", 6, "een",    5.05
"mios-sla", 7, "bmc",    3.68
"mios-sla", 8, "38b",    26.66
shnarazk commented 7 years ago

case 4: activity * size / lsb (overflow)

# p='', t=1260 on xingu @ 2017-10-01T15:39:13+09:00
"mios-sla", 1, 150,      2.05
"mios-sla", 2, 175,      6.32
"mios-sla", 3, 200,      17.99
"mios-sla", 4, 225,      46.10
"mios-sla", 5, 250,      157.30
"mios-sla", 6, "een",    4.46
"mios-sla", 7, "bmc",    3.67
"mios-sla", 8, "38b",    27.20

case 4': activity / lsb

# p='', t=1260 on xingu @ 2017-10-01T16:16:14+09:00
"mios-sla", 1, 150,      2.00
"mios-sla", 2, 175,      6.33
"mios-sla", 3, 200,      17.89
"mios-sla", 4, 225,      46.06
"mios-sla", 5, 250,      156.41
"mios-sla", 6, "een",    4.98
"mios-sla", 7, "bmc",    3.16
"mios-sla", 8, "38b",    26.32

case 5: SSL

# p='', t=1260 on xingu @ 2017-10-01T15:48:51+09:00
"mios-sla", 1, 150,      1.93
"mios-sla", 2, 175,      5.59
"mios-sla", 3, 200,      17.93
"mios-sla", 4, 225,      43.15
"mios-sla", 5, 250,      171.43
"mios-sla", 6, "een",    4.45
"mios-sla", 7, "bmc",    3.23
"mios-sla", 8, "38b",    53.28
shnarazk commented 7 years ago 
# p='', t=1260 on xingu @ 2017-10-01T19:12:06+09:00, size                                                                                                
"mios-sla", 1, 200,      17.14                                                                                                                           
"mios-sla", 2, 225,      50.68                                                                                                                           
"mios-sla", 3, 250,      192.39                                                                                                                          
"mios-sla", 4, "een",    4.47                                                                                                                            
"mios-sla", 5, "bmc",    3.71                                                                                                                            
"mios-sla", 6, "38b",    27.43                                                                                                                           

# p='', t=1260 on xingu @ 2017-10-01T19:19:45+09:00, lbd                                                                                                 
"mios-sla", 1, 200,      20.43                                                                                                                           
"mios-sla", 2, 225,      64.98                                                                                                                           
"mios-sla", 3, 250,      212.88                                                                                                                          
"mios-sla", 4, "een",    5.06                                                                                                                            
"mios-sla", 5, "bmc",    3.62                                                                                                                            
"mios-sla", 6, "38b",    43.71
shnarazk commented 7 years ago 
# p='', t=1260 on xingu @ 2017-10-01T19:12:06+09:00, size                                                                                                
"mios-sla", 1, 200,      17.14                                                                                                                           
"mios-sla", 2, 225,      50.68                                                                                                                           
"mios-sla", 3, 250,      192.39                                                                                                                          
"mios-sla", 4, "een",    4.47                                                                                                                            
"mios-sla", 5, "bmc",    3.71                                                                                                                            
"mios-sla", 6, "38b",    27.43                                                                                                                           

# p='', t=1260 on xingu @ 2017-10-01T19:19:45+09:00, lbd                                                                                                 
"mios-sla", 1, 200,      20.43                                                                                                                           
"mios-sla", 2, 225,      64.98                                                                                                                           
"mios-sla", 3, 250,      212.88                                                                                                                          
"mios-sla", 4, "een",    5.06                                                                                                                            
"mios-sla", 5, "bmc",    3.62                                                                                                                            
"mios-sla", 6, "38b",    43.71                                                                                                                           

# p='', t=1260 on xingu @ 2017-10-01T20:21:37+09:00, adaptive threshold = 5                                                                              
"mios-sla", 1, 200,      17.01                                                                                                                           
"mios-sla", 2, 225,      50.56                                                                                                                           
"mios-sla", 3, 250,      192.22                                                                                                                          
"mios-sla", 4, "een",    4.93                                                                                                                            
"mios-sla", 5, "bmc",    3.15                                                                                                                            
"mios-sla", 6, "38b",    27.54                                                                                                                           

# p='', t=1260 on xingu @ 2017-10-01T20:29:11+09:00, adaptive threshold = 6                                                                              
"mios-sla", 1, 200,      16.98                                                                                                                           
"mios-sla", 2, 225,      50.61                                                                                                                           
"mios-sla", 3, 250,      192.77                                                                                                                          
"mios-sla", 4, "een",    4.42                                                                                                                            
"mios-sla", 5, "bmc",    3.57                                                                                                                            
"mios-sla", 6, "38b",    27.55     
mios:SLA-ordering*$ sat-benchmark -3 250 -L 200 -s mios-sla -M 'k + r'                                                                                   
# p='', t=1260 on xingu @ 2017-10-01T20:43:44+09:00, k + r                                                                                               
"mios-sla", 1, 200,      17.20                                                                                                                           
"mios-sla", 2, 225,      50.96                                                                                                                           
"mios-sla", 3, 250,      192.64                                                                                                                          
"mios-sla", 4, "een",    4.47                                                                                                                            
"mios-sla", 5, "bmc",    3.16                                                                                                                            
"mios-sla", 6, "38b",    27.89                                                                                                                           
mios:SLA-ordering*$ sat-benchmark -3 250 -L 200 -s mios-sla -M 'k + r && flip all'                                                                       
# p='', t=1260 on xingu @ 2017-10-01T20:53:39+09:00, k + r && flip all                                                                                   
"mios-sla", 1, 200,      17.97                                                                                                                           
"mios-sla", 2, 225,      46.36                                                                                                                           
"mios-sla", 3, 250,      156.78                                                                                                                          
"mios-sla", 4, "een",    5.00                                                                                                                            
"mios-sla", 5, "bmc",    3.14                                                                                                                            
"mios-sla", 6, "38b",    25.49                                                                                                                           
mios:SLA-ordering*$ sat-benchmark -3 250 -L 200 -s mios-sla -M 'k && flip all'                                                                           
# p='', t=1260 on xingu @ 2017-10-01T21:07:58+09:00, k && flip all                                                                                       
"mios-sla", 1, 200,      17.98                                                                                                                           
"mios-sla", 2, 225,      45.88                                                                                                                           
"mios-sla", 3, 250,      156.54                                                                                                                          
"mios-sla", 4, "een",    5.02                                                                                                                            
"mios-sla", 5, "bmc",    3.57                                                                                                                            
"mios-sla", 6, "38b",    26.54                                                                                                                           
mios:SLA-ordering*$ sat-benchmark -3 250 -L 200 -s mios-sla -M 'r && flip all'                                                                           
# p='', t=1260 on xingu @ 2017-10-01T21:31:31+09:00, r && flip all                                                                                       
"mios-sla", 1, 200,      18.28                                                                                                                           
"mios-sla", 2, 225,      51.01                                                                                                                           
"mios-sla", 3, 250,      224.05                                                                                                                          
"mios-sla", 4, "een",    4.62                                                                                                                            
"mios-sla", 5, "bmc",    3.14                                                                                                                            
"mios-sla", 6, "38b",    119.03
shnarazk commented 7 years ago 
# 2017-10-08T04:23 mios-45; mios-1.4.1 #36 #39 #40 #43 #44 #42SLA-ordering
# p='', t=1260 on xingu @ 2017-10-08T04:23:51+09:00
"mios-45", 1, 175,       5.38
"mios-45", 2, 200,       15.21
"mios-45", 3, 225,       35.82
"mios-45", 4, 250,       117.86
"mios-45", 5, "een",     5.45
"mios-45", 6, "bmc",     4.17
"mios-45", 7, "38b",     10.31
shnarazk commented 7 years ago

My 'sort half and drop half' is better more or less.

# 2017-10-10T14:15 mios-45; mios-1.4.1 #36 #39 #40 #43 #44 #42SLA-ordering
# p='', t=1260 on xingu @ 2017-10-10T14:30:21+09:00, limit = n
"mios-45", 1, 175,       4.07
"mios-45", 2, 200,       11.70
"mios-45", 3, 225,       27.27
"mios-45", 4, 250,       97.57
"mios-45", 5, "itox",    12.64
"mios-45", 6, "m283",    105.98
"mios-45", 7, "38b",     43.68
"mios-45", 8, "48b",     700.50

# p='', t=1260 on xingu @ 2017-10-10T14:55:35+09:00, limit=div n 2
"mios-45", 1, 175,       4.10
"mios-45", 2, 200,       11.69
"mios-45", 3, 225,       27.28
"mios-45", 4, 250,       96.25
"mios-45", 5, "itox",    13.92
"mios-45", 6, "m283",    113.69
"mios-45", 7, "38b",     43.27
"mios-45", 8, "48b",     668.67

# p='', t=1260 on xingu @ 2017-10-10T15:17:13+09:00, sort and drop!
"mios-45", 1, 175,   4.02
"mios-45", 2, 200,   11.58
"mios-45", 3, 225,   25.48
"mios-45", 4, 250,   69.57
"mios-45", 5, "itox",    13.60
"mios-45", 6, "m283",    22.66
"mios-45", 7, "38b",     67.83
"mios-45", 8, "48b",     296.91

# p='', t=1260 on xingu @ 2017-10-10T15:26:59+09:00, size -> rank and drop
"mios-45", 1, 175,       4.07
"mios-45", 2, 200,       12.08
"mios-45", 3, 225,       31.01
"mios-45", 4, 250,       90.77
"mios-45", 5, "itox",    13.63
"mios-45", 6, "m283",    31.05
"mios-45", 7, "38b",     18.89
"mios-45", 8, "48b",     197.63

# p='', t=1260 on xingu @ 2017-10-10T15:35:38+09:00, at rank and drop
"mios-45", 1, 175,       3.83
"mios-45", 2, 200,       12.31
"mios-45", 3, 225,       31.24
"mios-45", 4, 250,       86.61
"mios-45", 5, "itox",    13.56
"mios-45", 6, "m283",    32.41
"mios-45", 7, "38b",     3.20
"mios-45", 8, "48b",     95.60

# p='', t=1260 on xingu @ 2017-10-10T15:46:29+09:00, 0.1*at, rank and drop  82f99cc
"mios-45", 1, 175,       3.86
"mios-45", 2, 200,       11.89
"mios-45", 3, 225,       33.58
"mios-45", 4, 250,       81.44
"mios-45", 5, "itox",    11.96
"mios-45", 6, "m283",    42.92
"mios-45", 7, "38b",     44.44
"mios-45", 8, "48b",     61.04

# 2017-08-31T16:03 mios-1.4.1; mios 1.4.1
"mios-1.4.1", 1, 175,    5.26
"mios-1.4.1", 2, 200,    12.63
"mios-1.4.1", 3, 225,    41.89
"mios-1.4.1", 4, 250,    87.42
"mios-1.4.1", 5, "itox",         17.56
"mios-1.4.1", 6, "m283",         133.73
"mios-1.4.1", 7, "38b",  20.84
"mios-1.4.1", 8, "48b",  545.59