Biclause optimization #48

shnarazk · 2017-10-23T23:11:12Z

changelog

simplifyDB is called only after restart. Since this means decision level is zero, locked is removed from it. Note: In some problems, the number of propagations increases by calling simplifyDB. Is it possible!? 😲

objective

Binary clause, or biclause, has a specific representation.
biclause should be handled as a kind of problem clause.
learning a binary clause should be a trigger to simplify or subsumpiton.

related branch

investigate the probability of biclause
comparison to the previous code: Biclause comparison on itox #51

This is a week project. 👨‍⚕️
cf #19, #28

shnarazk · 2017-10-24T09:16:21Z

# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-24T18:02:46+09:00
# 2017-10-24T18:02 mios-48; mios-1.5.0WIP #48
"mios-48", 1, 175,       4.83
"mios-48", 2, 200,       13.75
"mios-48", 3, 225,       40.79
"mios-48", 4, 250,       94.78
"mios-48", 5, "itox",    21.08
"mios-48", 6, "m283",    35.14
"mios-48", 7, "38b",     18.61
"mios-48", 8, "48b",     221.15
# 2017-10-21T10:46 mios-1.5.0; mios-1.5.0 https://github.com/shnarazk/mios/
"mios-1.5.0", 1, 175,    3.85
"mios-1.5.0", 2, 200,    11.78
"mios-1.5.0", 3, 225,    33.13
"mios-1.5.0", 4, 250,    80.74
"mios-1.5.0", 5, "itox",         13.51
"mios-1.5.0", 6, "m283",         43.28
"mios-1.5.0", 7, "38b",  46.35
"mios-1.5.0", 8, "48b",  60.05

shnarazk · 2017-10-24T10:44:18Z

# 2017-10-24T19:27 mios-48; mios-1.5.0WIP #48
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-24T19:35:30+09:00
"mios-48", 1, 175,       4.60
"mios-48", 2, 200,       13.61
"mios-48", 3, 225,       36.46
"mios-48", 4, 250,       82.98
"mios-48", 5, "itox",    20.88
"mios-48", 6, "m283",    38.76
"mios-48", 7, "38b",     19.17
"mios-48", 8, "48b",     223.81

shnarazk · 2017-10-25T01:20:56Z

# 2017-10-25T09:32 mios-48; mios-1.5.0WIP #48, inplaceSubsume on learnts
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T09:33:15+09:00
"mios-48", 1, 175,       3.77
"mios-48", 2, 200,       11.54
"mios-48", 3, 225,       33.38
"mios-48", 4, 250,       79.62
"mios-48", 5, "itox",    22.30
"mios-48", 6, "m283",    82.48
"mios-48", 7, "38b",     23.86
"mios-48", 8, "48b",     644.31   
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T09:49:14+09:00, inplaceSubsume on clauses
"mios-48", 1, 175,       3.83
"mios-48", 2, 200,       11.63
"mios-48", 3, 225,       33.52
"mios-48", 4, 250,       80.00
"mios-48", 5, "itox",    24.90
"mios-48", 6, "m283",    76.95
"mios-48", 7, "38b",     23.94
"mios-48", 8, "48b",     636.22
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T10:05:58+09:00, subsumeAll on both
"mios-48", 1, 175,       4.25
"mios-48", 2, 200,       11.99
"mios-48", 3, 225,       33.72
"mios-48", 4, 250,       81.66
"mios-48", 5, "itox",    117.57
"mios-48", 6, "m283",    99.59
"mios-48", 7, "38b",     32.53
"mios-48", 8, "48b",     392.78

shnarazk · 2017-10-25T12:59:54Z

A very interesting behavior: difference between 3-SATs and industrials on 9800e1d

solver, num, target, time
# 2017-10-25T21:15 mios-48; mios-1.5.0WIP #48, pushTo learnts 
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T21:16:34+09:00
"mios-48", 2, 200,       11.79
"mios-48", 3, 225,       33.63
"mios-48", 4, 250,       81.71
"mios-48", 5, "itox",    22.16
"mios-48", 6, "m283",    38.49
"mios-48", 7, "38b",     15.71
"mios-48", 8, "48b",     80.84

# 2017-10-25T21:22 mios-48; mios-1.5.0WIP #48, pushTo clauses
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T21:22:22+09:00
"mios-48", 2, 200,       11.53    -- good
"mios-48", 3, 225,       33.31.   -- good
"mios-48", 4, 250,       79.66    -- good
"mios-48", 5, "itox",    21.46
"mios-48", 6, "m283",    73.83    -- doubled
"mios-48", 7, "38b",     23.38
"mios-48", 8, "48b",     619.84  !!!

Some clauses lost a registration of watch literals.

shnarazk · 2017-10-27T02:50:59Z

shnarazk · 2017-11-12T05:41:34Z

# 2017-11-12T07:54 mios-52; mios-1.5.0WIP #52
"mios-52", 1, 175,       3.83
"mios-52", 2, 200,       11.87
"mios-52", 3, 225,       33.57
"mios-52", 4, 250,       82.40
"mios-52", 5, "itox",    12.83
"mios-52", 6, "m283",    39.92
"mios-52", 7, "38b",     47.47
"mios-52", 8, "44b",     58.80
# 2017-11-12T12:40 mios-48; mios-1.5.0WIP #52 #48
"mios-48", 1, 175,       3.94
"mios-48", 2, 200,       12.01
"mios-48", 3, 225,       34.56
"mios-48", 4, 250,       83.22
"mios-48", 5, "itox",    70.79
"mios-48", 6, "m283",    37.50
"mios-48", 7, "38b",     57.45
"mios-48", 8, "44b",     450.05

