Implement LBD again (4.1.2) #36

shnarazk · 2017-09-01T00:39:08Z

comparison target

# 2017-08-31T16:03 mios-1.4.1 ; mios 1.4.1
# p='', t=1260 on xingu @ 2017-09-01T11:36:08+09:00
"mios-1.4.1", 1, 100,    0.71
"mios-1.4.1", 2, 125,    1.18
"mios-1.4.1", 3, 150,    2.10
"mios-1.4.1", 4, 175,    6.94
"mios-1.4.1", 5, 200,    15.74
"mios-1.4.1", 6, 225,    42.32
"mios-1.4.1", 7, 250,    88.32
"mios-1.4.1", 8, "een",  4.57
"mios-1.4.1", 9, "bmc",  2.92
"mios-1.4.1", 10, "38b",         19.32

shnarazk · 2017-09-01T01:00:33Z

25eafb3

# 2017-09-01T11:14 mios-lbd ; mios #master #clause-recycle #LBD
# p='', t=1260 on xingu @ 2017-09-01T11:16:55+09:00
"mios-lbd", 1, 100,      0.68
"mios-lbd", 2, 125,      1.17
"mios-lbd", 3, 150,      2.14
"mios-lbd", 4, 175,      5.31
"mios-lbd", 5, 200,      13.92
"mios-lbd", 6, 225,      36.88
"mios-lbd", 7, 250,      112.80
"mios-lbd", 8, "een",    4.54
"mios-lbd", 9, "bmc",    2.91
"mios-lbd", 10, "38b",   115.70

shnarazk · 2017-09-01T07:58:13Z

060f85b

$ sat-benchmark -3 250 -L 100 -s mios-lbd
solver, num, target, time
# 2017-09-01T16:53 mios-lbd ; mios lbd:PR#36
# p='', t=1260 on xingu @ 2017-09-01T16:54:01+09:00
"mios-lbd", 1, 100,      0.69
"mios-lbd", 2, 125,      1.29
"mios-lbd", 3, 150,      2.27
"mios-lbd", 4, 175,      7.01
"mios-lbd", 5, 200,      17.72
"mios-lbd", 6, 225,      44.52
"mios-lbd", 7, 250,      133.84
"mios-lbd", 8, "een",    5.18
"mios-lbd", 9, "bmc",    3.30
"mios-lbd", 10, "38b",   5.80

shnarazk · 2017-09-01T12:18:07Z

Too many core dumps 😟

shnarazk · 2017-09-01T12:47:01Z

wrong result

eliminate protected field

# 2017-09-01T21:42 /home/narazaki/.local/bin/mios-lbd ; mios lbd:PR#36
# p='', t=1260 on smithi @ 2017-09-01T21:43:35+09:00
"mios-lbd", 1, 200,      11.05
"mios-lbd", 2, 225,      27.22
"mios-lbd", 3, 250,      83.22
"mios-lbd", 4, "een",    4.08
"mios-lbd", 5, "bmc",    2.21
"mios-lbd", 6, "38b",    31.48

460e2b5: simplify sortClauses

# 2017-09-01T21:55 /home/narazaki/.local/bin/mios-lbd ; mios lbd:PR#36
# p='', t=1260 on smithi @ 2017-09-01T21:55:21+09:00
"mios-lbd", 1, 200,      10.88
"mios-lbd", 2, 225,      26.60
"mios-lbd", 3, 250,      80.74
"mios-lbd", 4, "een",    3.88
"mios-lbd", 5, "bmc",    2.04
"mios-lbd", 6, "38b",    30.28

shnarazk · 2017-09-02T05:26:31Z

wrong result

5dfcb60

# 2017-09-02T14:19 mios-lbd ; mios lbd:PR#36
# p='', t=1260 on smithi @ 2017-09-02T14:19:41+09:00
"mios-lbd", 1, 75,       0.64
"mios-lbd", 2, 100,      0.99
"mios-lbd", 3, 125,      1.57
"mios-lbd", 4, 150,      2.66
"mios-lbd", 5, 175,      6.85
"mios-lbd", 6, 200,      21.32
"mios-lbd", 7, 225,      72.87
"mios-lbd", 8, 250,       246.41
"mios-lbd", 9, "een",    3.85
"mios-lbd", 10, "bmc",   2.00
"mios-lbd", 11, "38b",   17.74

