375 lines
8.0 KiB
Plaintext
375 lines
8.0 KiB
Plaintext
c ------------------- Paras list -------------------
|
|
c Name Type Now Default Comment
|
|
c mode int 0 0 SAT=1, UNSAT=2
|
|
c reset int 0 0 Dynamically reseting
|
|
c reset_time int 10 10 Reseting base interval (seconds)
|
|
c share int 1 0 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 simplify int 1 1 Use Simplify (only preprocess)
|
|
c times double 5000.000000 5000 Cutoff time
|
|
c threads int 2 32 Thread number
|
|
c --------------------------------------------------
|
|
c filename: /pub/data/chenzh/data/sat2021/WS_500_16_70_10.apx_0.cnf
|
|
c After preprocess: vars: 1500 -> 998 , clauses: 11501 -> 9964 ,
|
|
c After preprocess: vars: 998 -> 498 , clauses: 9964 -> 8962 ,
|
|
c -----------------solve start----------------------
|
|
start sharing 500000
|
|
get 101 exported clauses
|
|
get 100 exported clauses
|
|
-106 67
|
|
-240 213
|
|
-480 67
|
|
-312 4
|
|
-148 16 -261
|
|
-488 83 130
|
|
-163 472 56
|
|
-103 -93 94
|
|
-240 352 213
|
|
-182 284 81
|
|
-265 431 443
|
|
-453 314 228
|
|
-396 168 343
|
|
-336 -261 177
|
|
-429 314 228
|
|
-299 148 91
|
|
-265 176 16
|
|
-299 148 91
|
|
-240 15 213
|
|
-41 83 253
|
|
-229 228 372
|
|
-381 359 130
|
|
-100 148 91
|
|
376 182 -5
|
|
-316 201 377
|
|
-293 385 86
|
|
-6 472 56
|
|
-182 284 81
|
|
261 56 4
|
|
-148 16 -261
|
|
-100 91 -261
|
|
-34 94 95
|
|
-182 81 284
|
|
-266 16 177
|
|
-67 270 15
|
|
9 -148 56
|
|
-41 83 253
|
|
-79 216 42
|
|
-40 143 56
|
|
-111 408 182
|
|
-182 284 81
|
|
-256 372 314
|
|
-391 65 310 249
|
|
101 96 -93 94
|
|
-103 96 -93 94
|
|
-34 95 96 94
|
|
-227 128 77 71
|
|
76 96 -93 94
|
|
-231 35 153 199
|
|
-377 382 34 47
|
|
-220 331 -11 467
|
|
-192 431 443 299
|
|
-154 -230 153 5
|
|
-293 385 86 118
|
|
-303 386 47 341
|
|
-378 168 345 343
|
|
-243 -409 319 397
|
|
-280 312 103 -241
|
|
-91 95 96 79
|
|
-432 339 178 402
|
|
-438 40 207 119
|
|
-304 158 34 394
|
|
-212 7 346 166
|
|
-480 79 96 95
|
|
-272 341 182 -302
|
|
-237 239 319 182
|
|
376 -302 182 341
|
|
-303 386 47 341
|
|
-239 386 47 341
|
|
-61 -401 120 65
|
|
-406 318 65 238 57
|
|
-360 423 -9 58 319
|
|
-79 216 137 -93 42
|
|
-167 372 482 174 479
|
|
-19 -93 58 319 423
|
|
-127 216 137 -93 42
|
|
-312 -93 58 319 423
|
|
-360 -261 16 412 388
|
|
-148 312 -261 49 320
|
|
-154 413 257 77 409
|
|
-5 237 281 400 178
|
|
-42 127 344 235 317
|
|
-163 465 39 325 56
|
|
-209 304 158 395 -166
|
|
-83 33 34 290 -236
|
|
241 395 435 98 343
|
|
-322 66 58 -93 319 423
|
|
-191 301 -425 171 365 159
|
|
-67 37 181 124 472 56
|
|
-322 352 213 5 -156 487
|
|
-255 169 5 409 -59 192
|
|
-489 78 278 110 327 48
|
|
-73 158 395 304 342 377
|
|
-243 435 319 136 22 397
|
|
-32 237 394 314 19 439 305
|
|
-111 69 240 46 220 237 238
|
|
-18 56 58 55 4 54 57 42
|
|
395 243 90 98 435 392 48 -376 231
|
|
-131 391 5 421 6 25 -9 388 221
|
|
-316 339 314 160 197 343 133 369 57 377 415
|
|
-480 67
|
|
-240 213
|
|
-106 67
|
|
-488 83 130
|
|
-488 83 130
|
|
-44 177 176
|
|
-67 15 270
|
|
-103 -93 94
|
|
-42 352 270
|
|
-163 472 56
|
|
-91 76 96
|
|
-316 201 377
|
|
-6 472 56
|
|
-148 -261 16
|
|
302 143 56
|
|
261 4 56
|
|
-299 91 148
|
|
-434 433 423
|
|
-100 91 148
|
|
-148 -261 16
|
|
-34 95 94
|
|
-396 168 343
|
|
-182 284 81
|
|
-61 284 81
|
|
-111 408 182
|
|
-488 130 83
|
|
-293 86 385
|
|
-148 4 16
|
|
-202 241 385
|
|
-40 56 143
|
|
-62 315 303
|
|
-231 -338 153
|
|
-41 253 83
|
|
261 4 56
|
|
-100 -261 91
|
|
-336 -261 177
|
|
-96 42 138
|
|
-229 228 372
|
|
-67 15 270
|
|
-111 182 408
|
|
-266 16 177
|
|
-42 270 352
|
|
-44 176 177
|
|
-256 314 372
|
|
-267 179 151
|
|
-138 96 94 95
|
|
-280 103 312 -241
|
|
-488 178 339 402
|
|
-328 372 310 208
|
|
-238 433 77 423
|
|
-237 56 207 406
|
|
-351 385 118 86
|
|
-237 182 319 239
|
|
-293 86 385 118
|
|
-446 213 183 115
|
|
241 385 123 118
|
|
230 386 -315 277
|
|
-244 215 64 334
|
|
-467 413 389 78
|
|
-127 -302 386 182
|
|
-338 -230 5 153
|
|
-377 382 34 47
|
|
-432 339 402 178
|
|
-141 129 303 389
|
|
425 182 341 47
|
|
-190 312 -241 103
|
|
-148 339 160 209
|
|
-356 124 208 372
|
|
-294 128 127 71
|
|
-73 158 -386 304
|
|
-402 77 413 409 157
|
|
-100 419 111 436 303
|
|
302 449 484 45 409
|
|
-441 463 330 90 19
|
|
53 423 -93 319 92
|
|
-112 303 419 111 436
|
|
-237 301 77 313 359
|
|
-401 238 120 65 318
|
|
4 -241 103 49 67
|
|
-111 -148 47 341 386
|
|
-343 327 16 -261 387
|
|
-402 413 77 157 409
|
|
-80 360 471 267 31
|
|
-57 160 197 339 314
|
|
-164 -182 160 209 178
|
|
-498 409 449 32 307
|
|
-37 354 113 99 80 135
|
|
-29 -261 75 37 472 124
|
|
-244 454 5 277 386 204
|
|
-343 327 16 387 209 -261
|
|
-57 51 331 316 8 354
|
|
-386 379 378 111 75 23
|
|
-83 33 34 290 8 -236
|
|
-138 113 102 96 91 131
|
|
156 321 463 331 135 146 -53
|
|
-70 91 89 88 86 92 90
|
|
-204 107 127 249 314 311 -236
|
|
-446 178 202 327 313 69 294
|
|
-489 -241 294 326 131 188 351
|
|
-490 -193 237 400 64 38 71 121
|
|
-369 293 244 -226 326 231 325 318 472 56 67
|
|
start sharing 500000
|
|
get 135 exported clauses
|
|
get 157 exported clauses
|
|
-381 -41
|
|
-103 -299
|
|
-265 16 176
|
|
376 -303 341
|
|
-103 217 148
|
|
-265 431 443
|
|
-41 83 253
|
|
-129 314 228
|
|
302 56 143
|
|
-148 4 16
|
|
-122 99 166 7
|
|
-102 95 -93 94
|
|
-401 -230 -212 449
|
|
-265 431 299 443
|
|
-41 151 325 253
|
|
-43 -127 148 150
|
|
-44 433 18 -233
|
|
-148 -280 312 -261
|
|
-131 42 216 302
|
|
-204 153 5 35
|
|
-382 95 -93 79
|
|
-282 47 386 182
|
|
-488 83 228 281
|
|
-29 207 333 42
|
|
-237 313 359 301
|
|
-48 -41 377 201
|
|
-112 127 121 -66
|
|
-83 185 90 -92
|
|
-388 423 415 449
|
|
-83 -166 11 80
|
|
-69 202 74 382
|
|
-293 494 485 466
|
|
-212 67 385 75
|
|
-433 160 178 339
|
|
-211 263 56 4
|
|
-237 406 207 56
|
|
1 67 377 51
|
|
-141 303 389 129
|
|
-91 96 95 79
|
|
-409 143 -235 395
|
|
-400 389 20 182
|
|
-227 338 -428 200
|
|
-111 176 177 408
|
|
302 231 -397 277
|
|
-397 -160 -237 -127
|
|
-477 123 118 180
|
|
1 67 377 51
|
|
-119 406 439 108
|
|
-359 476 147 433
|
|
-313 147 423 476
|
|
-106 96 -93 79
|
|
-294 71 128 127
|
|
-386 63 274 398 142
|
|
-11 445 267 360 471
|
|
-428 338 200 161 187
|
|
-77 102 111 121 64
|
|
-69 76 229 -93 202
|
|
-220 42 355 454 437
|
|
-269 -111 240 237 238
|
|
-290 325 112 297 39
|
|
-243 22 136 397 319
|
|
-255 395 343 98 90
|
|
-224 -93 96 94 42
|
|
-312 -431 157 470 441
|
|
-120 237 -193 178 400
|
|
-471 427 395 392 -376
|
|
302 201 34 144 382
|
|
-83 34 33 290 -236
|
|
-144 483 -412 163 -101
|
|
-194 -83 -92 103 320
|
|
-185 415 2 125 474
|
|
-142 332 240 58 38
|
|
-190 136 16 111 303
|
|
-5 237 281 400 178
|
|
-91 138 34 216 42
|
|
-112 127 274 121 106
|
|
-117 363 122 24 461
|
|
-92 -305 -407 424 313
|
|
-488 494 163 244 83
|
|
376 -186 111 163 323
|
|
-392 338 200 372 161
|
|
-136 257 157 24 413
|
|
-250 233 234 235 232
|
|
-229 359 65 228 77
|
|
-195 400 237 281 178
|
|
-122 54 323 265 305
|
|
-130 313 65 77 228
|
|
-350 387 17 458 400
|
|
-83 -236 34 290 33
|
|
-356 343 351 152 456
|
|
-92 471 164 31 445
|
|
-264 -230 58 451 50 47
|
|
-43 150 95 96 -93 148
|
|
-90 65 120 318 314 281
|
|
-69 34 290 331 8 467
|
|
-19 190 467 -61 395 197
|
|
-320 420 -271 350 426 233
|
|
-47 246 115 24 381 301
|
|
-343 123 -399 49 408 116
|
|
-311 346 379 395 316 373
|
|
-247 454 277 386 199 153
|
|
-280 215 374 38 240 58
|
|
-361 34 290 -236 467 33
|
|
-171 6 369 352 166 213
|
|
399 152 61 248 274 322
|
|
-387 301 171 365 -425 368
|
|
-305 -407 330 375 424 313
|
|
-475 188 15 195 39 169
|
|
-243 331 8 451 316 354
|
|
-48 230 277 454 201 8
|
|
-96 111 71 121 64 138
|
|
-269 -97 100 55 99 98
|
|
-111 238 69 220 240 237
|
|
-320 304 115 246 301 24
|
|
76 476 253 130 147 433
|
|
-95 472 -261 144 37 181
|
|
193 147 339 221 -359 448
|
|
412 -177 387 449 423 327
|
|
-269 30 484 320 47 130 83
|
|
-373 27 495 54 223 161 122
|
|
-5 214 221 24 329 127 470
|
|
-130 281 228 343 435 243 395
|
|
-176 165 162 205 443 303 197
|
|
-345 290 227 388 18 122 433
|
|
-496 227 47 138 -76 127 266
|
|
-67 275 39 377 327 215 496
|
|
-35 402 160 209 78 48 -489
|
|
207 356 40 340 439 108 406
|
|
-384 -221 67 -93 128 303 423
|
|
-297 99 100 -88 55 340 40
|
|
-24 189 -1 -226 227 229 228
|
|
-325 -341 131 64 221 69 312
|
|
-220 340 119 356 415 326 125
|
|
-132 -53 68 38 312 18 484
|
|
-237 359 301 228 147 423 476
|
|
-103 67 100 -341 163 -85 -487
|
|
-103 -93 -341 163 -85 -487 100
|
|
302 138 127 227 -185 415 125 -76
|
|
-163 465 -177 490 290 197 34 -83
|
|
-352 258 237 100 177 58 489 164
|
|
-22 487 -156 391 65 431 465 299
|
|
-319 303 206 136 158 16 -497 130
|
|
-31 377 483 -123 -101 275 -412 163
|
|
-293 -140 180 166 123 7 163 99
|
|
-103 443 144 335 205 60 433 -359
|
|
-486 451 90 19 330 267 406 359 253
|
|
-233 -1 207 208 7 -24 127 346 11
|
|
-90 -202 16 -261 209 322 323 -302 324
|
|
-281 462 439 490 37 418 356 421 391 -156
|
|
405 280 269 -308 161 235 -108 294 167 478
|
|
301 115 304 24 246 385 17 75 -241 103 49
|