shnarazk commented 6 years ago

$ mios-48.0 -X --stat ../SATbench/SR2015/itox_vc1130.cnf 
## [                                   itox_vc1130.cnf]
NumOfBackjump: 6030
NumOfRestart: 8
NumOfPropagation: 23799789

$ mios-48 -X --stat ../SATbench/SR2015/itox_vc1130.cnf 
## [                                   itox_vc1130.cnf]
NumOfBackjump: 2520
NumOfRestart: 6
NumOfPropagation: 22114736

shnarazk commented 6 years ago

$ mios-48 -X --stat ../SATbench/SR2015/itox_vc1130.cnf  | head -10
## [                                   itox_vc1130.cnf]
NumOfBackjump: 2520
NumOfRestart: 6
NumOfPropagation: 22114736
(298369,297739)
(298361,297737)
(298105,297673)
(149572,149509)
(149184,149177)
(298097,297671)
(298089,297669)
(298081,297667)
(298073,297665)
(298065,297663)
┌─[t%4]─[narazaki@xingu]─[mios@10-27T16:34:23]─[biclause-comparison*]
$ mios-48.0 -X --stat ../SATbench/SR2015/itox_vc1130.cnf  | head -10
(298369,297739)
(298361,297737)
(298105,297673)
(149572,149509)
(149184,149177)
(298097,297671)
(298089,297669)
(298081,297667)
(298073,297665)
(298065,297663)
## [                                   itox_vc1130.cnf]
NumOfBackjump: 6030
NumOfRestart: 8
NumOfPropagation: 23799789

shnarazk commented 6 years ago

$ mios-48 -X --stat ../SATbench/SR2015/itox_vc1130.cnf  
     100 |   141459   429691 |   157553       93 |   383413
     250 |   141438   429691 |   173308      236 |   837879
     475 |   141438   429691 |   190639      461 |   927249
     812 |   141438   429691 |   209703      798 |  1194263
    1318 |   141335   429691 |   230673     1298 |  6468240
    2077 |   141316   429691 |   253741     2038 | 16174392
## [                                   itox_vc1130.cnf]
NumOfBackjump: 2520
NumOfRestart: 6
NumOfPropagation: 22114736
┌─[t%4]─[narazaki@xingu]─[mios@10-27T16:40:38]─[biclause*]
$ mios-48.0 -X --stat ../SATbench/SR2015/itox_vc1130.cnf  
     100 |   141459   429691 |   157553       93 |   382593
     250 |   141441   429691 |   173308      239 |   727360
     475 |   141429   429691 |   190639      451 |  2175874
     812 |   141429   429691 |   209703      788 |  2255446
    1318 |   141429   429691 |   230673     1294 |  2462122
    2077 |   141291   429691 |   253741     2041 |  3584079
    3216 |   141194   429691 |   279115     3107 |  4940512
    4924 |   141194   429691 |   307026     4815 |  5701986
## [                                   itox_vc1130.cnf]
NumOfBackjump: 6030
NumOfRestart: 8
NumOfPropagation: 23799789

shnarazk commented 6 years ago

memo during a weekend power cut

propagate failed to update biclauses' blockers in some cases.
propagate has to return a right ordered BiClause. This order affects the order of literals in the heap, leading to the different futures.
analyze failed to push some literals that are bumped later.

And the last problem: analyze in the original branch distinguishes problem binary clauses from learnt binary clauses. That's impossible in biclause branch. 😕 I think biclauses shouldn't be learnts. So the original branch is the branch to be revised.

shnarazk commented 6 years ago

$ time mios-48p ~/Repositories/SATbench/SR2015/itox_vc1130.cnf -X --stat
## [                                   itox_vc1130.cnf]
NumOfBackjump: 6231
NumOfRestart: 8
NumOfPropagation: 27554818

real    0m24.681s
user    0m24.554s
sys     0m0.127s

$ time mios-48 Repositories/SATbench/SR2015/itox_vc1130.cnf -X --stat
## [                                   itox_vc1130.cnf]
NumOfBackjump: 6231
NumOfRestart: 8
NumOfPropagation: 27554818

real    0m23.586s
user    0m23.434s
sys     0m0.151s

shnarazk commented 6 years ago

yet another problem

