mios version 1.5.3

[shnarazk]

ChangeLog

• implement EMA based Glucose heuristics (Biere 2015) #62
• implement two-phase restart
• fix a bug on learnt clause reduction in a marginal situation
• thread-based timeout handling #58
• update command line options
• update the benchmark report format #64
• add a new type to represent search result #64
• learnt clause simplification uses 64-bit computation

TODO

• [x] a better timeout implementation using threads and MVar #58
• [x] Glucose heuristics on restart #62
• [x] check documentation coverage by haddock
• [x] hlint
• [x] consistency check

related PR

• 59 (was #57)

• 60

[shnarazk]

Awesome 😲

[shnarazk]

Consistency check: all the UNSAT declared by Mios are really UNSAT.

Confirmed with Glucose and Lingerling 👍

• [x] "mios-1.5.3",211,"SC17main/mp1-Nb5T06.cnf",99.342,0
• [x] "mios-1.5.3",216,"SC17main/mp1-Nb6T06.cnf",168.315,0
• [x] "mios-1.5.3",238,"SC17main/mp1-blockpuzzle_7x10_s9_free6.cnf",221.586,0
• [x] "mios-1.5.3",250,"SC17main/mp1-bsat180-648.cnf",19.094,0
• [x] "mios-1.5.3",251,"SC17main/mp1-bsat192-689.cnf",28.628,0
• [x] "mios-1.5.3",252,"SC17main/mp1-bsat201-707.cnf",125.759,0
• [x] "mios-1.5.3",253,"SC17main/mp1-bsat210-739.cnf",215.320,0
• [x] "mios-1.5.3",294,"SC17main/mp1-ps_5000_21250_3_0_0.8_0_1.50_0.cnf",100.088,0
• [x] "mios-1.5.3",295,"SC17main/mp1-ps_5000_21250_3_0_0.8_0_1.50_2.cnf",270.760,0
• [x] "mios-1.5.3",296,"SC17main/mp1-ps_5000_21250_3_0_0.8_0_1.50_4.cnf",235.251,0
• [x] "mios-1.5.3",297,"SC17main/mp1-ps_5000_21250_3_0_0.8_0_1.50_6.cnf",80.435,0
• [x] "mios-1.5.3",298,"SC17main/mp1-ps_5000_21250_3_0_0.8_0_1.50_8.cnf",180.621,0
• [x] "mios-1.5.3",318,"SC17main/mp1-rubikcube101.cnf",479.607,0
• [x] "mios-1.5.3",328,"SC17main/mp1-rubikcube601.cnf",251.789,0
• [x] "mios-1.5.3",330,"SC17main/mp1-rubikcube701.cnf",472.388,0
• [x] "mios-1.5.3",334,"SC17main/mp1-rubikcube901.cnf",312.806,0
• [x] "mios-1.5.3",346,"SC17main/mp1-tri_ali_s11_c35_abio_UNS.cnf",93.359,0
• [x] "mios-1.5.3",347,"SC17main/mp1-tri_ali_s11_c35_abix_UNS.cnf",115.600,0
• [x] "mios-1.5.3",348,"SC17main/mp1-tri_ali_s11_c35_bail_UNS.cnf",55.247,0
• [x] "mios-1.5.3",349,"SC17main/mp1-tri_ali_s11_c35_sinx_UNS.cnf",48.353,0
• [x] "mios-1.5.3",350,"SC17main/mp1-tri_ali_s11_c35_sinz_UNS.cnf",47.561,0

[shnarazk]

The last blocker was resolved.

The WIP was affected heavily by other processes, I think.