Update learnt DB's size as same as MiniSat 2.2 does

[shnarazk]

description

The size of learnt clause DB increases in search, controlled by the following parameters:

• The learnt DB expansion period scaling factor learntsize_adjust_inc is 1.5.
• The DB scaling factor learntsize_int is 1.1.

Mios has only one parameter so far.

baseline

373fe97

# p='', t=1260 on xingu @ 2017-09-11T20:08:54+09:00
"mios-sla", 5, 200,      12.73
"mios-sla", 6, 225,      33.61
"mios-sla", 7, 250,      145.78
"mios-sla", 8, "een",    5.04
"mios-sla", 9, "bmc",    3.24
"mios-sla", 10, "38b",   4.30

[shnarazk]

8f9251d

# p='', t=1260 on xingu @ 2017-09-12T18:07:23+09:00
"mios-sla", 5, 200,      13.44
"mios-sla", 6, 225,      44.87
"mios-sla", 7, 250,      104.19
"mios-sla", 8, "een",    5.25
"mios-sla", 9, "bmc",    3.74
"mios-sla", 10, "38b",   26.59

[shnarazk]

b125f06 -- to check the value without errors

# p='', t=1260 on xingu @ 2017-09-12T19:45:50+09:00
"mios-sla", 5, 200,      15.11
"mios-sla", 6, 225,      38.12
"mios-sla", 7, 250,      96.51
"mios-sla", 8, "een",    5.07
"mios-sla", 9, "bmc",    3.63
"mios-sla", 10, "38b",   22.90

And change restartScale's value from 4 to 2:

# p='', t=1260 on xingu @ 2017-09-12T19:51:09+09:00
"mios-sla", 1, 200,      19.56
"mios-sla", 2, 225,      48.23
"mios-sla", 3, 250,      124.66
"mios-sla", 4, "een",    5.05
"mios-sla", 5, "bmc",    3.19
"mios-sla", 6, "38b",    100.07

to 3:

# p='', t=1260 on xingu @ 2017-09-12T20:00:06+09:00
"mios-sla", 1, 200,      13.48
"mios-sla", 2, 225,      32.38
"mios-sla", 3, 250,      132.42
"mios-sla", 4, "een",    4.55
"mios-sla", 5, "bmc",    3.59
"mios-sla", 6, "38b",    80.37

This setting records about 700 secs against 009-???.cnf! 🎉