$ sat-benchmark -3 250 -s mios-1.5.0 mios-48p mios-48
solver, num, target, time
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-30T16:38:53+09:00
# 2017-10-21T10:46 mios-1.5.0; mios-1.5.0 https://github.com/shnarazk/mios/
"mios-1.5.0", 1, 175,    3.89
"mios-1.5.0", 2, 200,    11.87
"mios-1.5.0", 3, 225,    33.36
"mios-1.5.0", 4, 250,    81.42
"mios-1.5.0", 5, "itox",         11.97
"mios-1.5.0", 6, "m283",         40.64
"mios-1.5.0", 7, "38b",  46.42
"mios-1.5.0", 8, "48b",  60.71

# 2017-10-30T16:35 mios-48p; mios-1.5.0WIP paralell implementation with #48
# call simplifyDB only after restart
"mios-48p", 1, 175,      3.95
"mios-48p", 2, 200,      11.76
"mios-48p", 3, 225,      33.79
"mios-48p", 4, 250,      79.27
"mios-48p", 5, "itox",   20.09
"mios-48p", 6, "m283",   39.76
"mios-48p", 7, "38b",    8.19
"mios-48p", 8, "48b",    150.64

# 2017-10-30T16:29 mios-48; mios-1.5.0WIP #48
# call simplifyDB only after restart
"mios-48", 1, 175,       3.98
"mios-48", 2, 200,       12.10
"mios-48", 3, 225,       34.36
"mios-48", 4, 250,       80.57
"mios-48", 5, "itox",    18.94
"mios-48", 6, "m283",    38.62
"mios-48", 7, "38b",     8.13
"mios-48", 8, "48b",     152.16

solver, num, target, time
# 2017-10-30T16:56 mios-48; mios-1.5.0WIP #48
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-30T16:57:09+09:00, revert on call sites
"mios-48", 1, 175,       3.98
"mios-48", 2, 200,       12.00
"mios-48", 3, 225,       34.34
"mios-48", 4, 250,       80.61
"mios-48", 5, "itox",    19.71
"mios-48", 6, "m283",    37.04
"mios-48", 7, "38b",     8.20
"mios-48", 8, "48b",     291.94          <= not better, much worser

shnarazk commented 6 years ago

evaluation of variants

# 2017-10-30T16:29 mios-48; mios-1.5.0WIP #48, simplify after restart
"mios-48", 1, 175,       3.98
"mios-48", 2, 200,       12.10
"mios-48", 3, 225,       34.36
"mios-48", 4, 250,       80.57
"mios-48", 5, "itox",    18.94
"mios-48", 6, "m283",    38.62
"mios-48", 7, "38b",     8.13
"mios-48", 8, "48b",     152.16

# on xingu, revert on call sites
"mios-48", 1, 175,       3.98
"mios-48", 2, 200,       12.00
"mios-48", 3, 225,       34.34
"mios-48", 4, 250,       80.61
"mios-48", 5, "itox",    19.71
"mios-48", 6, "m283",    37.04
"mios-48", 7, "38b",     8.20
"mios-48", 8, "48b",     291.94

# on xingu, simplify after restart, push biclause into clauses
"mios-48", 1, 175,       4.13
"mios-48", 2, 200,       11.97
"mios-48", 3, 225,       35.43
"mios-48", 4, 250,       80.19
"mios-48", 5, "itox",    19.36
"mios-48", 6, "m283",    138.19
"mios-48", 7, "38b",     57.57
"mios-48", 8, "48b",     239.41

# on xingu, simplify after restart, push biclause into learns, all subsumes
"mios-48", 1, 175,       4.31
"mios-48", 2, 200,       12.11
"mios-48", 3, 225,       32.57
"mios-48", 4, 250,       79.27
"mios-48", 5, "itox",    88.30
"mios-48", 6, "m283",    121.22
"mios-48", 7, "38b",     22.15
"mios-48", 8, "48b",     541.59

# on xingu, simplify after restart, push biclause into learns, clauses subsume
"mios-48", 1, 175,       4.03
"mios-48", 2, 200,       12.09
"mios-48", 3, 225,       34.59
"mios-48", 4, 250,       80.78
"mios-48", 5, "itox",    89.65
"mios-48", 6, "m283",    37.48
"mios-48", 7, "38b",     8.83
"mios-48", 8, "48b",     1243.37

shnarazk commented 6 years ago

another topic: normalize reason at level = 0

+simplify +normalize

## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 58183
NumOfRestart: 13
NumOfPropagation: 4002991
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 116881
NumOfRestart: 15
NumOfPropagation: 77312363
## [                                   itox_vc1130.cnf]
NumOfBackjump: 6013
NumOfRestart: 8
NumOfPropagation: 23723317
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 1020089
NumOfRestart: 21
NumOfPropagation: 96366811

+simplify - normalize

## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 58183
NumOfRestart: 13
NumOfPropagation: 4002991
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 116881
NumOfRestart: 15
NumOfPropagation: 77312363
## [                                   itox_vc1130.cnf]
NumOfBackjump: 6013
NumOfRestart: 8
NumOfPropagation: 23723317
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 1020089
NumOfRestart: 21
NumOfPropagation: 96366811

-simplify

## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 58183
NumOfRestart: 13
NumOfPropagation: 4002991
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 116881
NumOfRestart: 15
NumOfPropagation: 77312363
## [                                   itox_vc1130.cnf]
NumOfBackjump: 6013
NumOfRestart: 8
NumOfPropagation: 23723317
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 1077311
NumOfRestart: 21
NumOfPropagation: 99290038

shnarazk commented 6 years ago

whether we call subsume?

+subsumeAll clauses

## [                                   itox_vc1130.cnf]
NumOfBackjump: 6,013
NumOfRestart: 8
NumOfPropagation: 23,723,317
## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 58,183
NumOfRestart: 13
NumOfPropagation: 4,002,991
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 116,881
NumOfRestart: 15
NumOfPropagation: 77,312,363
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 1,077,311
NumOfRestart: 21
NumOfPropagation: 99,290,038

-subsumeAll clauses

## [                                   itox_vc1130.cnf]
NumOfBackjump: 5,992
NumOfRestart: 8
NumOfPropagation: 22,175,799
## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 58,183
NumOfRestart: 13
NumOfPropagation: 4,002,993
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 116,881
NumOfRestart: 15
NumOfPropagation: 77,312,363
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 1,306,450
NumOfRestart: 21
NumOfPropagation: 115,707,874

-subsume, pushTo learnt?

## [                                   itox_vc1130.cnf]
NumOfBackjump: 5,992
NumOfRestart: 8
NumOfPropagation: 22,175,799
## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 314,658
NumOfRestart: 18
NumOfPropagation: 23,986,213
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 205,249
NumOfRestart: 17
NumOfPropagation: 134,599,190
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 3,866,345
NumOfRestart: 24
NumOfPropagation: 378,615,940

-subsume, pushTo clauses

## [                                   itox_vc1130.cnf]
NumOfBackjump: 6,013
NumOfRestart: 8
NumOfPropagation: 23,723,317
## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 348,659
NumOfRestart: 18
NumOfPropagation: 27,850,532
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 205,249
NumOfRestart: 17
NumOfPropagation: 134,599,190
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 3,159,681
NumOfRestart: 23
NumOfPropagation: 296,605,447

subsume clauses, pushTo learnts

## [                                   itox_vc1130.cnf]
NumOfBackjump: 6,013
NumOfRestart: 8
NumOfPropagation: 23,723,317
## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 58,183
NumOfRestart: 13
NumOfPropagation: 4,002,991
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 116,881
NumOfRestart: 15
NumOfPropagation: 77,312,363
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 1,020,089
NumOfRestart: 21
NumOfPropagation: 96,366,811

subsume both, pushTo learnts

## [                                   itox_vc1130.cnf]
NumOfBackjump: 6,013
NumOfRestart: 8
NumOfPropagation: 23,723,317
## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 103,839
NumOfRestart: 15
NumOfPropagation: 7,870,764
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 192,915
NumOfRestart: 16
NumOfPropagation: 129,492,998
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 2,027,565
NumOfRestart: 22
NumOfPropagation: 194,218,999

subsume size < 5, pushTo learnts

## [                                   itox_vc1130.cnf]
NumOfBackjump: 6,013
NumOfRestart: 8
NumOfPropagation: 23,723,317
## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 177,228
NumOfRestart: 16
NumOfPropagation: 14,042,528
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 302,216
NumOfRestart: 18
NumOfPropagation: 199,160,464
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 387,824
NumOfRestart: 18
NumOfPropagation: 39,904,459

subsume size > 4, pushTo learnts