shnarazk · 2017-09-04T00:28:10Z

wrong result

8232f99: longer period for large problems + early restart

restart factor was changed from 1.5 to 1.4 (quick restart)
clauseDB reduction trigger = number-of-the-given-clauses

# 2017-09-03T11:28 mios-lbd ; mios lbd:PR#36
# p='', t=1260 on smithi @ 2017-09-04T09:28:38+09:00
"mios-lbd", 1, 75,       0.71
"mios-lbd", 2, 100,      1.04
"mios-lbd", 3, 125,      1.64
"mios-lbd", 4, 150,      2.32
"mios-lbd", 5, 175,      5.20
"mios-lbd", 6, 200,      13.12
"mios-lbd", 7, 225,      33.41
"mios-lbd", 8, 250,      105.82
"mios-lbd", 9, "een",    3.88
"mios-lbd", 10, "bmc",   2.12
"mios-lbd", 11, "38b",   11.56

shnarazk · 2017-09-04T09:19:30Z

wrong result

rethink on `an'lastDL` (in progress)

update LBD on 8232f99

Firstly, each time a learnt clause is used in unit-propagation (it is a reason of a propagated lit- eral), we compute a new LBD score and update it if neces- sary. Secondly, we explicitly increase the score of variables of the learnt clause that were propagated by a glue clause.

drop rankOf based on clause size
update LBD when a learnt is checked in analyze
rewritten on an'lastLD

# p='', t=1260 on xingu @ 2017-09-04T13:15:59+09:00, 8232f99
"mios-lbd", 1, 100,      0.84
"mios-lbd", 2, 125,      1.58
"mios-lbd", 3, 150,      2.76
"mios-lbd", 4, 175,      7.51
"mios-lbd", 5, 200,      18.45
"mios-lbd", 6, 225,      42.74
"mios-lbd", 7, 250,      133.29
"mios-lbd", 8, "een",    4.93
"mios-lbd", 9, "bmc",    2.87
"mios-lbd", 10, "38b",   17.08

# just update LBD of learnt clauses used in analyze phase
"mios-lbd", 1, 100,      0.71
"mios-lbd", 2, 125,      1.17
"mios-lbd", 3, 150,      2.16
"mios-lbd", 4, 175,      6.01
"mios-lbd", 5, 200,      15.93
"mios-lbd", 6, 225,      41.81
"mios-lbd", 7, 250,      132.23
"mios-lbd", 8, "een",    4.32
"mios-lbd", 9, "bmc",    3.17
"mios-lbd", 10, "38b",   17.33

# 2017-09-04T18:25   the best so far after refactoring
"mios-lbd", 1, 100,      0.68                                                           
"mios-lbd", 2, 125,      1.15                                                           
"mios-lbd", 3, 150,      2.03                                                           
"mios-lbd", 4, 175,      6.59                                                           
"mios-lbd", 5, 200,      16.22                                                          
"mios-lbd", 6, 225,      43.38                                                          
"mios-lbd", 7, 250,      133.90                                                         
"mios-lbd", 8, "een",    5.03                                                           
"mios-lbd", 9, "bmc",    2.61                                                           
"mios-lbd", 10, "38b",   17.

shnarazk · 2017-09-05T01:42:06Z

src/SAT/Mios/Glucose.hs

+      l <- getNth level . lit2var =<< getNth vec i
+      x <- getNth lbd'seen l
+      if x /= k
+        then setNth lbd'seen l 1 >> loop (i + 1) (n + 1)


Here's a terrible bug. It must be setNth lbd'seen l k

* Glucose.hs: fix LBD computation * `asList` should contain the first element of 'Vec' * validate LBD computation; update the value in `analyze` * check the soundness of learnt-reduction

shnarazk · 2017-09-06T04:53:13Z

cea31b7

