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

a comparison of IO layer #78

Closed shnarazk closed 6 years ago

shnarazk commented 6 years ago
shnarazk commented 6 years ago
┌─[t%0]─[narazaki@xingu]─[mios@03-24T12:54:33]─[2018-03-streamly*]
$ mios-78  --validate ~/Documents/SAT-RACE/SC17main/g2-ACG-15-10p1.cnf 
 - number of clauses = 1155731, 21MB
 - making a new solver: 1.174 sec
injecting w/ streamly: 254.505 sec
injecting w/ ByteString: 15.147 sec
injecting w/ Handle: 24.375 sec
injecting w/o IO (1144812):7.827 sec

$ mios-78  --validate ~/Documents/SAT-RACE/SC17main/g2-T75.2.0.cnf 
 - number of clauses = 5251942, 109MB
 - making a new solver: 21.540 sec
injecting w/ streamly: 7925.713 sec
injecting w/ ByteString: 378.158 sec
injecting w/ Handle: 811.630 sec
injecting w/o IO (5251942):184.046 sec
shnarazk commented 6 years ago
$ sat-benchmark -3 250 -s mios-78
solver, num, target, time
# 2018-03-24T21:21 mios-78 compiled with ghc-8.4.1
"mios-78", 1, 250,       153.89
"mios-78", 2, "itox",    15.02
"mios-78", 3, "m283",    70.00
"mios-78", 4, "38b",     67.51

$ sat-benchmark -3 250 -s mios-74-altitude
# 2018-03-19T09:52 mios-74-altitude compiled with ghc-8.2.2
"mios-74-altitude", 1, 250,      189.15
"mios-74-altitude", 2, "itox",   24.01
"mios-74-altitude", 3, "m283",   113.65
"mios-74-altitude", 4, "38b",    93.54

# 2018-03-25T09:57 mios-74-altitude compiled with ghc-8.4.1
"mios-74-altitude", 1, 250,      157.82
"mios-74-altitude", 2, "itox",   15.30
"mios-74-altitude", 3, "m283",   71.05
"mios-74-altitude", 4, "38b",    69.86
shnarazk commented 6 years ago
$ mios-78 ~/Documents/SAT-RACE/SC17main/g2-T1.2.1.cnf
 - number of clauses = 14484930
 - making a new solver: 158.697 sec
injecting w/ ByteString: 1296.056 sec

$ mios-78 ~/Documents/SAT-RACE/SC17main/g2-T75.2.0.cnf 
 - number of clauses = 5251942
 - making a new solver: 22.362 sec
injecting w/ ByteString: 163.974 sec
injecting w/o IO (5251942):155.487 sec