311 lines
32 KiB
Plaintext
311 lines
32 KiB
Plaintext
|
c ------------------- Paras list -------------------
|
||
|
|
c Name Type Now Default Comment
|
||
|
|
c DPS int 0 0 DPS/NPS
|
||
|
|
c DPS_period int 10000 10000 DPS sharing period
|
||
|
|
c margin int 0 0 DPS margin
|
||
|
|
c pakis int 1 1 Use pakis diversity
|
||
|
|
c reset int 0 0 Dynamically reseting
|
||
|
|
c reset_time int 10 10 Reseting base interval (seconds)
|
||
|
|
c share int 1 1 Sharing learnt clauses
|
||
|
|
c share_intv int 500000 500000 Sharing interval (microseconds)
|
||
|
|
c share_lits int 1500 1500 Sharing lits (per every #share_intv seconds)
|
||
|
|
c shuffle int 1 1 Use random shuffle
|
||
|
|
c simplify int 1 1 Use Simplify (only preprocess)
|
||
|
|
c threads int 32 32 Thread number
|
||
|
|
c times double 3600.000000 5000 Cutoff time
|
||
|
|
c config string "" Config file
|
||
|
|
c instance string /pub/data/chenzh/data/sat2022/0205e0724a8a912dde9ad7dfba2aee0b-003-23-80.cnf "" CNF format instance
|
||
|
|
c --------------------------------------------------
|
||
|
|
c [leader] preprocess(simplify) input data
|
||
|
|
c After preprocess: vars: 4288 -> 3814 , clauses: 132592 -> 75393 ,
|
||
|
|
c [CE] almost one cons: 509
|
||
|
|
c After preprocess: vars: 3814 -> 3813 , clauses: 75393 -> 75391 ,
|
||
|
|
c sz 5
|
||
|
|
c turns: 8
|
||
|
|
c After preprocess: vars: 3813 -> 3616 , clauses: 75391 -> 71955 ,
|
||
|
|
c [leader] hand out length of cnf instance to all nodes
|
||
|
|
c [leader] hand out cnf instance to all nodes
|
||
|
|
c [leader] hand out done!
|
||
|
|
c [worker] round 1, time: 0.0
|
||
|
|
c [worker] round 1, time: 0.0
|
||
|
|
c [worker] round 1, time: 0.0
|
||
|
|
c [worker] round 1, time: 0.0
|
||
|
|
c [worker] round 1, time: 0.0
|
||
|
|
c [worker] round 1, time: 0.0
|
||
|
|
c [worker] round 1, time: 0.0
|
||
|
|
c [worker] round 1, time: 0.0
|
||
|
|
c [worker] round 2, time: 0.524
|
||
|
|
c [worker] round 2, time: 0.526
|
||
|
|
c [worker] round 2, time: 0.543
|
||
|
|
c [worker] round 2, time: 0.577
|
||
|
|
c [worker] round 2, time: 0.515
|
||
|
|
c [worker] round 2, time: 0.602
|
||
|
|
c [worker] round 2, time: 0.570
|
||
|
|
c [worker] round 2, time: 0.614
|
||
|
|
c [worker] round 3, time: 1.45
|
||
|
|
c [worker] round 3, time: 1.108
|
||
|
|
c [worker] round 3, time: 1.102
|
||
|
|
c [worker] round 3, time: 1.80
|
||
|
|
c [worker] round 3, time: 1.154
|
||
|
|
c [worker] round 3, time: 1.236
|
||
|
|
c [worker] round 3, time: 1.231
|
||
|
|
c [worker] round 3, time: 1.215
|
||
|
|
c [worker] round 4, time: 1.612
|
||
|
|
c [worker] round 4, time: 1.584
|
||
|
|
c [worker] round 4, time: 1.623
|
||
|
|
c [worker] round 4, time: 1.676
|
||
|
|
c [worker] round 4, time: 1.735
|
||
|
|
c [worker] round 4, time: 1.716
|
||
|
|
c [worker] round 4, time: 1.785
|
||
|
|
c [worker] round 4, time: 1.836
|
||
|
|
c [worker] round 5, time: 2.85
|
||
|
|
c [worker] round 5, time: 2.179
|
||
|
|
c [worker] round 5, time: 2.238
|
||
|
|
c [worker] round 5, time: 2.247
|
||
|
|
c [worker] round 5, time: 2.284
|
||
|
|
c [worker] round 5, time: 2.294
|
||
|
|
c [worker] round 5, time: 2.369
|
||
|
|
c [worker] round 5, time: 2.369
|
||
|
|
c [worker] round 6, time: 2.592
|
||
|
|
c [worker] round 6, time: 2.776
|
||
|
|
c [worker] round 6, time: 2.792
|
||
|
|
c [worker] round 6, time: 2.818
|
||
|
|
c [worker] round 6, time: 2.806
|
||
|
|
c [worker] round 6, time: 2.860
|
||
|
|
c [worker] round 6, time: 2.877
|
||
|
|
c [worker] round 6, time: 3.4
|
||
|
|
c [worker] round 7, time: 3.94
|
||
|
|
c [worker] round 7, time: 3.318
|
||
|
|
c [worker] round 7, time: 3.322
|
||
|
|
c [worker] round 7, time: 3.321
|
||
|
|
c [worker] round 7, time: 3.380
|
||
|
|
c [worker] round 7, time: 3.409
|
||
|
|
c [worker] round 7, time: 3.473
|
||
|
|
c [worker] round 7, time: 3.512
|
||
|
|
c [worker] round 8, time: 3.600
|
||
|
|
c [worker] round 8, time: 3.827
|
||
|
|
c [worker] round 8, time: 3.826
|
||
|
|
c [worker] round 8, time: 3.888
|
||
|
|
c [worker] round 8, time: 3.989
|
||
|
|
c [worker] round 8, time: 3.930
|
||
|
|
c [worker] round 8, time: 4.18
|
||
|
|
c [worker] round 8, time: 4.21
|
||
|
|
c [worker] round 9, time: 4.102
|
||
|
|
c [worker] round 9, time: 4.330
|
||
|
|
c [worker] round 9, time: 4.357
|
||
|
|
c [worker] round 9, time: 4.404
|
||
|
|
c [worker] round 9, time: 4.506
|
||
|
|
c [worker] round 9, time: 4.440
|
||
|
|
c [worker] round 9, time: 4.532
|
||
|
|
c [worker] round 9, time: 4.535
|
||
|
|
c [worker] round 10, time: 4.603
|
||
|
|
c [worker] round 10, time: 4.838
|
||
|
|
c [worker] round 10, time: 4.867
|
||
|
|
c [worker] round 10, time: 4.906
|
||
|
|
c [worker] round 10, time: 5.14
|
||
|
|
c [worker] round 10, time: 4.945
|
||
|
|
c [worker] round 10, time: 5.36
|
||
|
|
c [worker] round 10, time: 5.43
|
||
|
|
c [worker] round 11, time: 5.108
|
||
|
|
c [worker] round 11, time: 5.342
|
||
|
|
c [worker] round 11, time: 5.375
|
||
|
|
c [worker] round 11, time: 5.412
|
||
|
|
c [worker] round 11, time: 5.517
|
||
|
|
c [worker] round 11, time: 5.451
|
||
|
|
c [worker] round 11, time: 5.544
|
||
|
|
c [worker] round 11, time: 5.548
|
||
|
|
c [worker] round 12, time: 5.609
|
||
|
|
c [worker] round 12, time: 5.878
|
||
|
|
c [worker] round 12, time: 5.874
|
||
|
|
c [worker] round 12, time: 5.920
|
||
|
|
c [worker] round 12, time: 6.26
|
||
|
|
c [worker] round 12, time: 5.959
|
||
|
|
c [worker] round 12, time: 6.49
|
||
|
|
c [worker] round 12, time: 6.71
|
||
|
|
c [worker] round 13, time: 6.112
|
||
|
|
c [worker] round 13, time: 6.381
|
||
|
|
c [worker] round 13, time: 6.378
|
||
|
|
c [worker] round 13, time: 6.428
|
||
|
|
c [worker] round 13, time: 6.534
|
||
|
|
c [worker] round 13, time: 6.463
|
||
|
|
c [worker] round 13, time: 6.564
|
||
|
|
c [worker] round 13, time: 6.579
|
||
|
|
c [worker] round 14, time: 6.616
|
||
|
|
c [worker] round 14, time: 6.885
|
||
|
|
c [worker] round 14, time: 6.881
|
||
|
|
c [worker] round 14, time: 6.933
|
||
|
|
c [worker] round 14, time: 6.967
|
||
|
|
c [worker] round 14, time: 7.46
|
||
|
|
c [worker] round 14, time: 7.70
|
||
|
|
c [worker] round 14, time: 7.86
|
||
|
|
c [worker] round 15, time: 7.120
|
||
|
|
c [worker] round 15, time: 7.391
|
||
|
|
c [worker] round 15, time: 7.386
|
||
|
|
c [worker] round 15, time: 7.438
|
||
|
|
c [worker] round 15, time: 7.471
|
||
|
|
c [worker] round 15, time: 7.554
|
||
|
|
c [worker] round 15, time: 7.576
|
||
|
|
c [worker] round 15, time: 7.592
|
||
|
|
c [worker] round 16, time: 7.624
|
||
|
|
c [worker] round 16, time: 7.895
|
||
|
|
c [worker] round 16, time: 7.890
|
||
|
|
c [worker] round 16, time: 7.942
|
||
|
|
c [worker] round 16, time: 7.975
|
||
|
|
c [worker] round 16, time: 8.59
|
||
|
|
c [worker] round 16, time: 8.80
|
||
|
|
c [worker] round 16, time: 8.97
|
||
|
|
c [worker] round 17, time: 8.125
|
||
|
|
c [worker] round 17, time: 8.398
|
||
|
|
c [worker] round 17, time: 8.394
|
||
|
|
c [worker] round 17, time: 8.446
|
||
|
|
c [worker] round 17, time: 8.479
|
||
|
|
c [worker] round 17, time: 8.566
|
||
|
|
c [worker] round 17, time: 8.588
|
||
|
|
c [worker] round 17, time: 8.603
|
||
|
|
c [worker] round 18, time: 8.627
|
||
|
|
c [worker] round 18, time: 8.900
|
||
|
|
c [worker] round 18, time: 8.897
|
||
|
|
c [worker] round 18, time: 8.952
|
||
|
|
c [worker] round 18, time: 8.982
|
||
|
|
c [worker] round 18, time: 9.71
|
||
|
|
c [worker] round 18, time: 9.96
|
||
|
|
c [worker] round 18, time: 9.108
|
||
|
|
c [worker] round 19, time: 9.132
|
||
|
|
c [worker] round 19, time: 9.403
|
||
|
|
c [worker] round 19, time: 9.406
|
||
|
|
c [worker] round 19, time: 9.456
|
||
|
|
c [worker] round 19, time: 9.485
|
||
|
|
c [worker] round 19, time: 9.578
|
||
|
|
c [worker] round 19, time: 9.603
|
||
|
|
c [worker] round 19, time: 9.615
|
||
|
|
c [worker] round 20, time: 9.636
|
||
|
|
c [worker] round 20, time: 9.911
|
||
|
|
c [worker] round 20, time: 9.909
|
||
|
|
c [worker] round 20, time: 9.960
|
||
|
|
c [worker] round 20, time: 9.991
|
||
|
|
c [worker] round 20, time: 10.86
|
||
|
|
c [worker] round 20, time: 10.108
|
||
|
|
c [worker] round 20, time: 10.120
|
||
|
|
c [worker] round 21, time: 10.140
|
||
|
|
c [worker] round 21, time: 10.415
|
||
|
|
c [worker] round 21, time: 10.412
|
||
|
|
c [worker] round 21, time: 10.464
|
||
|
|
c [worker] round 21, time: 10.495
|
||
|
|
c [worker] round 21, time: 10.591
|
||
|
|
c [worker] round 21, time: 10.616
|
||
|
|
c [worker] round 21, time: 10.627
|
||
|
|
c [worker] round 22, time: 10.644
|
||
|
|
c [worker] round 22, time: 10.919
|
||
|
|
c [worker] round 22, time: 10.926
|
||
|
|
c [worker] round 22, time: 10.972
|
||
|
|
c [worker] round 22, time: 10.998
|
||
|
|
c [worker] round 22, time: 11.98
|
||
|
|
c [worker] round 22, time: 11.120
|
||
|
|
c [worker] round 22, time: 11.131
|
||
|
|
c [worker] round 23, time: 11.145
|
||
|
|
c [worker] round 23, time: 11.421
|
||
|
|
c [worker] round 23, time: 11.430
|
||
|
|
c [worker] round 23, time: 11.476
|
||
|
|
c [worker] round 23, time: 11.502
|
||
|
|
c [worker] round 23, time: 11.602
|
||
|
|
c [worker] round 23, time: 11.628
|
||
|
|
c [worker] round 23, time: 11.635
|
||
|
|
c [worker] round 24, time: 11.648
|
||
|
|
c [worker] round 24, time: 11.923
|
||
|
|
c [worker] round 24, time: 11.984
|
||
|
|
c [worker] round 24, time: 11.994
|
||
|
|
c [worker] round 24, time: 12.7
|
||
|
|
c [worker] round 24, time: 12.106
|
||
|
|
c [worker] round 24, time: 12.139
|
||
|
|
c [worker] round 24, time: 12.183
|
||
|
|
c [worker] round 25, time: 12.152
|
||
|
|
c [worker] round 25, time: 12.426
|
||
|
|
c [worker] round 25, time: 12.488
|
||
|
|
c [worker] round 25, time: 12.498
|
||
|
|
c [worker] round 25, time: 12.511
|
||
|
|
c [worker] round 25, time: 12.614
|
||
|
|
c [worker] round 25, time: 12.647
|
||
|
|
c [worker] round 25, time: 12.688
|
||
|
|
c [worker] round 26, time: 12.656
|
||
|
|
c [worker] round 26, time: 12.931
|
||
|
|
c [worker] round 26, time: 12.992
|
||
|
|
c [worker] round 26, time: 13.42
|
||
|
|
c [worker] round 26, time: 13.19
|
||
|
|
c [worker] round 26, time: 13.122
|
||
|
|
c [worker] round 26, time: 13.155
|
||
|
|
c [worker] round 26, time: 13.200
|
||
|
|
c [worker] round 27, time: 13.157
|
||
|
|
c [worker] round 27, time: 13.433
|
||
|
|
c [worker] round 27, time: 13.496
|
||
|
|
c [worker] round 27, time: 13.546
|
||
|
|
c [worker] round 27, time: 13.626
|
||
|
|
c [worker] round 27, time: 13.560
|
||
|
|
c [worker] round 27, time: 13.659
|
||
|
|
c [worker] round 27, time: 13.703
|
||
|
|
c [worker] round 28, time: 13.659
|
||
|
|
c [worker] round 28, time: 13.939
|
||
|
|
c [worker] round 28, time: 13.999
|
||
|
|
c [worker] round 28, time: 14.49
|
||
|
|
c [worker] round 28, time: 14.130
|
||
|
|
c [worker] round 28, time: 14.63
|
||
|
|
c [worker] round 28, time: 14.163
|
||
|
|
c [worker] round 28, time: 14.208
|
||
|
|
c [worker] round 29, time: 14.164
|
||
|
|
c [worker] round 29, time: 14.448
|
||
|
|
c [worker] round 29, time: 14.504
|
||
|
|
c [worker] round 29, time: 14.554
|
||
|
|
c [worker] round 29, time: 14.634
|
||
|
|
c [worker] round 29, time: 14.566
|
||
|
|
c [worker] round 29, time: 14.667
|
||
|
|
c [worker] round 29, time: 14.712
|
||
|
|
c [worker] round 30, time: 14.668
|
||
|
|
c [worker] round 30, time: 14.950
|
||
|
|
c [worker] round 30, time: 15.14
|
||
|
|
c [worker] round 30, time: 15.58
|
||
|
|
c [worker] round 30, time: 15.137
|
||
|
|
c [worker] round 30, time: 15.104
|
||
|
|
c [worker] round 30, time: 15.171
|
||
|
|
c [worker] round 31, time: 15.172
|
||
|
|
c [worker] round 30, time: 15.225
|
||
|
|
c sharing nums: 30
|
||
|
|
c sharing time: 0.68
|
||
|
|
c [worker6] kissat exit with result: 10
|
||
|
|
c [worker6] getting send model signal
|
||
|
|
c [leader] received model size: 3616
|
||
|
|
c [worker] round 31, time: 15.452
|
||
|
|
c sharing nums: 31
|
||
|
|
c sharing time: 0.40
|
||
|
|
c [worker2] kissat exit with result: 0
|
||
|
|
c [worker] round 31, time: 15.520
|
||
|
|
c sharing nums: 31
|
||
|
|
c sharing time: 0.48
|
||
|
|
c [worker5] kissat exit with result: 0
|
||
|
|
c [worker] round 31, time: 15.562
|
||
|
|
c sharing nums: 31
|
||
|
|
c sharing time: 0.51
|
||
|
|
c [worker3] kissat exit with result: 0
|
||
|
|
c [worker] round 31, time: 15.641
|
||
|
|
c sharing nums: 31
|
||
|
|
c sharing time: 0.59
|
||
|
|
c [worker7] kissat exit with result: 0
|
||
|
|
c [worker] round 31, time: 15.607
|
||
|
|
c sharing nums: 31
|
||
|
|
c sharing time: 0.58
|
||
|
|
c [worker] round 31, time: 15.681
|
||
|
|
c [worker4] kissat exit with result: 0
|
||
|
|
c sharing nums: 31
|
||
|
|
c sharing time: 0.65
|
||
|
|
c [worker8] kissat exit with result: 0
|
||
|
|
c [worker] round 32, time: 15.675
|
||
|
|
c sharing nums: 32
|
||
|
|
c sharing time: 0.11
|
||
|
|
c [worker1] kissat exit with result: 0
|
||
|
|
s SATISFIABLE
|
||
|
|
v -1 2 3 4 -5 6 7 -8 9 -10 11 12 -13 14 15 -16 17 18 19 -20 -21 22 -23 24 25 26 27 28 29 -30 31 -32 -33 -34 35 36 37 38 39 40 -41 -42 -43 -44 45 46 47 -48 -49 50 -51 -52 53 54 -55 -56 57 58 -59 60 -61 -62 63 64 65 -66 -67 -68 -69 70 -71 72 73 74 -75 -76 -77 78 -79 80 -81 82 83 84 85 86 87 -88 89 90 91 92 -93 94 95 -96 97 -98 -99 -100 101 -102 103 -104 -105 -106 107 -108 -109 -110 -111 -112 113 114 -115 116 -117 -118 119 -120 -121 -122 -123 -124 125 -126 127 -128 -129 130 131 132 -133 134 -135 -136 137 -138 -139 -140 141 142 143 144 -145 -146 147 148 -149 -150 -151 -152 153 -154 155 156 -157 -158 -159 -160 161 -162 163 -164 165 -166 167 168 -169 170 -171 -172 -173 174 175 -176 177 178 -179 180 181 182 -183 -184 185 186 -187 188 -189 190 -191 192 -193 194 195 196 -197 -198 199 200 201 202 203 204 205 206 207 -208 -209 210 -211 -212 213 -214 215 216 217 -218 219 220 -221 222 223 224 225 -226 -227 228 -229 230 -231 -232 -233 234 235 -236 -237 -238 -239 240 241 -242 -243 244 -245 246 -247 -248 249 -250 251 -252 253 254 -255 -256 -257 -258 259 260 -261 -262 263 264 265 266 -267 -268 -269 270 -271 -272 273 274 275 -276 277 278 279 280 281 -282 -283 284 285 -286 287 -288 -289 -290 -291 -292 -293 -294 295 -296 -297 298 -299 300 -301 302 -303 -304 -305 306 -307 -308 309 -310 -311 312 -313 314 315 -316 317 -318 -319 320 -321 322 -323 -324 -325 326 -327 -328 -329 330 -331 332 333 334 335 -336 337 338 339 340 341 342 -343 -344 345 346 -347 -348 349 350 351 -352 353 354 355 -356 -357 358 359 360 -361 -362 -363 364 -365 366 -367 368 -369 370 -371 372 -373 -374 375 -376 377 378 379 380 -381 382 383 384 385 386 387 388 -389 -390 391 392 -393 -394 -395 -396 -397 -398 -399 -400 401 402 -403 404 405 -406 -407 408 409 -410 -411 -412 413 414 -415 416 -417 -418 419 420 421 -422 -423 -424 425 -426 -427 -428 -429 430 -431 432 433 -434 -435 436 437 -438 -439 440 -441 -442 443 -444 445 446 447 -448 -449 450 -451 -452 453 -454 455 456 457 -458 -459 -460 -461 462 463 -464 -465 466 467 468 469 470 471 -472 -473 474 475 -476 477 -478 479 480 -481 482 483 484 485 -486 487 488 -489 -490 -491 -492 -493 -494 -495 496 497 498 499 500 -501 -502 -503 504 -505 506 -507 508 -509 -510 -511 -512 513 514 515 516 517 -518 -519 -520 -521 -522 523 524 -525 -526 527 -528 529 530 531 -532 533 534 -535 536 537 -538 539 540 541 -542 -543 -544 545 546 547 548 549 550 -551 -552 553 554 555 556 557 558 -559 -560 561 -562 563 -564 565 -566 -567 568 569 570 -571 572 573 -574 575 576 577 578 -579 -580 581 582 583 -584 -585 -586 -587 588 -589 590 -591 592 -593 594 -595 -596 -597 -598 599 600 601 602 -603 604 605 -606 -607 -608 609 -610 611 612 613 -614 615 -616 -617 618 619 -620 621 -622 623 -624 -625 -626 627 -628 629 -630 631 -632 633 634 635 636 -637 638 -639 -640 -641 -642 -643 -644 645 -646 647 -648 -649 -650 -651 -652 653 654 655 656 657 658 659 660 -661 662 663 -664 -665 666 667 -668 -669 670 671 672 -673 674 675 -676 -677 -678 -679 -680 681 -682 683 -684 685 -686 -687 -688 -689 690 691 692 -693 -694 -695 -696 697 -698 699 700 701 -702 703 704 -705 706 -707 708 -709 710 711 -712 713 -714 -715 -716 717 -718 -719 720 721 722 -723 -724 725 726 727 728 -729 -730 731 732 733 734 -735 -736 737 -738 -739 -740 -741 -742 -743 -744 745 746 -747 -748 -749 750 -751 -752 753 -754 755 -756 -757 -758 759 -760 761 762 763 -764 -765 766 767 -768 769 -770 -771 772 -773 -774 -775 776 777 778 -779 780 -781 782 -783 784 785 -786 787 788 -789 -790 791 792 793 794 795 796 -797 798 799 800 -801 802 803 804 805 806 807 808 -809 -810 811 812 813 -814 815 816 -817 818 -819 820 821 822 -823 824 -825 -826 -827 828 829 -830 -831 832 -833 834 835 -836 837 838 839 -840 -841 -842 843 -844 845 -846 847 -848 -849 850 -851 -852 853 854 -855 -856 -857 -858 -859 -860 861 -862 -863 -864 -865 -866 -867 -868 869 870 871 872 873 -874 -875 -876 -877 878 879 880 -881 882 -883 -884 885 -886 887 888 889 890 -891 -892 -893 -894 895 896 -897 -898 -899 -900 -901 -902 903 904 -905 906 907 908 -909 910 911 912 -913 -914 915 916 917 918 919 -920 -921 -922 923 -924 925 -926 927 928 929 930 -931 932 933 934 935 -936 -937
|
||
|
|
|
||
|
|
real 16.93
|
||
|
|
user 2010.35
|
||
|
|
sys 17.03
|
||
|
|
mem 891484
|
||
|
|
|