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 without proxy vectors #84

Closed shnarazk closed 6 years ago

shnarazk commented 6 years ago

precondition

validation of ebbfe71d35b6a6032a0b6923ba8088605e7a83ac

parallel "mios-{} --dump=1 -X test/data/44bits_11.dimacs.cnf " ::: 76 84.0 84.1
NumOfBackjump,NumOfRestart,NumOfBlockRestart,NumOfGeometricRestart,NumOfPropagation,NumOfReduction,NumOfClause,NumOfLearnt,NumOfVariable,NumOfAssigned,emaAFast,emaASlow,emaBDLvl,emaCDLvl,emaDFast,emaDSlow
911718,61,58,0,77135508,245,15081,6540,594,609,115.772,109.656,13.152,14.216,8.339,9.288
911718,61,58,0,77135508,245,15081,6540,594,609,115.772,109.656,13.152,14.216,8.339,9.288
911718,61,58,0,77135508,245,15081,6540,594,609,115.772,109.656,13.152,14.216,8.339,9.288
shnarazk commented 6 years ago
# sat-benchmark 0.14.2, j=1, t=510, p='' on xingu @ 2018-04-07T17:04:55+09:00
solver, num, target, time
# 2018-04-07T16:28 mios-84.0; #82.0 https://github.com/shnarazk/mios/commit/164044bcd4e382bc306c969d737f70eab935f511
"mios-84.0", 1, 250,     166.32
"mios-84.0", 2, "itox",  14.54
"mios-84.0", 3, "m283",  70.68
"mios-84.0", 4, "38b",   24.04
"mios-84.0", 5, "44b",   124.43
# 2018-04-07T17:04 mios-84.1; #84.1 https://github.com/shnarazk/mios/commit/ebbfe71d35b6a6032a0b6923ba8088605e7a83ac
"mios-84.1", 1, 250,     165.13
"mios-84.1", 2, "itox",  14.64
"mios-84.1", 3, "m283",  68.94
"mios-84.1", 4, "38b",   23.47
"mios-84.1", 5, "44b",   125.90
shnarazk commented 6 years ago

cherry-picked by #85