shnarazk · 2017-11-12T06:17:37Z

# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-11-12T15:09:38+09:00
"mios-48", 1, 175,       3.98
"mios-48", 2, 200,       12.08
"mios-48", 3, 225,       34.28
"mios-48", 4, 250,       84.04
"mios-48", 5, "itox",    62.81
"mios-48", 6, "m283",    37.28
"mios-48", 7, "38b",     74.19
"mios-48", 8, "44b",     121.93

parallel "mios-{} --stat -X ../SATbench/SR2015/38bits_10.dimacs.cnf " ::: 48 52 [ 38bits_10.dimacs.cnf] NumOfBackjump: 251267 NumOfRestart: 17 NumOfPropagation: 19348963 [ 38bits_10.dimacs.cnf] NumOfBackjump: 251267 NumOfRestart: 17 NumOfPropagation: 19348963

shnarazk · 2017-11-19T11:20:18Z

moved to #55

start a branch: biclause

0a75dee

shnarazk self-assigned this Oct 23, 2017

Clause.hs: add BiClause

23c4b50

shnarazk added the MiniSat2 label Oct 23, 2017

shnarazk added 3 commits October 24, 2017 10:03

ClauseManager.hs: implement asList for ClauseExtManager

074edef

WIP: seems to work

894dfd7

remove probes

089616a

implement analyzeRemovable for BiClause; slow down in some problems

f0be5de

shnarazk added 3 commits October 25, 2017 09:31

implement some methods on BiClause

953829c

WIP: simple subsume on learnts instead of full subsume on clauses

810fa42

fix an error

0fbb2f3

WIP: settings for experimentation

ab1fa0e

shnarazk added 2 commits October 25, 2017 22:00

simplify; back to 1.5.0

9800e1d

import a fix from #50

dce3cd6

Some clauses lost a registration of watch literals.

shnarazk added 3 commits October 27, 2017 14:06

Solver.hs: clauseNew uses BiClause

4357cae

Solver.hs: clauesNew sets valid blockers

1ecfdd5

[WIP] identical to 1.5.0

9f77901

shnarazk pushed a commit that referenced this pull request Oct 27, 2017

clauseNew: import a fix from #48

01a71bc

shnarazk added 7 commits October 27, 2017 16:31

newClauseFromStack returns BiClause if n == 2

63efca8

add a probe

7dca2ba

-probe; +verbose

323e13e

another probe

8b5f460

another probe for satisfiability of biclause

b5ebc39

update the probe

7bd76d4

reactivate generator probe

d010576

shnarazk added 21 commits November 12, 2017 11:36

Solver.hs: clauseNew uses BiClause

3f733d4

Solver.hs: clauesNew sets valid blockers

4f767ce

[WIP] identical to 1.5.0

4594927

newClauseFromStack returns BiClause if n == 2

83f6b9a

add a probe

e3b749b

-probe; +verbose

30613cd

another probe

e6e4705

another probe for satisfiability of biclause

a0f052e

update the probe

ff91437

reactivate generator probe

6f8c47a

stop simplify

74cb7bb

update probes

46402ab

As I said, #49 and #51 were synchrosized; removing probes

a163d46

remove probes; and FIX a BUG

14049de

ditto

6789032

non sync

1f12c1f

call simplify only after restart

3018326

refactored based on experimentation so far

d51dcd1

analyze.loopONLastDL; fix a bug and use LBD instead of size

2884e44

fix UPDATEVARCATIVITY

97a8f48

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

86bd5ba

analyze: add a marginal case

0a3151c

shnarazk added 2 commits November 12, 2017 17:05

almost revert the previous commit

a79f37c

shnarazk merged commit a79f37c into WIP-for-1.5.1 Nov 19, 2017

shnarazk deleted the biclause branch June 17, 2018 11:27

shnarazk restored the biclause branch June 19, 2018 14:03

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Biclause optimization #48

Biclause optimization #48

shnarazk commented Oct 23, 2017 •

edited

Loading

shnarazk commented Oct 24, 2017

shnarazk commented Oct 24, 2017

shnarazk commented Oct 25, 2017

shnarazk commented Oct 25, 2017 •

edited

Loading

shnarazk commented Oct 27, 2017

shnarazk commented Nov 12, 2017

shnarazk commented Nov 12, 2017

shnarazk commented Nov 19, 2017 •

edited

Loading

Biclause optimization #48

Biclause optimization #48

Conversation

shnarazk commented Oct 23, 2017 • edited Loading

changelog

objective

related branch

shnarazk commented Oct 24, 2017

shnarazk commented Oct 24, 2017

shnarazk commented Oct 25, 2017

shnarazk commented Oct 25, 2017 • edited Loading

shnarazk commented Oct 27, 2017

shnarazk commented Nov 12, 2017

shnarazk commented Nov 12, 2017

shnarazk commented Nov 19, 2017 • edited Loading

shnarazk commented Oct 23, 2017 •

edited

Loading

shnarazk commented Oct 25, 2017 •

edited

Loading

shnarazk commented Nov 19, 2017 •

edited

Loading