## [                                   itox_vc1130.cnf]
NumOfBackjump: 5,992
NumOfRestart: 8
NumOfPropagation: 22,175,799
## [                              38bits_10.dimacs.cnf]
NumOfBackjump: 42,266
NumOfRestart: 13
NumOfPropagation: 2,702,281
## [                     manthey_DimacsSorter_28_3.cnf]
NumOfBackjump: 359,658
NumOfRestart: 18
NumOfPropagation: 233,529,557
## [                              44bits_11.dimacs.cnf]
NumOfBackjump: 3,537,647
NumOfRestart: 24
NumOfPropagation: 333,020,106

shnarazk commented 6 years ago

whether we call subsume?

problem	backjumps	restarts	propagations
+subsumeAll clauses	---------	--------	--------
itox_vc1130.cnf	6,013	8	23,723,317
38bits_10.dimacs.cnf	58,183	13	4,002,991
manthey_DimacsSorter_28_3.cnf	116,881	15	77,312,363
44bits_11.dimacs.cnf	1,077,311	21	99,290,038
-subsumeAll clauses	---------	---------	---------
itox_vc1130.cnf	5,992	8	22,175,799
38bits_10.dimacs.cnf	58,183	13	4,002,993
manthey_DimacsSorter_28_3.cnf	116,881	15	77,312,363
44bits_11.dimacs.cnf	1,306,450	21	115,707,874

problem	backjumps	restarts	propagations
-subsume, pushTo learnt?	---------	--------	--------
itox_vc1130.cnf	5,992	8	22,175,799
38bits_10.dimacs.cnf	314,658	18	23,986,213
manthey_DimacsSorter_28_3.cnf	205,249	17	134,599,190
44bits_11.dimacs.cnf	3,866,345	24	378,615,940
-subsume, pushTo clauses	---------	---------	---------
itox_vc1130.cnf	6,013	8	23,723,317
38bits_10.dimacs.cnf	348,659	18	27,850,532
manthey_DimacsSorter_28_3.cnf	205,249	17	134,599,190
44bits_11.dimacs.cnf	3,159,681	23	296,605,447
subsume clauses, pushTo learnts	---------	---------	---------
itox_vc1130.cnf	6,013	8	23,723,317
38bits_10.dimacs.cnf	58,183	13	4,002,991
manthey_DimacsSorter_28_3.cnf	116,881	15	77,312,363
44bits_11.dimacs.cnf	1,020,089	21	96,366,811
subsume clauses:4<size, pushTo learnts	---------	---------	---------
itox_vc1130.cnf	5,992	8	22,175,799
38bits_10.dimacs.cnf	58,183	13	4,002,993
manthey_DimacsSorter_28_3.cnf	116,881	15	77,312,363
44bits_11.dimacs.cnf	1,659,587	22	151,964,845
subsume clauses:size<5, pushTo learnts	---------	---------	---------
itox_vc1130.cnf	6,013	8	23,723,317
38bits_10.dimacs.cnf	58,183	13	4,002,991
manthey_DimacsSorter_28_3.cnf	116,881	15	77,312,363
44bits_11.dimacs.cnf	1,020,089	21	96,366,811
subsume clauses, pushTo clauses	---------	---------	---------
itox_vc1130.cnf	6,013	8	23,723,317
38bits_10.dimacs.cnf	348,659	18	27,850,532
manthey_DimacsSorter_28_3.cnf	205,249	17	134,599,190
44bits_11.dimacs.cnf	3,159,681	23	296,605,447
subsume both, pushTo learnts	---------	---------	---------
itox_vc1130.cnf	6,013	8	23,723,317
38bits_10.dimacs.cnf	103,839	15	7,870,764
manthey_DimacsSorter_28_3.cnf	192,915	16	129,492,998
44bits_11.dimacs.cnf	2,027,565	22	194,218,999
subsume both size < 5, pushTo learnts	---------	---------	---------
itox_vc1130.cnf	6,013	8	23,723,317
38bits_10.dimacs.cnf	177,228	16	14,042,528
manthey_DimacsSorter_28_3.cnf	302,216	18	199,160,464
44bits_11.dimacs.cnf	387,824	18	39,904,459
subsume both size > 4, pushTo learnts	---------	---------	---------
itox_vc1130.cnf	5,992	8	22,175,799
38bits_10.dimacs.cnf	42,266	13	2,702,281
manthey_DimacsSorter_28_3.cnf	359,658	18	233,529,557
44bits_11.dimacs.cnf	3,537,647	24	333,020,106

shnarazk / mios

Biclause comparison on itox #51

memo during a weekend power cut

yet another problem

another topic: normalize reason at level = 0

whether we call subsume?

whether we call subsume?