* Glucose.hs: fix LBD computation * `asList` should contain the first element of 'Vec' * validate LBD computation; update the value in `analyze` * check the soundness of learnt-reduction

- p='', t=1260 on xingu @ 2017-09-08T12:52:42+09:00 "mios-lbd", 1, 100, 0.67 "mios-lbd", 2, 125, 1.18 "mios-lbd", 3, 150, 2.07 "mios-lbd", 4, 175, 6.01 "mios-lbd", 5, 200, 16.10 "mios-lbd", 6, 225, 51.00 "mios-lbd", 7, 250, 179.73 "mios-lbd", 8, "een", 5.10 "mios-lbd", 9, "bmc", 3.25 "mios-lbd", 10, "38b", 14.54

shnarazk · 2017-09-08T04:01:37Z

bff1cc1 -- using a larger value for restartBase is important.

# p='', t=1260 on xingu @ 2017-09-08T12:52:42+09:00
"mios-lbd", 1, 100,      0.67
"mios-lbd", 2, 125,      1.18
"mios-lbd", 3, 150,      2.07
"mios-lbd", 4, 175,      6.01
"mios-lbd", 5, 200,      16.10
"mios-lbd", 6, 225,      51.00
"mios-lbd", 7, 250,      179.73
"mios-lbd", 8, "een",    5.10
"mios-lbd", 9, "bmc",    3.25
"mios-lbd", 10, "38b",   14.54

restartBase = sqrt $ nc * nv

# p='', t=1260 on xingu @ 2017-09-08T12:48:29+09:00
"mios-lbd", 1, 100,      0.77
"mios-lbd", 2, 125,      1.27
"mios-lbd", 3, 150,      2.00
"mios-lbd", 4, 175,      5.33
"mios-lbd", 5, 200,      15.49
"mios-lbd", 6, 225,      45.80
"mios-lbd", 7, 250,      146.84
"mios-lbd", 8, "een",    4.49
"mios-lbd", 9, "bmc",    3.21
"mios-lbd", 10, "38b",   9.95

The latter is better, but I pick up the former for simplicity.

shnarazk · 2017-09-08T04:10:59Z

Note: cherrypicking the restart w/o phases

# p='', t=1260 on xingu @ 2017-09-08T13:06:16+09:00
"mios-lbd", 1, 100,      0.63
"mios-lbd", 2, 125,      1.19
"mios-lbd", 3, 150,      2.14
"mios-lbd", 4, 175,      4.86
"mios-lbd", 5, 200,      14.80
"mios-lbd", 6, 225,      39.17
"mios-lbd", 7, 250,      132.83
"mios-lbd", 8, "een",    5.10
"mios-lbd", 9, "bmc",    3.27
"mios-lbd", 10, "38b",   10.46

👍

shnarazk · 2017-09-09T03:05:59Z

shnarazk · 2017-09-10T05:50:14Z

This PR is followed by #42

merge #36 #39 #40 #43 #44 #45 #41 - use LBD - not use Luby - eliminate some fields in Clause - add some utilities

update IDs

0e59b88

1st implementation of LBD that works

25eafb3

shnarazk changed the title ~~implement LBD~~ implement LBD again (4.1.2) Sep 1, 2017

shnarazk changed the title ~~implement LBD again (4.1.2)~~ Implement LBD again (4.1.2) Sep 1, 2017

shnarazk mentioned this pull request Sep 1, 2017

TODO for 1.4.2 #15

Closed

4 tasks

shnarazk self-assigned this Sep 1, 2017

shnarazk added 2 commits September 1, 2017 16:54

A better reduction approach based on LBD values

0b6fa18

embed the PR number into versionID

060f85b

delete protected

460e2b5

shnarazk added the new implementation label Sep 2, 2017

try a conventional values for reduceDB

5dfcb60

exp. on reduction period

8232f99

exp: restart=1.4, reduction=min nv 1000

9017e86

shnarazk commented Sep 5, 2017

View reviewed changes

shnarazk and others added 7 commits September 5, 2017 11:09

