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

ERA: experimentation on reset variable/clause activity #59

Closed shnarazk closed 6 years ago

shnarazk commented 6 years ago 
# sat-benchmark 0.13.4, j=1, t=1260, p='' on xingu @ 2017-11-25T17:39:34+09:00
# 2017-11-25T17:38 mios-WIP; mios-1.5.3WIP #58 -- https://github.com/shnarazk/mios
"mios-WIP", 1, 175,      4.24
"mios-WIP", 2, 200,      11.80
"mios-WIP", 3, 225,      33.32
"mios-WIP", 4, 250,      81.50
"mios-WIP", 5, "itox",   13.81
"mios-WIP", 6, "m283",   42.65
"mios-WIP", 7, "38b",    48.17
"mios-WIP", 8, "44b",    59.40
# 2017-11-25T17:39 mios-rca; mios-1.5.3WIP #58 #59RCA -- https://github.com/shnarazk/mios
"mios-rca", 1, 175,      4.44
"mios-rca", 2, 200,      14.08
"mios-rca", 3, 225,      29.00
"mios-rca", 4, 250,      70.16
"mios-rca", 5, "itox",   13.63
"mios-rca", 6, "m283",   185.13
"mios-rca", 7, "38b",    28.02
"mios-rca", 8, "44b",    479.95
shnarazk commented 6 years ago 
# 2017-11-25T18:18 mios-era; mios-1.5.3WIP #58 #59ERA -- https://github.com/shnarazk/mios
# sat-benchmark 0.13.4, j=1, t=1260, p='-e 1' on xingu @ 2017-11-25T18:19:31+09:00, expConfig=1
"mios-era", 1, 175,      8.90
"mios-era", 2, 200,      29.61
"mios-era", 3, 225,      73.14
"mios-era", 4, 250,      214.69
"mios-era", 5, "itox",   46.18
"mios-era", 6, "m283",   349.59
"mios-era", 7, "38b",    168.57
"mios-era", 8, "44b",    98.00
# 2017-11-25T18:18 mios-era; mios-1.5.3WIP #58 #59ERA -- https://github.com/shnarazk/mios
# sat-benchmark 0.13.4, j=1, t=1260, p='-e 2' on xingu @ 2017-11-25T18:40:59+09:00, expConfig=2
"mios-era", 1, 175,      4.67
"mios-era", 2, 200,      12.98
"mios-era", 3, 225,      35.64
"mios-era", 4, 250,      101.82
"mios-era", 5, "itox",   26.98
"mios-era", 6, "m283",   171.25
"mios-era", 7, "38b",    69.81
"mios-era", 8, "44b",     380.05
shnarazk commented 6 years ago 
$ parallel -j 1 "mios-era -e {} -X --stat SATbench/SR2015/44bits_11.dimacs.cnf" ::: 0 1 2 5 
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 4077754
NumOfRestart: 24
NumOfPropagation: 360528089
NumOfPureLitElimination: 7
NumOfBinaryClause: 73
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 417454
NumOfRestart: 18
NumOfPropagation: 39360885
NumOfPureLitElimination: 3
NumOfBinaryClause: 47
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 1338692
NumOfRestart: 21
NumOfPropagation: 129480289
NumOfPureLitElimination: 5
NumOfBinaryClause: 48

## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 3030178
NumOfRestart: 23
NumOfPropagation: 281080577
NumOfPureLitElimination: 3
NumOfBinaryClause: 66
shnarazk commented 6 years ago 
# p='-e 0' on xingu @ 2017-11-27T17:57:24+09:00
"mios-era", 2, 200,      15.54
"mios-era", 3, 225,      37.36
"mios-era", 4, 250,      104.19
"mios-era", 5, "itox",   23.78
"mios-era", 6, "m283",   97.53
"mios-era", 7, "38b",    58.74
"mios-era", 8, "44b",    1003.23

# p='-e 1' on xingu @ 2017-11-27T17:52:01+09:00
"mios-era", 2, 200,      11.81
"mios-era", 3, 225,      33.44
"mios-era", 4, 250,      82.13
"mios-era", 5, "itox",   14.87
"mios-era", 6, "m283",   42.68
"mios-era", 7, "38b",    47.91
"mios-era", 8, "44b",    60.69

# p='-e 2' on xingu @ 2017-11-27T18:20:05+09:00
"mios-era", 2, 200,      28.63
"mios-era", 3, 225,      71.03
"mios-era", 4, 250,      213.26
"mios-era", 5, "itox",   26.79
"mios-era", 6, "m283",   98.50
"mios-era", 7, "38b",    54.87
"mios-era", 8, "44b",    100.40

# p='-e 3' on xingu @ 2017-11-27T18:31:51+09:00
"mios-era", 2, 200,      26.70
"mios-era", 3, 225,      67.10
"mios-era", 4, 250,      214.69
"mios-era", 5, "itox",   14.99
"mios-era", 6, "m283",   43.14
"mios-era", 7, "38b",    56.74
"mios-era", 8, "44b",    284.28

# p='-e 4' on xingu @ 2017-11-27T18:45:41+09:00
"mios-era", 2, 200,      14.07
"mios-era", 3, 225,      38.98
"mios-era", 4, 250,      107.06
"mios-era", 5, "itox",   26.58
"mios-era", 6, "m283",   98.82
"mios-era", 7, "38b",    4.85
"mios-era", 8, "44b",    343.52

# p='-e 5' on xingu @ 2017-11-27T20:36:02+09:00
"mios-era", 1, 200,      12.74
"mios-era", 2, 225,      26.22
"mios-era", 3, 250,      71.64
"mios-era", 4, "itox",   14.49
"mios-era", 5, "m283",   40.62
"mios-era", 6, "38b",    48.86
"mios-era", 7, "44b",    403.13

#  p='-e 6' on xingu @ 2017-11-27T20:51:20+09:00
"mios-era", 1, 200,      22.16
"mios-era", 2, 225,      61.80
"mios-era", 3, 250,      185.76
"mios-era", 4, "itox",   25.56
"mios-era", 5, "m283",   93.78
"mios-era", 6, "38b",    54.74
"mios-era", 7, "44b",    814.15

# p='-e 7' on xingu @ 2017-11-27T21:25:09+09:00
"mios-era", 1, 200,      27.00
"mios-era", 2, 225,      65.26
"mios-era", 3, 250,      189.13
"mios-era", 4, "itox",   14.74
"mios-era", 5, "m283",   41.70
"mios-era", 6, "38b",    65.18
"mios-era", 7, "44b",    435.05