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

regression in 1.5 candidate #30

Closed shnarazk closed 7 years ago

shnarazk commented 7 years ago 
"mios-1.4.0 (2d91fb9@2016-09-12)", 50, "SR15m/manthey_DimacsSorterHalf_37_6.cnf",  772.28
"mios-1.5@08-24", 50, "SR15m131/manthey_DimacsSorterHalf_37_6.cnf",  818.46
shnarazk commented 7 years ago

feb510c2b5c77bd5adc66ce23826d6f4f5d0ed0a

# 2017-08-24T15:33 .local/bin/mios-r15 ; Mios-1.5.0                       
# p='', t=1260 on smithi @ 2017-08-24T15:33:47+09:00           
"mios-r15", 1, "SAT-RACE/SR15m131/manthey_DimacsSorterHalf_37_6.cnf",  807.59
shnarazk commented 7 years ago

c6bba01 : import the new implementation without the algorithm

solver UF200 UF225 UF250 een bmc 38bits DSH_37_6
1.4.0 w/o llvm 20.73 64.21 132.38 8.20 5.55 23.05 1240.83
mios-1.4.0 11.44 772.28
mios-MC 14.10 44.52 117.11 5.37 3. 31 29.50 timout > 1260
mios- 1.4.1 12.36 36.96 106.52 5.28 3.81 26.24 171.19
⬆️ 04aca1c 10.31 33.31 70.06 4.2 2.17 11.53 793.80
minisat2.2 10.59 35.45 114.94 0.90 0.56 4.96 11.03

😲

shnarazk commented 7 years ago

5e93751

┌─[@xingu]─[~/Repositories/mios]─[regression-1.5*]─[2017-40-26T13:40:43]
$ mios-1.4.0 --stat -X test/data/38bits_10.dimacs.cnf ; mios-1.4.1 --stat -X ...
## [38bits_10.dimacs.cnf] NumOfBackjump: 95935, NumOfRestart: 15, EndOfStatIndex: 4435624
## [38bits_10.dimacs.cnf] NumOfBackjump: 123073, NumOfRestart: 15, EndOfStatIndex: 0

fixed by 99d4307

$ parallel -j1 "{} --stat -X test/data/38bits_10.dimacs.cnf" ::: mios-1.4.0 mios-1.4.1 
## [38bits_10.dimacs.cnf] NumOfBackjump: 95935, NumOfRestart: 15, EndOfStatIndex: 4435624
## [38bits_10.dimacs.cnf] NumOfBackjump: 95935, NumOfRestart: 15, EndOfStatIndex: 0
┌─[t%0]─[@xingu]─[~/Repositories/mios]─[regression-1[2017-07-26T14:07:06]
$ sat-benchmark -3 250 -L 200 -s mios-1.4.0 mios-1.4.1
solver, num, target, time
# p='', t=1260 on xingu @ 2017-08-26T14:07:13+09:00
# 2017-08-26T14:06 .local/bin/mios-1.4.0 ; mios 1.4.0 on regression15 branch
"mios-1.4.0", 1, 200,    14.43
"mios-1.4.0", 2, 225,    45.57
"mios-1.4.0", 3, 250,    94.83
"mios-1.4.0", 4, "een",  4.66
"mios-1.4.0", 5, "bmc",  3.05
"mios-1.4.0", 6, "38b",  20.89
# 2017-08-26T14:06 .local/bin/mios-1.4.1 ; mios 1.4.1 alpha on regression15 branch
"mios-1.4.1", 1, 200,    12.64
"mios-1.4.1", 2, 225,    41.97
"mios-1.4.1", 3, 250,    87.89
"mios-1.4.1", 4, "een",  4.60
"mios-1.4.1", 5, "bmc",  3.02
"mios-1.4.1", 6, "38b",  18.69
shnarazk commented 7 years ago

cactus-2017-05-22

## [atco_enc2_opt2_20_11.cnf] NumOfBackjump: 704895, NumOfRestart: 20 -- mios-1.4.0 
"mios-1.4.0@2016-09-12", 22, "atco_enc2_opt2_20_11.cnf",  1070.57
## [atco_enc2_opt2_20_11.cnf] NumOfBackjump: 704895, NumOfRestart: 20 -- mios-1.4.1
"mios-1.4.1@2017-08-26", 22, "atco_enc2_opt2_20_11.cnf",  1258.65

mios-1 4 0-22

mios-1 4 1-22

shnarazk commented 7 years ago

Mios-1.4.0 can solve 113 112 problems now. No regression exists.

cactus-sr15m131

shnarazk commented 7 years ago

e25a0863326ff4888b276d7522fbc9cf8fe4f00e