Validate LBD implementation (#37)

859d0f4

* Glucose.hs: fix LBD computation * `asList` should contain the first element of 'Vec' * validate LBD computation; update the value in `analyze` * check the soundness of learnt-reduction

tiny changes

cea31b7

sort literals in clauses (cherry-picked)

2c195a8

fix crash

030d1e5

delete debug code

c2c80b2

change indentation

05eddb5

change the reduciton limit

cc6f5d7

fix an indentation

c40264a

shnarazk and others added 22 commits September 8, 2017 09:38

1st implementation of LBD that works

a32115f

A better reduction approach based on LBD values

b9092dc

embed the PR number into versionID

b5c4600

delete protected

e907c9d

Validate LBD implementation (#37)

dca794d

* Glucose.hs: fix LBD computation * `asList` should contain the first element of 'Vec' * validate LBD computation; update the value in `analyze` * check the soundness of learnt-reduction

tiny changes

27c412f

sort literals in clauses (cherry-picked)

edb4f28

fix crash

5307780

delete debug code

964bad0

change indentation

7bd5e57

change the reduciton limit

bbf336e

fix an indentation

59bf6e8

A better reduction approach based on LBD values

7f7cad9

try a conventional values for reduceDB

c29f7d0

exp: restart=1.4, reduction=min nv 1000

bd8ed42

tiny changes

9040f5c

sort literals in clauses (cherry-picked)

33723e0

fix crash

47d2fd3

delete debug code

f5522e0

change indentation

7b299d7

Merge branch 'lbd' of github.com:shnarazk/mios into lbd

1dad504

Merge branch 'WIP-for-1.4.2' into lbd

b2036ee

shnarazk merged commit fb1917a into WIP-for-1.4.2 Sep 8, 2017

shnarazk added this to the 1.4.2 milestone Sep 9, 2017

shnarazk added a commit that referenced this pull request Oct 21, 2017

mios verision 1.5.0

e176288

merge #36 #39 #40 #43 #44 #45 #41 - use LBD - not use Luby - eliminate some fields in Clause - add some utilities

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement LBD again (4.1.2) #36

Implement LBD again (4.1.2) #36

shnarazk commented Sep 1, 2017 •

edited

shnarazk commented Sep 1, 2017 •

edited

shnarazk commented Sep 1, 2017

shnarazk commented Sep 1, 2017

shnarazk commented Sep 1, 2017 •

edited

shnarazk commented Sep 2, 2017 •

edited

shnarazk commented Sep 4, 2017 •

edited

shnarazk commented Sep 4, 2017 •

edited

shnarazk Sep 5, 2017 •

edited

shnarazk commented Sep 6, 2017

shnarazk commented Sep 8, 2017 •

edited

shnarazk commented Sep 8, 2017

shnarazk commented Sep 9, 2017

shnarazk commented Sep 10, 2017

Implement LBD again (4.1.2) #36

Implement LBD again (4.1.2) #36

Conversation

shnarazk commented Sep 1, 2017 • edited

shnarazk commented Sep 1, 2017 • edited

shnarazk commented Sep 1, 2017

shnarazk commented Sep 1, 2017

shnarazk commented Sep 1, 2017 • edited

wrong result

shnarazk commented Sep 2, 2017 • edited

wrong result

shnarazk commented Sep 4, 2017 • edited

wrong result

shnarazk commented Sep 4, 2017 • edited

wrong result

rethink on an'lastDL (in progress)

shnarazk Sep 5, 2017 • edited

Choose a reason for hiding this comment

shnarazk commented Sep 6, 2017

shnarazk commented Sep 8, 2017 • edited

shnarazk commented Sep 8, 2017

shnarazk commented Sep 9, 2017

shnarazk commented Sep 10, 2017

shnarazk commented Sep 1, 2017 •

edited

shnarazk commented Sep 1, 2017 •

edited

shnarazk commented Sep 1, 2017 •

edited

shnarazk commented Sep 2, 2017 •

edited

shnarazk commented Sep 4, 2017 •

edited

shnarazk commented Sep 4, 2017 •

edited

rethink on `an'lastDL` (in progress)

shnarazk Sep 5, 2017 •

edited

shnarazk commented Sep 8, 2017 •

edited