minisat+ conversion to SAT
311 views
Skip to first unread message
lesshaste
Jun 12, 2011, 5:09:34 PM6/12/11
to MiniSat
I am trying to use minisat+ to convert a PB problem to SAT. The
problem I am having is that the default setting is very slow but if I
use
"-ca -adders Convert PB-constrs to clauses through adders."
the conversion certainly runs fast but appears to give a CNF which is
incorrect. To be precise I am doing
minisat+ -ca -cnf=test.cnf file.pbo
When I do that and then put test.cnf through a standard SAT solver it
says it is SATISFIABLE. However
minisat+ file.pbo
says it is UNSATISFIABLE (which I happen to know is correct).
Does anyone know/remember if the -ca option is supposed to output an
equivalent CNF file or does it do something else? Are there any other
tools to convert from PB to SAT that run reasonably fast?
Raphael
P.S. The example file.pbo is below.
* #variable= 39 #constraint= 4
min: 1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1
x11 +1 x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1
x21 +1 x22 +1 x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 ;
1 x1 +1048545 x2 +378 x3 +1045297 x4 +20475 x5 +950293 x6 +376740 x7
+913106 x8 +1010959 x9 +433111 x10 +540234 x11 +545853 x12 +13138 x13
+306468 x14 +270826 x15 +306468 x16 +13138 x17 +545853 x18 +540234 x19
+433111 x20 +1010959 x21 +913106 x22 +376740 x23 +950293 x24 +20475
x25 +1045297 x26 +378 x27 +1048545 x28 +1 x29 -1048573 x30 -2097146
x31 -4194292 x32 -8388584 x33 -16777168 x34 = 0;
1 x1 +1048543 x2 +378 x3 +1045295 x4 +20475 x5 +950291 x6 +376740 x7
+913102 x8 +1010963 x9 +433097 x10 +540258 x11 +545811 x12 +13196 x13
+306396 x14 +270902 x15 +306396 x16 +13196 x17 +545811 x18 +540258 x19
+433097 x20 +1010963 x21 +913102 x22 +376740 x23 +950291 x24 +20475
x25 +1045295 x26 +378 x27 +1048543 x28 +1 x29 -1048571 x35 -2097142
x36 -4194284 x37 -8388568 x38 -16777136 x39 = 0;
1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1
x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1
x22 +1 x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 >= 1;
1 x1 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1 x12 +1
x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1
x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 <= 27 ;
problem I am having is that the default setting is very slow but if I
use
"-ca -adders Convert PB-constrs to clauses through adders."
the conversion certainly runs fast but appears to give a CNF which is
incorrect. To be precise I am doing
minisat+ -ca -cnf=test.cnf file.pbo
When I do that and then put test.cnf through a standard SAT solver it
says it is SATISFIABLE. However
minisat+ file.pbo
says it is UNSATISFIABLE (which I happen to know is correct).
Does anyone know/remember if the -ca option is supposed to output an
equivalent CNF file or does it do something else? Are there any other
tools to convert from PB to SAT that run reasonably fast?
Raphael
P.S. The example file.pbo is below.
* #variable= 39 #constraint= 4
min: 1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1
x11 +1 x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1
x21 +1 x22 +1 x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 ;
1 x1 +1048545 x2 +378 x3 +1045297 x4 +20475 x5 +950293 x6 +376740 x7
+913106 x8 +1010959 x9 +433111 x10 +540234 x11 +545853 x12 +13138 x13
+306468 x14 +270826 x15 +306468 x16 +13138 x17 +545853 x18 +540234 x19
+433111 x20 +1010959 x21 +913106 x22 +376740 x23 +950293 x24 +20475
x25 +1045297 x26 +378 x27 +1048545 x28 +1 x29 -1048573 x30 -2097146
x31 -4194292 x32 -8388584 x33 -16777168 x34 = 0;
1 x1 +1048543 x2 +378 x3 +1045295 x4 +20475 x5 +950291 x6 +376740 x7
+913102 x8 +1010963 x9 +433097 x10 +540258 x11 +545811 x12 +13196 x13
+306396 x14 +270902 x15 +306396 x16 +13196 x17 +545811 x18 +540258 x19
+433097 x20 +1010963 x21 +913102 x22 +376740 x23 +950291 x24 +20475
x25 +1045295 x26 +378 x27 +1048543 x28 +1 x29 -1048571 x35 -2097142
x36 -4194284 x37 -8388568 x38 -16777136 x39 = 0;
1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1
x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1
x22 +1 x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 >= 1;
1 x1 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1 x12 +1
x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1
x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 <= 27 ;
Niklas Sörensson
Jun 14, 2011, 6:16:05 AM6/14/11
to min...@googlegroups.com
Hello Raphael,
On Sun, Jun 12, 2011 at 11:09 PM, lesshaste <drr...@gmail.com> wrote:
> I am trying to use minisat+ to convert a PB problem to SAT. The
> problem I am having is that the default setting is very slow but if I
> use
>
> "-ca -adders Convert PB-constrs to clauses through adders."
>
> the conversion certainly runs fast but appears to give a CNF which is
> incorrect. To be precise I am doing
>
> minisat+ -ca -cnf=test.cnf file.pbo
>
> When I do that and then put test.cnf through a standard SAT solver it
> says it is SATISFIABLE. However
>
> minisat+ file.pbo
>
> says it is UNSATISFIABLE (which I happen to know is correct).
>
> Does anyone know/remember if the -ca option is supposed to output an
> equivalent CNF file or does it do something else? Are there any other
> tools to convert from PB to SAT that run reasonably fast?
Ok, two comments.
First, the CNF-generation of MiniSat+ is know to be buggy (this
feature was never tested much by us). I have started porting MiniSat+
to a newer MiniSat backend, and I *think* that might solve this
problem. If you'd like to try it out, you can download the source here
(choose the "next" branch!):
https://github.com/niklasso/minisatp
You'll need to also download the source to MiniSat separately:
https://github.com/niklasso/minisat
Secondly, and maybe more importantly, even though generating
constraints via adders produces smaller CNFs, the performance is
usually very very bad. The adder method is really a last resort, that
sometimes works even if performance is bad. For instance, when I tried
to repeat your issue with the problem you posted, MiniSat simply
didn't terminate within 15 minutes.
Is it possible to send an example of the real OPB-problem that you'd
like to solve? Then I can take a look myself and maybe come up with
some recommendation.
Regards,
/Niklas
lesshaste
Jun 14, 2011, 7:39:48 AM6/14/11
to MiniSat
Hi,
> Ok, two comments.
>
> First, the CNF-generation of MiniSat+ is know to be buggy (this
> feature was never tested much by us). I have started porting MiniSat+
> to a newer MiniSat backend, and I *think* that might solve this
> problem. If you'd like to try it out, you can download the source here
> (choose the "next" branch!):
>
> https://github.com/niklasso/minisatp
>
> You'll need to also download the source to MiniSat separately:
>
> https://github.com/niklasso/minisat
>
Thanks! The addition of bignum support is a huge help and means I
don't have to split the equality constraint up any more using the
Chinese Remainder Theorem and converting the added integer variable to
binary ones. The upshot is that I now have only 3 constraints but with
big coefficients in one of them.
> Secondly, and maybe more importantly, even though generating
> constraints via adders produces smaller CNFs, the performance is
> usually very very bad. The adder method is really a last resort, that
> sometimes works even if performance is bad. For instance, when I tried
> to repeat your issue with the problem you posted, MiniSat simply
> didn't terminate within 15 minutes.
>
> Is it possible to send an example of the real OPB-problem that you'd
> like to solve? Then I can take a look myself and maybe come up with
> some recommendation.
>
Sure. Here is the original formulation for one large problem with
large coefficients.
* #variable= 141 #constraint= 3
1 x1 -140 x2 +9730 x3 -447580 x4 +15329615 x5 -416965528 x6
+9381724380 x7 -179593009560 x8 +2985733783935 x9 -43790762164384 x10
+573658984353452 x11 -6779606178722296 x12 +72880766421268000 x13
-717595238609422720 x14 +6509613950242167808 x15 -54680757182033354752
x16 +427193415484620800000 x17 -3115999030593960017920 x18
+21292660042393605636096 x19 -136721290798510278443008 x20
+827163809331026101010432 x21 -4726650339034364762914816 x22
+25566881379322088459862016 x23 -131169217511304783116369920 x24
+639449935367587246911782912 x25 -2967047700105727773060890624 x26
+13123480212006120928923615232 x27 -55410249784025115801088425984 x28
+223619936628378720393616162816 x29 -863635617323493296638223450112
x30 +3195451784096823542873587712000 x31
-11338699879052724554836423475200 x32
+38622446463022766483790519861248 x33
-126400733878982331842910215995392 x34
+397790544854461169205182669520896 x35
-1204737078702064618467635754958848 x36
+3513816479547775263902622969495552 x37
-9876673347917898790505860183359488 x38
+26770983021988185096613602646818816 x39
-70016417134435466734995794122768384 x40
+176791453264437922141973003523588096 x41
-431198666498598912119527957910781952 x42
+1016396856746722048937408536105713664 x43
-2316439347934321778381895802571194368 x44
+5106695835219179517446766187878809600 x45
-10894284448468144145103482210314354688 x46
+22499065708791367665104398223969091584 x47
-44998131417582810888072522362261602304 x48
+87183879621565055663583525233875746816 x49
-163692182146615402644169042197838036992 x50
+297919771506855169697017187846047399936 x51
-525740773247383822368775271230382014464 x52
+899825554211802918761313906622587731968 x53
-1494049976804446989608787629933024247808 x54
+2407080518185190017243511961637896585216 x55
-3763798628435065636949864282772826226688 x56
+5712908632445624127183722384139564875776 x57
-8419023247815115797917747728052060684288 x58
+12047912578769003980849324116817920131072 x59
-16744556465408542325919626763390364418048 x60
+22605151228300904344813370253646567047168 x61
-29646099971544074661812364867319915085824 x62
+37774869318581156314836050191366469189632 x63
-46768885823003336805696402525829948506112 x64
+56268815755800470399325532916222827429888 x65
-65791230729861077356267334426532736139264 x66
+74762762193024615351390195699261311549440 x67
-82573797049006459320500090861997787185152 x68
+88645399773199578661523243729816700059648 x69
-92499547589427908726131345622661450432512 x70
+93820969697847617436442575650631073136640 x71
-92499547589425278103547864189577289793536 x72
+88645399773199578661523243729816700059648 x73
-82573797049006459320500090861997787185152 x74
+74762762193028870770275239193956277288960 x75
-65791230729861077356267334426532736139264 x76
+56268815755802066181407424226733439582208 x77
-46768885823004661788394700159405426475008 x78
+37774869318581156314836050191366469189632 x79
-29646099971544920909886095107742209409024 x80
+22605151228301547493349405236367510732800 x81
-16744556465408542325919626763390364418048 x82
+12047912578769347315782094671503536685056 x83
-8419023247815115797917747728052060684288 x84
+5712908632445624127183722384139564875776 x85
-3763798628435172626884900177454787723264 x86
+2407080518185190017243511961637896585216 x87
-1494049976804446989608787629933024247808 x88
+899825554211777380203374547581272064000 x89
-525740773247398707267929276352095584256 x90
+297919771506863632177754490250270343168 x91
-163692182146615402644169042197838036992 x92
+87183879621567530183620548927967723520 x93
-44998131417582810888072522362261602304 x94
+22499065708791367665104398223969091584 x95
-10894284448467834830098854248552857600 x96
+5106695835219179517446766187878809600 x97
-2316439347934255960399040806891028480 x98
+1016396856746693124442700959528779776 x99
-431198666498605036438560429481918464 x100
+176791453264435376491290831605465088 x101
-70016417134436462859175774438555648 x102
+26770983021987802326674073173622784 x103
-9876673347918039446929422218690560 x104
+3513816479547775263902622969495552 x105
-1204737078702064618467635754958848 x106
+397790544854472482247446624206848 x107
-126400733878980548417457777278976 x108
+38622446463022766483790519861248 x109
-11338699879052724554836423475200 x110
+3195451784096869141819814838272 x111 -863635617323493296638223450112
x112 +223619936628378720393616162816 x113
-55410249784023541300437450752 x114 +13123480212006494762877059072
x115 -2967047700105727773060890624 x116 +639449935367605526292594688
x117 -131169217511301982797692928 x118 +25566881379321542999015424
x119 -4726650339034431871778816 x120 +827163809331014424068096 x121
-136721290798515143835648 x122 +21292660042393907625984 x123
-3115999030593804828672 x124 +427193415484626894848 x125
-54680757182034526208 x126 +6509613950242259968 x127
-717595238609453312 x128 +72880766421269040 x129 -6779606178722007
x130 +573658984353473 x131 -43790762164386 x132 +2985733783935 x133
-179593009560 x134 +9381724380 x135 -416965528 x136 +15329615 x137
-447580 x138 +9730 x139 -140 x140 +1 x141 = 0;
x32 +1 x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1
x42 +1 x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 +1 x51 +1
x52 +1 x53 +1 x54 +1 x55 +1 x56 +1 x57 +1 x58 +1 x59 +1 x60 +1 x61 +1
x62 +1 x63 +1 x64 +1 x65 +1 x66 +1 x67 +1 x68 +1 x69 +1 x70 +1 x71 +1
x72 +1 x73 +1 x74 +1 x75 +1 x76 +1 x77 +1 x78 +1 x79 +1 x80 +1 x81 +1
x82 +1 x83 +1 x84 +1 x85 +1 x86 +1 x87 +1 x88 +1 x89 +1 x90 +1 x91 +1
x92 +1 x93 +1 x94 +1 x95 +1 x96 +1 x97 +1 x98 +1 x99 +1 x100 +1 x101
+1 x102 +1 x103 +1 x104 +1 x105 +1 x106 +1 x107 +1 x108 +1 x109 +1
x110 +1 x111 +1 x112 +1 x113 +1 x114 +1 x115 +1 x116 +1 x117 +1 x118
+1 x119 +1 x120 +1 x121 +1 x122 +1 x123 +1 x124 +1 x125 +1 x126 +1
x127 +1 x128 +1 x129 +1 x130 +1 x131 +1 x132 +1 x133 +1 x134 +1 x135
+1 x136 +1 x137 +1 x138 +1 x139 +1 x140 +1 x141 >= 1;
x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1 x42 +1
x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 +1 x51 +1 x52 +1
x53 +1 x54 +1 x55 +1 x56 +1 x57 +1 x58 +1 x59 +1 x60 +1 x61 +1 x62 +1
x63 +1 x64 +1 x65 +1 x66 +1 x67 +1 x68 +1 x69 +1 x70 +1 x71 +1 x72 +1
x73 +1 x74 +1 x75 +1 x76 +1 x77 +1 x78 +1 x79 +1 x80 +1 x81 +1 x82 +1
x83 +1 x84 +1 x85 +1 x86 +1 x87 +1 x88 +1 x89 +1 x90 +1 x91 +1 x92 +1
x93 +1 x94 +1 x95 +1 x96 +1 x97 +1 x98 +1 x99 +1 x100 +1 x101 +1 x102
+1 x103 +1 x104 +1 x105 +1 x106 +1 x107 +1 x108 +1 x109 +1 x110 +1
x111 +1 x112 +1 x113 +1 x114 +1 x115 +1 x116 +1 x117 +1 x118 +1 x119
+1 x120 +1 x121 +1 x122 +1 x123 +1 x124 +1 x125 +1 x126 +1 x127 +1
x128 +1 x129 +1 x130 +1 x131 +1 x132 +1 x133 +1 x134 +1 x135 +1 x136
+1 x137 +1 x138 +1 x139 +1 x140 +1 x141 <= 139 ;
and after conversion to reduce the size of the coefficients
* #variable= 261 #constraint= 17
1 x1 +881 x2 +541 x3 +639 x4 +321 x5 +662 x6 +420 x7 +128 x8 +935 x9
+917 x10 +363 x11 +391 x12 +391 x13 +515 x14 +812 x15 +176 x16 +747
x17 +1008 x18 +1017 x19 +119 x20 +1018 x21 +613 x22 +247 x23 +952 x24
+961 x25 +22 x26 +20 x27 +577 x28 +850 x29 +852 x30 +956 x31 +803 x32
+1001 x33 +661 x34 +209 x35 +144 x36 +698 x37 +199 x38 +76 x39 +493
x40 +190 x41 +300 x42 +757 x43 +169 x44 +484 x45 +357 x46 +605 x47
+741 x48 +202 x49 +833 x50 +455 x51 +427 x52 +377 x53 +803 x54 +23 x55
+911 x56 +807 x57 +360 x58 +83 x59 +656 x60 +1004 x61 +141 x62 +961
x63 +66 x64 +990 x65 +923 x66 +516 x67 +716 x68 +888 x69 +161 x70 +848
x71 +254 x72 +888 x73 +716 x74 +216 x75 +923 x76 +367 x77 +113 x78
+961 x79 +920 x80 +657 x81 +656 x82 +82 x83 +360 x84 +807 x85 +701 x86
+23 x87 +803 x88 +249 x89 +878 x90 +437 x91 +833 x92 +885 x93 +741 x94
+605 x95 +570 x96 +484 x97 +340 x98 +778 x99 +505 x100 +675 x101 +594
x102 +25 x103 +88 x104 +698 x105 +144 x106 +662 x107 +656 x108 +1001
x109 +803 x110 +77 x111 +852 x112 +850 x113 +175 x114 +1014 x115 +22
x116 +138 x117 +919 x118 +825 x119 +457 x120 +852 x121 +220 x122 +546
x123 +298 x124 +225 x125 +828 x126 +61 x127 +553 x128 +410 x129 +680
x130 +384 x131 +915 x132 +935 x133 +128 x134 +420 x135 +662 x136 +321
x137 +639 x138 +541 x139 +881 x140 +1 x141 -1021 x142 -2042 x143 -4084
x144 -8168 x145 -16336 x146 -32672 x147 -65344 x148 -130688 x149 = 0;
1 x1 +879 x2 +559 x3 +780 x4 +798 x5 +101 x6 +275 x7 +413 x8 +649 x9
+1007 x10 +994 x11 +614 x12 +284 x13 +277 x14 +618 x15 +817 x16 +848
x17 +314 x18 +311 x19 +25 x20 +144 x21 +496 x22 +172 x23 +303 x24 +91
x25 +470 x26 +142 x27 +934 x28 +315 x29 +304 x30 +531 x31 +86 x32 +106
x33 +988 x34 +741 x35 +932 x36 +247 x37 +246 x38 +257 x39 +22 x40 +233
x41 +805 x42 +245 x43 +920 x44 +757 x45 +831 x46 +446 x47 +360 x48
+723 x49 +889 x50 +886 x51 +250 x52 +16 x53 +473 x54 +327 x55 +140 x56
+812 x57 +996 x58 +314 x59 +572 x60 +301 x61 +450 x62 +284 x63 +143
x64 +818 x65 +747 x66 +6 x67 +949 x68 +793 x69 +405 x70 +389 x71 +536
x72 +793 x73 +949 x74 +128 x75 +747 x76 +609 x77 +860 x78 +284 x79
+391 x80 +998 x81 +572 x82 +303 x83 +996 x84 +812 x85 +931 x86 +327
x87 +473 x88 +307 x89 +296 x90 +265 x91 +889 x92 +480 x93 +360 x94
+446 x95 +928 x96 +757 x97 +928 x98 +374 x99 +393 x100 +516 x101 +753
x102 +486 x103 +545 x104 +247 x105 +932 x106 +256 x107 +686 x108 +106
x109 +86 x110 +228 x111 +304 x112 +315 x113 +233 x114 +690 x115 +470
x116 +419 x117 +223 x118 +869 x119 +326 x120 +950 x121 +191 x122 +378
x123 +957 x124 +38 x125 +192 x126 +49 x127 +255 x128 +305 x129 +903
x130 +1015 x131 +1005 x132 +649 x133 +413 x134 +275 x135 +101 x136
+798 x137 +780 x138 +559 x139 +879 x140 +1 x141 -1019 x150 -2038 x151
-4076 x152 -8152 x153 -16304 x154 -32608 x155 -65216 x156 -130432
x157 = 0;
1 x1 +873 x2 +613 x3 +166 x4 +899 x5 +467 x6 +129 x7 +859 x8 +281 x9
+602 x10 +442 x11 +252 x12 +609 x13 +245 x14 +251 x15 +186 x16 +928
x17 +232 x18 +581 x19 +805 x20 +362 x21 +603 x22 +479 x23 +858 x24
+476 x25 +702 x26 +832 x27 +374 x28 +866 x29 +656 x30 +233 x31 +864
x32 +185 x33 +168 x34 +17 x35 +447 x36 +895 x37 +735 x38 +702 x39 +24
x40 +757 x41 +966 x42 +341 x43 +49 x44 +599 x45 +244 x46 +936 x47 +472
x48 +149 x49 +468 x50 +608 x51 +800 x52 +752 x53 +673 x54 +437 x55
+700 x56 +101 x57 +365 x58 +434 x59 +972 x60 +603 x61 +363 x62 +319
x63 +132 x64 +29 x65 +868 x66 +14 x67 +418 x68 +256 x69 +343 x70 +464
x71 +945 x72 +256 x73 +418 x74 +94 x75 +868 x76 +59 x77 +15 x78 +319
x79 +255 x80 +523 x81 +972 x82 +993 x83 +365 x84 +101 x85 +203 x86
+437 x87 +673 x88 +858 x89 +640 x90 +447 x91 +468 x92 +371 x93 +472
x94 +936 x95 +525 x96 +599 x97 +508 x98 +162 x99 +879 x100 +373 x101
+138 x102 +380 x103 +934 x104 +895 x105 +447 x106 +316 x107 +149 x108
+185 x109 +864 x110 +598 x111 +656 x112 +866 x113 +225 x114 +890 x115
+702 x116 +636 x117 +555 x118 +2 x119 +988 x120 +196 x121 +567 x122
+987 x123 +919 x124 +555 x125 +771 x126 +228 x127 +43 x128 +636 x129
+541 x130 +463 x131 +600 x132 +281 x133 +859 x134 +129 x135 +467 x136
+899 x137 +166 x138 +613 x139 +873 x140 +1 x141 -1013 x158 -2026 x159
-4052 x160 -8104 x161 -16208 x162 -32416 x163 -64832 x164 -129664
x165 = 0;
1 x1 +869 x2 +649 x3 +416 x4 +887 x5 +695 x6 +2 x7 +250 x8 +132 x9 +78
x10 +816 x11 +398 x12 +553 x13 +636 x14 +745 x15 +210 x16 +876 x17
+662 x18 +612 x19 +39 x20 +395 x21 +1003 x22 +326 x23 +573 x24 +455
x25 +821 x26 +619 x27 +940 x28 +22 x29 +525 x30 +375 x31 +613 x32 +353
x33 +591 x34 +459 x35 +998 x36 +998 x37 +589 x38 +126 x39 +672 x40
+153 x41 +532 x42 +846 x43 +366 x44 +715 x45 +230 x46 +777 x47 +631
x48 +598 x49 +345 x50 +429 x51 +14 x52 +872 x53 +914 x54 +408 x55
+1000 x56 +689 x57 +623 x58 +409 x59 +619 x60 +822 x61 +797 x62 +910
x63 +250 x64 +237 x65 +253 x66 +499 x67 +205 x68 +124 x69 +911 x70
+410 x71 +497 x72 +124 x73 +205 x74 +957 x75 +253 x76 +661 x77 +644
x78 +910 x79 +511 x80 +999 x81 +619 x82 +329 x83 +623 x84 +689 x85
+357 x86 +408 x87 +914 x88 +814 x89 +625 x90 +896 x91 +345 x92 +426
x93 +631 x94 +777 x95 +713 x96 +715 x97 +256 x98 +98 x99 +178 x100
+638 x101 +116 x102 +230 x103 +688 x104 +998 x105 +998 x106 +190 x107
+502 x108 +353 x109 +613 x110 +238 x111 +525 x112 +22 x113 +299 x114
+588 x115 +821 x116 +968 x117 +57 x118 +117 x119 +442 x120 +142 x121
+354 x122 +836 x123 +665 x124 +355 x125 +203 x126 +77 x127 +314 x128
+584 x129 +687 x130 +837 x131 +76 x132 +132 x133 +250 x134 +2 x135
+695 x136 +887 x137 +416 x138 +649 x139 +869 x140 +1 x141 -1009 x166
-2018 x167 -4036 x168 -8072 x169 -16144 x170 -32288 x171 -64576 x172
-129152 x173 = 0;
1 x1 +857 x2 +757 x3 +73 x4 +740 x5 +809 x6 +242 x7 +210 x8 +746 x9
+354 x10 +768 x11 +759 x12 +393 x13 +967 x14 +472 x15 +230 x16 +87 x17
+706 x18 +960 x19 +305 x20 +424 x21 +169 x22 +935 x23 +9 x24 +968 x25
+567 x26 +768 x27 +426 x28 +511 x29 +107 x30 +996 x31 +954 x32 +859
x33 +811 x34 +947 x35 +763 x36 +739 x37 +59 x38 +172 x39 +461 x40 +374
x41 +620 x42 +924 x43 +139 x44 +409 x45 +520 x46 +436 x47 +25 x48 +678
x49 +779 x50 +909 x51 +432 x52 +400 x53 +762 x54 +952 x55 +135 x56
+410 x57 +596 x58 +842 x59 +525 x60 +657 x61 +590 x62 +488 x63 +880
x64 +218 x65 +114 x66 +784 x67 +783 x68 +469 x69 +441 x70 +371 x71
+517 x72 +469 x73 +783 x74 +731 x75 +114 x76 +572 x77 +6 x78 +488 x79
+221 x80 +419 x81 +525 x82 +610 x83 +596 x84 +410 x85 +109 x86 +952
x87 +762 x88 +498 x89 +672 x90 +145 x91 +779 x92 +962 x93 +25 x94 +436
x95 +57 x96 +409 x97 +304 x98 +543 x99 +608 x100 +357 x101 +411 x102
+919 x103 +832 x104 +739 x105 +763 x106 +442 x107 +679 x108 +859 x109
+954 x110 +868 x111 +107 x112 +511 x113 +877 x114 +410 x115 +567 x116
+636 x117 +734 x118 +884 x119 +778 x120 +851 x121 +566 x122 +545 x123
+922 x124 +274 x125 +249 x126 +908 x127 +285 x128 +436 x129 +51 x130
+789 x131 +352 x132 +746 x133 +210 x134 +242 x135 +809 x136 +740 x137
+73 x138 +757 x139 +857 x140 +1 x141 -997 x174 -1994 x175 -3988 x176
-7976 x177 -15952 x178 -31904 x179 -63808 x180 -127616 x181 = 0;
1 x1 +851 x2 +811 x3 +352 x4 +827 x5 +695 x6 +714 x7 +206 x8 +787 x9
+15 x10 +717 x11 +854 x12 +579 x13 +695 x14 +868 x15 +239 x16 +658 x17
+948 x18 +382 x19 +19 x20 +692 x21 +627 x22 +985 x23 +311 x24 +832 x25
+785 x26 +170 x27 +568 x28 +358 x29 +916 x30 +355 x31 +193 x32 +815
x33 +816 x34 +726 x35 +802 x36 +639 x37 +81 x38 +11 x39 +822 x40 +647
x41 +72 x42 +160 x43 +57 x44 +451 x45 +896 x46 +134 x47 +569 x48 +91
x49 +773 x50 +676 x51 +66 x52 +725 x53 +422 x54 +966 x55 +315 x56 +164
x57 +258 x58 +250 x59 +671 x60 +456 x61 +108 x62 +836 x63 +681 x64
+192 x65 +280 x66 +107 x67 +256 x68 +180 x69 +592 x70 +26 x71 +946 x72
+180 x73 +256 x74 +155 x75 +280 x76 +210 x77 +612 x78 +836 x79 +639
x80 +211 x81 +671 x82 +380 x83 +258 x84 +164 x85 +271 x86 +966 x87
+422 x88 +205 x89 +449 x90 +86 x91 +773 x92 +675 x93 +569 x94 +134 x95
+969 x96 +451 x97 +586 x98 +643 x99 +15 x100 +486 x101 +759 x102 +441
x103 +836 x104 +639 x105 +802 x106 +548 x107 +324 x108 +815 x109 +193
x110 +669 x111 +916 x112 +358 x113 +398 x114 +185 x115 +785 x116 +452
x117 +182 x118 +200 x119 +666 x120 +455 x121 +168 x122 +858 x123 +587
x124 +856 x125 +145 x126 +865 x127 +824 x128 +628 x129 +152 x130 +738
x131 +13 x132 +787 x133 +206 x134 +714 x135 +695 x136 +827 x137 +352
x138 +811 x139 +851 x140 +1 x141 -991 x182 -1982 x183 -3964 x184 -7928
x185 -15856 x186 -31712 x187 -63424 x188 -126848 x189 = 0;
1 x1 +843 x2 +883 x3 +668 x4 +713 x5 +463 x6 +887 x7 +293 x8 +904 x9
+827 x10 +689 x11 +576 x12 +75 x13 +572 x14 +449 x15 +572 x16 +29 x17
+500 x18 +272 x19 +408 x20 +971 x21 +13 x22 +826 x23 +515 x24 +9 x25
+515 x26 +269 x27 +944 x28 +194 x29 +229 x30 +434 x31 +29 x32 +295 x33
+726 x34 +92 x35 +733 x36 +512 x37 +895 x38 +134 x39 +742 x40 +817 x41
+914 x42 +769 x43 +19 x44 +452 x45 +57 x46 +931 x47 +670 x48 +807 x49
+832 x50 +58 x51 +620 x52 +183 x53 +374 x54 +205 x55 +653 x56 +294 x57
+512 x58 +253 x59 +184 x60 +57 x61 +366 x62 +847 x63 +155 x64 +172 x65
+835 x66 +866 x67 +383 x68 +136 x69 +778 x70 +817 x71 +140 x72 +136
x73 +383 x74 +470 x75 +835 x76 +515 x77 +180 x78 +847 x79 +199 x80
+931 x81 +184 x82 +860 x83 +512 x84 +294 x85 +964 x86 +205 x87 +374
x88 +789 x89 +60 x90 +561 x91 +832 x92 +456 x93 +670 x94 +931 x95 +136
x96 +452 x97 +532 x98 +786 x99 +885 x100 +574 x101 +305 x102 +808 x103
+740 x104 +512 x105 +733 x106 +390 x107 +294 x108 +295 x109 +29 x110
+557 x111 +229 x112 +194 x113 +686 x114 +367 x115 +515 x116 +347 x117
+18 x118 +469 x119 +448 x120 +624 x121 +673 x122 +764 x123 +589 x124
+277 x125 +852 x126 +207 x127 +453 x128 +132 x129 +865 x130 +710 x131
+825 x132 +904 x133 +293 x134 +887 x135 +463 x136 +713 x137 +668 x138
+883 x139 +843 x140 +1 x141 -983 x190 -1966 x191 -3932 x192 -7864 x193
-15728 x194 -31456 x195 -62912 x196 -125824 x197 = 0;
1 x1 +837 x2 +937 x3 +863 x4 +485 x5 +486 x6 +789 x7 +947 x8 +743 x9
+497 x10 +643 x11 +269 x12 +182 x13 +97 x14 +356 x15 +487 x16 +739 x17
+210 x18 +467 x19 +298 x20 +604 x21 +608 x22 +619 x23 +475 x24 +882
x25 +277 x26 +582 x27 +850 x28 +844 x29 +837 x30 +533 x31 +876 x32
+868 x33 +36 x34 +691 x35 +563 x36 +161 x37 +29 x38 +818 x39 +289 x40
+683 x41 +954 x42 +583 x43 +740 x44 +167 x45 +212 x46 +174 x47 +825
x48 +306 x49 +90 x50 +608 x51 +395 x52 +239 x53 +615 x54 +397 x55 +396
x56 +116 x57 +695 x58 +224 x59 +530 x60 +225 x61 +735 x62 +461 x63 +32
x64 +457 x65 +169 x66 +976 x67 +351 x68 +975 x69 +238 x70 +135 x71
+647 x72 +975 x73 +351 x74 +402 x75 +169 x76 +486 x77 +2 x78 +461 x79
+616 x80 +589 x81 +530 x82 +624 x83 +695 x84 +116 x85 +464 x86 +397
x87 +615 x88 +51 x89 +904 x90 +150 x91 +90 x92 +726 x93 +825 x94 +174
x95 +753 x96 +167 x97 +554 x98 +139 x99 +531 x100 +619 x101 +179 x102
+242 x103 +606 x104 +161 x105 +563 x106 +555 x107 +948 x108 +868 x109
+876 x110 +956 x111 +837 x112 +844 x113 +734 x114 +549 x115 +277 x116
+750 x117 +194 x118 +903 x119 +416 x120 +86 x121 +245 x122 +632 x123
+824 x124 +84 x125 +454 x126 +678 x127 +769 x128 +245 x129 +558 x130
+664 x131 +495 x132 +743 x133 +947 x134 +789 x135 +486 x136 +485 x137
+863 x138 +937 x139 +837 x140 +1 x141 -977 x198 -1954 x199 -3908 x200
-7816 x201 -15632 x202 -31264 x203 -62528 x204 -125056 x205 = 0;
1 x1 +831 x2 +20 x3 +51 x4 +438 x5 +321 x6 +60 x7 +516 x8 +646 x9 +555
x10 +422 x11 +98 x12 +808 x13 +703 x14 +672 x15 +148 x16 +18 x17 +64
x18 +17 x19 +261 x20 +225 x21 +765 x22 +662 x23 +648 x24 +926 x25 +552
x26 +525 x27 +117 x28 +665 x29 +838 x30 +285 x31 +383 x32 +747 x33
+811 x34 +708 x35 +452 x36 +42 x37 +22 x38 +366 x39 +766 x40 +929 x41
+242 x42 +425 x43 +476 x44 +772 x45 +395 x46 +191 x47 +603 x48 +668
x49 +51 x50 +802 x51 +765 x52 +136 x53 +506 x54 +878 x55 +832 x56 +582
x57 +352 x58 +791 x59 +168 x60 +159 x61 +378 x62 +526 x63 +633 x64
+429 x65 +84 x66 +490 x67 +294 x68 +461 x69 +752 x70 +493 x71 +770 x72
+461 x73 +294 x74 +462 x75 +84 x76 +904 x77 +474 x78 +526 x79 +847 x80
+424 x81 +168 x82 +290 x83 +352 x84 +582 x85 +265 x86 +878 x87 +506
x88 +13 x89 +610 x90 +205 x91 +51 x92 +695 x93 +603 x94 +191 x95 +277
x96 +772 x97 +790 x98 +840 x99 +154 x100 +132 x101 +623 x102 +846 x103
+58 x104 +42 x105 +452 x106 +337 x107 +819 x108 +747 x109 +383 x110
+219 x111 +838 x112 +665 x113 +208 x114 +788 x115 +552 x116 +136 x117
+36 x118 +394 x119 +560 x120 +937 x121 +234 x122 +166 x123 +208 x124
+870 x125 +689 x126 +587 x127 +212 x128 +877 x129 +387 x130 +443 x131
+553 x132 +646 x133 +516 x134 +60 x135 +321 x136 +438 x137 +51 x138
+20 x139 +831 x140 +1 x141 -971 x206 -1942 x207 -3884 x208 -7768 x209
-15536 x210 -31072 x211 -62144 x212 -124288 x213 = 0;
1 x1 +827 x2 +60 x3 +141 x4 +731 x5 +37 x6 +618 x7 +50 x8 +861 x9 +906
x10 +724 x11 +641 x12 +537 x13 +374 x14 +727 x15 +476 x16 +854 x17
+205 x18 +785 x19 +720 x20 +373 x21 +964 x22 +97 x23 +931 x24 +887 x25
+622 x26 +837 x27 +916 x28 +553 x29 +675 x30 +134 x31 +625 x32 +271
x33 +677 x34 +297 x35 +942 x36 +78 x37 +952 x38 +792 x39 +768 x40 +683
x41 +132 x42 +82 x43 +665 x44 +168 x45 +407 x46 +652 x47 +193 x48 +239
x49 +416 x50 +412 x51 +251 x52 +39 x53 +886 x54 +349 x55 +294 x56 +664
x57 +496 x58 +426 x59 +539 x60 +137 x61 +103 x62 +514 x63 +864 x64
+204 x65 +69 x66 +395 x67 +887 x68 +271 x69 +820 x70 +476 x71 +634 x72
+271 x73 +887 x74 +151 x75 +69 x76 +596 x77 +140 x78 +514 x79 +657 x80
+799 x81 +539 x82 +903 x83 +496 x84 +664 x85 +382 x86 +349 x87 +886
x88 +284 x89 +225 x90 +39 x91 +416 x92 +771 x93 +193 x94 +652 x95 +957
x96 +168 x97 +90 x98 +300 x99 +785 x100 +902 x101 +181 x102 +168 x103
+746 x104 +78 x105 +942 x106 +697 x107 +235 x108 +271 x109 +625 x110
+315 x111 +675 x112 +553 x113 +64 x114 +370 x115 +622 x116 +947 x117
+653 x118 +516 x119 +908 x120 +781 x121 +890 x122 +441 x123 +458 x124
+701 x125 +57 x126 +55 x127 +726 x128 +610 x129 +930 x130 +745 x131
+904 x132 +861 x133 +50 x134 +618 x135 +37 x136 +731 x137 +141 x138
+60 x139 +827 x140 +1 x141 -967 x214 -1934 x215 -3868 x216 -7736 x217
-15472 x218 -30944 x219 -61888 x220 -123776 x221 = 0;
1 x1 +813 x2 +200 x3 +330 x4 +610 x5 +562 x6 +697 x7 +544 x8 +486 x9
+492 x10 +438 x11 +427 x12 +872 x13 +6 x14 +40 x15 +230 x16 +832 x17
+883 x18 +666 x19 +399 x20 +907 x21 +948 x22 +732 x23 +107 x24 +493
x25 +752 x26 +944 x27 +329 x28 +582 x29 +97 x30 +594 x31 +504 x32 +490
x33 +895 x34 +136 x35 +695 x36 +896 x37 +243 x38 +21 x39 +309 x40 +898
x41 +155 x42 +637 x43 +596 x44 +705 x45 +89 x46 +673 x47 +304 x48 +524
x49 +436 x50 +860 x51 +925 x52 +750 x53 +575 x54 +282 x55 +803 x56
+918 x57 +545 x58 +485 x59 +213 x60 +661 x61 +343 x62 +259 x63 +453
x64 +224 x65 +161 x66 +30 x67 +76 x68 +504 x69 +451 x70 +47 x71 +891
x72 +504 x73 +76 x74 +13 x75 +161 x76 +575 x77 +820 x78 +259 x79 +720
x80 +222 x81 +213 x82 +136 x83 +545 x84 +918 x85 +447 x86 +282 x87
+575 x88 +945 x89 +49 x90 +942 x91 +436 x92 +331 x93 +304 x94 +673 x95
+184 x96 +705 x97 +819 x98 +539 x99 +849 x100 +532 x101 +663 x102 +660
x103 +518 x104 +896 x105 +695 x106 +254 x107 +255 x108 +490 x109 +504
x110 +491 x111 +97 x112 +582 x113 +169 x114 +150 x115 +752 x116 +382
x117 +897 x118 +49 x119 +803 x120 +796 x121 +591 x122 +102 x123 +752
x124 +292 x125 +11 x126 +712 x127 +863 x128 +6 x129 +716 x130 +459
x131 +490 x132 +486 x133 +544 x134 +697 x135 +562 x136 +610 x137 +330
x138 +200 x139 +813 x140 +1 x141 -953 x222 -1906 x223 -3812 x224 -7624
x225 -15248 x226 -30496 x227 -60992 x228 -121984 x229 = 0;
1 x1 +807 x2 +260 x3 +351 x4 +526 x5 +466 x6 +879 x7 +490 x8 +140 x9
+468 x10 +141 x11 +374 x12 +718 x13 +210 x14 +345 x15 +16 x16 +439 x17
+875 x18 +349 x19 +778 x20 +222 x21 +101 x22 +19 x23 +412 x24 +108 x25
+134 x26 +897 x27 +497 x28 +773 x29 +920 x30 +462 x31 +762 x32 +522
x33 +889 x34 +772 x35 +472 x36 +389 x37 +532 x38 +92 x39 +135 x40 +298
x41 +774 x42 +774 x43 +361 x44 +887 x45 +606 x46 +922 x47 +121 x48
+545 x49 +804 x50 +786 x51 +334 x52 +340 x53 +535 x54 +288 x55 +118
x56 +630 x57 +238 x58 +497 x59 +716 x60 +303 x61 +739 x62 +934 x63
+556 x64 +530 x65 +888 x66 +588 x67 +363 x68 +589 x69 +70 x70 +599 x71
+751 x72 +589 x73 +363 x74 +102 x75 +888 x76 +111 x77 +307 x78 +934
x79 +459 x80 +137 x81 +716 x82 +800 x83 +238 x84 +630 x85 +272 x86
+288 x87 +535 x88 +663 x89 +116 x90 +410 x91 +804 x92 +824 x93 +121
x94 +922 x95 +49 x96 +887 x97 +547 x98 +705 x99 +211 x100 +914 x101
+129 x102 +116 x103 +518 x104 +389 x105 +472 x106 +516 x107 +348 x108
+522 x109 +762 x110 +467 x111 +920 x112 +773 x113 +847 x114 +869 x115
+134 x116 +264 x117 +945 x118 +608 x119 +372 x120 +665 x121 +568 x122
+460 x123 +498 x124 +395 x125 +946 x126 +646 x127 +869 x128 +811 x129
+663 x130 +162 x131 +466 x132 +140 x133 +490 x134 +879 x135 +466 x136
+526 x137 +351 x138 +260 x139 +807 x140 +1 x141 -947 x230 -1894 x231
-3788 x232 -7576 x233 -15152 x234 -30304 x235 -60608 x236 -121216
x237 = 0;
1 x1 +801 x2 +320 x3 +336 x4 +725 x5 +41 x6 +489 x7 +318 x8 +124 x9
+373 x10 +499 x11 +495 x12 +114 x13 +806 x14 +929 x15 +508 x16 +552
x17 +254 x18 +333 x19 +521 x20 +527 x21 +402 x22 +176 x23 +570 x24
+727 x25 +668 x26 +293 x27 +921 x28 +889 x29 +664 x30 +309 x31 +143
x32 +593 x33 +89 x34 +40 x35 +903 x36 +404 x37 +186 x38 +252 x39 +595
x40 +95 x41 +939 x42 +900 x43 +531 x44 +916 x45 +342 x46 +859 x47 +125
x48 +624 x49 +4 x50 +386 x51 +557 x52 +375 x53 +818 x54 +831 x55 +799
x56 +626 x57 +109 x58 +901 x59 +813 x60 +210 x61 +154 x62 +210 x63
+419 x64 +539 x65 +853 x66 +722 x67 +844 x68 +877 x69 +97 x70 +61 x71
+58 x72 +877 x73 +844 x74 +908 x75 +853 x76 +844 x77 +622 x78 +210 x79
+919 x80 +5 x81 +813 x82 +268 x83 +109 x84 +626 x85 +153 x86 +831 x87
+818 x88 +367 x89 +402 x90 +49 x91 +4 x92 +725 x93 +125 x94 +859 x95
+237 x96 +916 x97 +576 x98 +319 x99 +900 x100 +674 x101 +617 x102 +426
x103 +420 x104 +404 x105 +903 x106 +26 x107 +833 x108 +593 x109 +143
x110 +50 x111 +664 x112 +889 x113 +836 x114 +880 x115 +668 x116 +572
x117 +487 x118 +260 x119 +542 x120 +589 x121 +390 x122 +737 x123 +723
x124 +543 x125 +597 x126 +871 x127 +326 x128 +213 x129 +784 x130 +520
x131 +371 x132 +124 x133 +318 x134 +489 x135 +41 x136 +725 x137 +336
x138 +320 x139 +801 x140 +1 x141 -941 x238 -1882 x239 -3764 x240 -7528
x241 -15056 x242 -30112 x243 -60224 x244 -120448 x245 = 0;
1 x1 +797 x2 +360 x3 +306 x4 +295 x5 +409 x6 +636 x7 +140 x8 +15 x9
+713 x10 +145 x11 +53 x12 +640 x13 +97 x14 +516 x15 +267 x16 +184 x17
+447 x18 +144 x19 +716 x20 +779 x21 +843 x22 +315 x23 +778 x24 +673
x25 +200 x26 +465 x27 +255 x28 +178 x29 +16 x30 +410 x31 +500 x32 +219
x33 +425 x34 +772 x35 +361 x36 +699 x37 +329 x38 +278 x39 +20 x40 +755
x41 +472 x42 +763 x43 +159 x44 +342 x45 +222 x46 +83 x47 +149 x48 +511
x49 +922 x50 +99 x51 +878 x52 +246 x53 +769 x54 +727 x55 +813 x56 +567
x57 +132 x58 +322 x59 +345 x60 +468 x61 +498 x62 +199 x63 +647 x64
+786 x65 +230 x66 +474 x67 +608 x68 +361 x69 +823 x70 +846 x71 +431
x72 +361 x73 +608 x74 +832 x75 +230 x76 +686 x77 +872 x78 +199 x79
+693 x80 +882 x81 +345 x82 +698 x83 +132 x84 +567 x85 +841 x86 +727
x87 +769 x88 +835 x89 +154 x90 +425 x91 +922 x92 +736 x93 +149 x94 +83
x95 +133 x96 +342 x97 +225 x98 +276 x99 +94 x100 +56 x101 +602 x102
+840 x103 +242 x104 +699 x105 +361 x106 +839 x107 +822 x108 +219 x109
+500 x110 +130 x111 +16 x112 +178 x113 +455 x114 +167 x115 +200 x116
+604 x117 +837 x118 +98 x119 +725 x120 +230 x121 +253 x122 +554 x123
+7 x124 +784 x125 +61 x126 +850 x127 +426 x128 +743 x129 +342 x130
+166 x131 +711 x132 +15 x133 +140 x134 +636 x135 +409 x136 +295 x137
+306 x138 +360 x139 +797 x140 +1 x141 -937 x246 -1874 x247 -3748 x248
-7496 x249 -14992 x250 -29984 x251 -59968 x252 -119936 x253 = 0;
1 x1 +789 x2 +440 x3 +198 x4 +186 x5 +329 x6 +494 x7 +497 x8 +679 x9
+566 x10 +39 x11 +111 x12 +499 x13 +376 x14 +413 x15 +402 x16 +333 x17
+847 x18 +75 x19 +452 x20 +643 x21 +273 x22 +51 x23 +731 x24 +671 x25
+750 x26 +593 x27 +131 x28 +640 x29 +621 x30 +592 x31 +353 x32 +619
x33 +819 x34 +799 x35 +436 x36 +318 x37 +758 x38 +298 x39 +596 x40
+128 x41 +613 x42 +572 x43 +853 x44 +675 x45 +165 x46 +460 x47 +844
x48 +577 x49 +137 x50 +606 x51 +747 x52 +54 x53 +620 x54 +831 x55 +475
x56 +722 x57 +364 x58 +734 x59 +326 x60 +472 x61 +257 x62 +783 x63
+787 x64 +902 x65 +668 x66 +375 x67 +28 x68 +203 x69 +778 x70 +59 x71
+615 x72 +203 x73 +28 x74 +84 x75 +668 x76 +909 x77 +449 x78 +783 x79
+14 x80 +731 x81 +326 x82 +530 x83 +364 x84 +722 x85 +218 x86 +831 x87
+620 x88 +797 x89 +809 x90 +915 x91 +137 x92 +404 x93 +844 x94 +460
x95 +724 x96 +675 x97 +347 x98 +57 x99 +658 x100 +309 x101 +788 x102
+475 x103 +269 x104 +318 x105 +436 x106 +242 x107 +209 x108 +619 x109
+353 x110 +455 x111 +621 x112 +640 x113 +868 x114 +864 x115 +750 x116
+757 x117 +477 x118 +337 x119 +449 x120 +250 x121 +56 x122 +862 x123
+645 x124 +12 x125 +415 x126 +602 x127 +441 x128 +610 x129 +400 x130
+60 x131 +564 x132 +679 x133 +497 x134 +494 x135 +329 x136 +186 x137
+198 x138 +440 x139 +789 x140 +1 x141 -929 x254 -1858 x255 -3716 x256
-7432 x257 -14864 x258 -29728 x259 -59456 x260 -118912 x261 = 0;
x32 +1 x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1
x42 +1 x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 +1 x51 +1
x52 +1 x53 +1 x54 +1 x55 +1 x56 +1 x57 +1 x58 +1 x59 +1 x60 +1 x61 +1
x62 +1 x63 +1 x64 +1 x65 +1 x66 +1 x67 +1 x68 +1 x69 +1 x70 +1 x71 +1
x72 +1 x73 +1 x74 +1 x75 +1 x76 +1 x77 +1 x78 +1 x79 +1 x80 +1 x81 +1
x82 +1 x83 +1 x84 +1 x85 +1 x86 +1 x87 +1 x88 +1 x89 +1 x90 +1 x91 +1
x92 +1 x93 +1 x94 +1 x95 +1 x96 +1 x97 +1 x98 +1 x99 +1 x100 +1 x101
+1 x102 +1 x103 +1 x104 +1 x105 +1 x106 +1 x107 +1 x108 +1 x109 +1
x110 +1 x111 +1 x112 +1 x113 +1 x114 +1 x115 +1 x116 +1 x117 +1 x118
+1 x119 +1 x120 +1 x121 +1 x122 +1 x123 +1 x124 +1 x125 +1 x126 +1
x127 +1 x128 +1 x129 +1 x130 +1 x131 +1 x132 +1 x133 +1 x134 +1 x135
+1 x136 +1 x137 +1 x138 +1 x139 +1 x140 +1 x141 >= 1;
x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1 x42 +1
x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 +1 x51 +1 x52 +1
x53 +1 x54 +1 x55 +1 x56 +1 x57 +1 x58 +1 x59 +1 x60 +1 x61 +1 x62 +1
x63 +1 x64 +1 x65 +1 x66 +1 x67 +1 x68 +1 x69 +1 x70 +1 x71 +1 x72 +1
x73 +1 x74 +1 x75 +1 x76 +1 x77 +1 x78 +1 x79 +1 x80 +1 x81 +1 x82 +1
x83 +1 x84 +1 x85 +1 x86 +1 x87 +1 x88 +1 x89 +1 x90 +1 x91 +1 x92 +1
x93 +1 x94 +1 x95 +1 x96 +1 x97 +1 x98 +1 x99 +1 x100 +1 x101 +1 x102
+1 x103 +1 x104 +1 x105 +1 x106 +1 x107 +1 x108 +1 x109 +1 x110 +1
x111 +1 x112 +1 x113 +1 x114 +1 x115 +1 x116 +1 x117 +1 x118 +1 x119
+1 x120 +1 x121 +1 x122 +1 x123 +1 x124 +1 x125 +1 x126 +1 x127 +1
x128 +1 x129 +1 x130 +1 x131 +1 x132 +1 x133 +1 x134 +1 x135 +1 x136
+1 x137 +1 x138 +1 x139 +1 x140 +1 x141 <= 139 ;
Raphael
> Ok, two comments.
>
> First, the CNF-generation of MiniSat+ is know to be buggy (this
> feature was never tested much by us). I have started porting MiniSat+
> to a newer MiniSat backend, and I *think* that might solve this
> problem. If you'd like to try it out, you can download the source here
> (choose the "next" branch!):
>
> https://github.com/niklasso/minisatp
>
> You'll need to also download the source to MiniSat separately:
>
> https://github.com/niklasso/minisat
>
don't have to split the equality constraint up any more using the
Chinese Remainder Theorem and converting the added integer variable to
binary ones. The upshot is that I now have only 3 constraints but with
big coefficients in one of them.
> Secondly, and maybe more importantly, even though generating
> constraints via adders produces smaller CNFs, the performance is
> usually very very bad. The adder method is really a last resort, that
> sometimes works even if performance is bad. For instance, when I tried
> to repeat your issue with the problem you posted, MiniSat simply
> didn't terminate within 15 minutes.
>
> Is it possible to send an example of the real OPB-problem that you'd
> like to solve? Then I can take a look myself and maybe come up with
> some recommendation.
>
large coefficients.
* #variable= 141 #constraint= 3
1 x1 -140 x2 +9730 x3 -447580 x4 +15329615 x5 -416965528 x6
+9381724380 x7 -179593009560 x8 +2985733783935 x9 -43790762164384 x10
+573658984353452 x11 -6779606178722296 x12 +72880766421268000 x13
-717595238609422720 x14 +6509613950242167808 x15 -54680757182033354752
x16 +427193415484620800000 x17 -3115999030593960017920 x18
+21292660042393605636096 x19 -136721290798510278443008 x20
+827163809331026101010432 x21 -4726650339034364762914816 x22
+25566881379322088459862016 x23 -131169217511304783116369920 x24
+639449935367587246911782912 x25 -2967047700105727773060890624 x26
+13123480212006120928923615232 x27 -55410249784025115801088425984 x28
+223619936628378720393616162816 x29 -863635617323493296638223450112
x30 +3195451784096823542873587712000 x31
-11338699879052724554836423475200 x32
+38622446463022766483790519861248 x33
-126400733878982331842910215995392 x34
+397790544854461169205182669520896 x35
-1204737078702064618467635754958848 x36
+3513816479547775263902622969495552 x37
-9876673347917898790505860183359488 x38
+26770983021988185096613602646818816 x39
-70016417134435466734995794122768384 x40
+176791453264437922141973003523588096 x41
-431198666498598912119527957910781952 x42
+1016396856746722048937408536105713664 x43
-2316439347934321778381895802571194368 x44
+5106695835219179517446766187878809600 x45
-10894284448468144145103482210314354688 x46
+22499065708791367665104398223969091584 x47
-44998131417582810888072522362261602304 x48
+87183879621565055663583525233875746816 x49
-163692182146615402644169042197838036992 x50
+297919771506855169697017187846047399936 x51
-525740773247383822368775271230382014464 x52
+899825554211802918761313906622587731968 x53
-1494049976804446989608787629933024247808 x54
+2407080518185190017243511961637896585216 x55
-3763798628435065636949864282772826226688 x56
+5712908632445624127183722384139564875776 x57
-8419023247815115797917747728052060684288 x58
+12047912578769003980849324116817920131072 x59
-16744556465408542325919626763390364418048 x60
+22605151228300904344813370253646567047168 x61
-29646099971544074661812364867319915085824 x62
+37774869318581156314836050191366469189632 x63
-46768885823003336805696402525829948506112 x64
+56268815755800470399325532916222827429888 x65
-65791230729861077356267334426532736139264 x66
+74762762193024615351390195699261311549440 x67
-82573797049006459320500090861997787185152 x68
+88645399773199578661523243729816700059648 x69
-92499547589427908726131345622661450432512 x70
+93820969697847617436442575650631073136640 x71
-92499547589425278103547864189577289793536 x72
+88645399773199578661523243729816700059648 x73
-82573797049006459320500090861997787185152 x74
+74762762193028870770275239193956277288960 x75
-65791230729861077356267334426532736139264 x76
+56268815755802066181407424226733439582208 x77
-46768885823004661788394700159405426475008 x78
+37774869318581156314836050191366469189632 x79
-29646099971544920909886095107742209409024 x80
+22605151228301547493349405236367510732800 x81
-16744556465408542325919626763390364418048 x82
+12047912578769347315782094671503536685056 x83
-8419023247815115797917747728052060684288 x84
+5712908632445624127183722384139564875776 x85
-3763798628435172626884900177454787723264 x86
+2407080518185190017243511961637896585216 x87
-1494049976804446989608787629933024247808 x88
+899825554211777380203374547581272064000 x89
-525740773247398707267929276352095584256 x90
+297919771506863632177754490250270343168 x91
-163692182146615402644169042197838036992 x92
+87183879621567530183620548927967723520 x93
-44998131417582810888072522362261602304 x94
+22499065708791367665104398223969091584 x95
-10894284448467834830098854248552857600 x96
+5106695835219179517446766187878809600 x97
-2316439347934255960399040806891028480 x98
+1016396856746693124442700959528779776 x99
-431198666498605036438560429481918464 x100
+176791453264435376491290831605465088 x101
-70016417134436462859175774438555648 x102
+26770983021987802326674073173622784 x103
-9876673347918039446929422218690560 x104
+3513816479547775263902622969495552 x105
-1204737078702064618467635754958848 x106
+397790544854472482247446624206848 x107
-126400733878980548417457777278976 x108
+38622446463022766483790519861248 x109
-11338699879052724554836423475200 x110
+3195451784096869141819814838272 x111 -863635617323493296638223450112
x112 +223619936628378720393616162816 x113
-55410249784023541300437450752 x114 +13123480212006494762877059072
x115 -2967047700105727773060890624 x116 +639449935367605526292594688
x117 -131169217511301982797692928 x118 +25566881379321542999015424
x119 -4726650339034431871778816 x120 +827163809331014424068096 x121
-136721290798515143835648 x122 +21292660042393907625984 x123
-3115999030593804828672 x124 +427193415484626894848 x125
-54680757182034526208 x126 +6509613950242259968 x127
-717595238609453312 x128 +72880766421269040 x129 -6779606178722007
x130 +573658984353473 x131 -43790762164386 x132 +2985733783935 x133
-179593009560 x134 +9381724380 x135 -416965528 x136 +15329615 x137
-447580 x138 +9730 x139 -140 x140 +1 x141 = 0;
1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1
x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1
x22 +1 x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 +1 x30 +1 x31 +1
x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1
x32 +1 x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1
x42 +1 x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 +1 x51 +1
x52 +1 x53 +1 x54 +1 x55 +1 x56 +1 x57 +1 x58 +1 x59 +1 x60 +1 x61 +1
x62 +1 x63 +1 x64 +1 x65 +1 x66 +1 x67 +1 x68 +1 x69 +1 x70 +1 x71 +1
x72 +1 x73 +1 x74 +1 x75 +1 x76 +1 x77 +1 x78 +1 x79 +1 x80 +1 x81 +1
x82 +1 x83 +1 x84 +1 x85 +1 x86 +1 x87 +1 x88 +1 x89 +1 x90 +1 x91 +1
x92 +1 x93 +1 x94 +1 x95 +1 x96 +1 x97 +1 x98 +1 x99 +1 x100 +1 x101
+1 x102 +1 x103 +1 x104 +1 x105 +1 x106 +1 x107 +1 x108 +1 x109 +1
x110 +1 x111 +1 x112 +1 x113 +1 x114 +1 x115 +1 x116 +1 x117 +1 x118
+1 x119 +1 x120 +1 x121 +1 x122 +1 x123 +1 x124 +1 x125 +1 x126 +1
x127 +1 x128 +1 x129 +1 x130 +1 x131 +1 x132 +1 x133 +1 x134 +1 x135
+1 x136 +1 x137 +1 x138 +1 x139 +1 x140 +1 x141 >= 1;
1 x1 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1 x12 +1
x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1
x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 +1 x30 +1 x31 +1 x32 +1
x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1
x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1 x42 +1
x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 +1 x51 +1 x52 +1
x53 +1 x54 +1 x55 +1 x56 +1 x57 +1 x58 +1 x59 +1 x60 +1 x61 +1 x62 +1
x63 +1 x64 +1 x65 +1 x66 +1 x67 +1 x68 +1 x69 +1 x70 +1 x71 +1 x72 +1
x73 +1 x74 +1 x75 +1 x76 +1 x77 +1 x78 +1 x79 +1 x80 +1 x81 +1 x82 +1
x83 +1 x84 +1 x85 +1 x86 +1 x87 +1 x88 +1 x89 +1 x90 +1 x91 +1 x92 +1
x93 +1 x94 +1 x95 +1 x96 +1 x97 +1 x98 +1 x99 +1 x100 +1 x101 +1 x102
+1 x103 +1 x104 +1 x105 +1 x106 +1 x107 +1 x108 +1 x109 +1 x110 +1
x111 +1 x112 +1 x113 +1 x114 +1 x115 +1 x116 +1 x117 +1 x118 +1 x119
+1 x120 +1 x121 +1 x122 +1 x123 +1 x124 +1 x125 +1 x126 +1 x127 +1
x128 +1 x129 +1 x130 +1 x131 +1 x132 +1 x133 +1 x134 +1 x135 +1 x136
+1 x137 +1 x138 +1 x139 +1 x140 +1 x141 <= 139 ;
and after conversion to reduce the size of the coefficients
* #variable= 261 #constraint= 17
1 x1 +881 x2 +541 x3 +639 x4 +321 x5 +662 x6 +420 x7 +128 x8 +935 x9
+917 x10 +363 x11 +391 x12 +391 x13 +515 x14 +812 x15 +176 x16 +747
x17 +1008 x18 +1017 x19 +119 x20 +1018 x21 +613 x22 +247 x23 +952 x24
+961 x25 +22 x26 +20 x27 +577 x28 +850 x29 +852 x30 +956 x31 +803 x32
+1001 x33 +661 x34 +209 x35 +144 x36 +698 x37 +199 x38 +76 x39 +493
x40 +190 x41 +300 x42 +757 x43 +169 x44 +484 x45 +357 x46 +605 x47
+741 x48 +202 x49 +833 x50 +455 x51 +427 x52 +377 x53 +803 x54 +23 x55
+911 x56 +807 x57 +360 x58 +83 x59 +656 x60 +1004 x61 +141 x62 +961
x63 +66 x64 +990 x65 +923 x66 +516 x67 +716 x68 +888 x69 +161 x70 +848
x71 +254 x72 +888 x73 +716 x74 +216 x75 +923 x76 +367 x77 +113 x78
+961 x79 +920 x80 +657 x81 +656 x82 +82 x83 +360 x84 +807 x85 +701 x86
+23 x87 +803 x88 +249 x89 +878 x90 +437 x91 +833 x92 +885 x93 +741 x94
+605 x95 +570 x96 +484 x97 +340 x98 +778 x99 +505 x100 +675 x101 +594
x102 +25 x103 +88 x104 +698 x105 +144 x106 +662 x107 +656 x108 +1001
x109 +803 x110 +77 x111 +852 x112 +850 x113 +175 x114 +1014 x115 +22
x116 +138 x117 +919 x118 +825 x119 +457 x120 +852 x121 +220 x122 +546
x123 +298 x124 +225 x125 +828 x126 +61 x127 +553 x128 +410 x129 +680
x130 +384 x131 +915 x132 +935 x133 +128 x134 +420 x135 +662 x136 +321
x137 +639 x138 +541 x139 +881 x140 +1 x141 -1021 x142 -2042 x143 -4084
x144 -8168 x145 -16336 x146 -32672 x147 -65344 x148 -130688 x149 = 0;
1 x1 +879 x2 +559 x3 +780 x4 +798 x5 +101 x6 +275 x7 +413 x8 +649 x9
+1007 x10 +994 x11 +614 x12 +284 x13 +277 x14 +618 x15 +817 x16 +848
x17 +314 x18 +311 x19 +25 x20 +144 x21 +496 x22 +172 x23 +303 x24 +91
x25 +470 x26 +142 x27 +934 x28 +315 x29 +304 x30 +531 x31 +86 x32 +106
x33 +988 x34 +741 x35 +932 x36 +247 x37 +246 x38 +257 x39 +22 x40 +233
x41 +805 x42 +245 x43 +920 x44 +757 x45 +831 x46 +446 x47 +360 x48
+723 x49 +889 x50 +886 x51 +250 x52 +16 x53 +473 x54 +327 x55 +140 x56
+812 x57 +996 x58 +314 x59 +572 x60 +301 x61 +450 x62 +284 x63 +143
x64 +818 x65 +747 x66 +6 x67 +949 x68 +793 x69 +405 x70 +389 x71 +536
x72 +793 x73 +949 x74 +128 x75 +747 x76 +609 x77 +860 x78 +284 x79
+391 x80 +998 x81 +572 x82 +303 x83 +996 x84 +812 x85 +931 x86 +327
x87 +473 x88 +307 x89 +296 x90 +265 x91 +889 x92 +480 x93 +360 x94
+446 x95 +928 x96 +757 x97 +928 x98 +374 x99 +393 x100 +516 x101 +753
x102 +486 x103 +545 x104 +247 x105 +932 x106 +256 x107 +686 x108 +106
x109 +86 x110 +228 x111 +304 x112 +315 x113 +233 x114 +690 x115 +470
x116 +419 x117 +223 x118 +869 x119 +326 x120 +950 x121 +191 x122 +378
x123 +957 x124 +38 x125 +192 x126 +49 x127 +255 x128 +305 x129 +903
x130 +1015 x131 +1005 x132 +649 x133 +413 x134 +275 x135 +101 x136
+798 x137 +780 x138 +559 x139 +879 x140 +1 x141 -1019 x150 -2038 x151
-4076 x152 -8152 x153 -16304 x154 -32608 x155 -65216 x156 -130432
x157 = 0;
1 x1 +873 x2 +613 x3 +166 x4 +899 x5 +467 x6 +129 x7 +859 x8 +281 x9
+602 x10 +442 x11 +252 x12 +609 x13 +245 x14 +251 x15 +186 x16 +928
x17 +232 x18 +581 x19 +805 x20 +362 x21 +603 x22 +479 x23 +858 x24
+476 x25 +702 x26 +832 x27 +374 x28 +866 x29 +656 x30 +233 x31 +864
x32 +185 x33 +168 x34 +17 x35 +447 x36 +895 x37 +735 x38 +702 x39 +24
x40 +757 x41 +966 x42 +341 x43 +49 x44 +599 x45 +244 x46 +936 x47 +472
x48 +149 x49 +468 x50 +608 x51 +800 x52 +752 x53 +673 x54 +437 x55
+700 x56 +101 x57 +365 x58 +434 x59 +972 x60 +603 x61 +363 x62 +319
x63 +132 x64 +29 x65 +868 x66 +14 x67 +418 x68 +256 x69 +343 x70 +464
x71 +945 x72 +256 x73 +418 x74 +94 x75 +868 x76 +59 x77 +15 x78 +319
x79 +255 x80 +523 x81 +972 x82 +993 x83 +365 x84 +101 x85 +203 x86
+437 x87 +673 x88 +858 x89 +640 x90 +447 x91 +468 x92 +371 x93 +472
x94 +936 x95 +525 x96 +599 x97 +508 x98 +162 x99 +879 x100 +373 x101
+138 x102 +380 x103 +934 x104 +895 x105 +447 x106 +316 x107 +149 x108
+185 x109 +864 x110 +598 x111 +656 x112 +866 x113 +225 x114 +890 x115
+702 x116 +636 x117 +555 x118 +2 x119 +988 x120 +196 x121 +567 x122
+987 x123 +919 x124 +555 x125 +771 x126 +228 x127 +43 x128 +636 x129
+541 x130 +463 x131 +600 x132 +281 x133 +859 x134 +129 x135 +467 x136
+899 x137 +166 x138 +613 x139 +873 x140 +1 x141 -1013 x158 -2026 x159
-4052 x160 -8104 x161 -16208 x162 -32416 x163 -64832 x164 -129664
x165 = 0;
1 x1 +869 x2 +649 x3 +416 x4 +887 x5 +695 x6 +2 x7 +250 x8 +132 x9 +78
x10 +816 x11 +398 x12 +553 x13 +636 x14 +745 x15 +210 x16 +876 x17
+662 x18 +612 x19 +39 x20 +395 x21 +1003 x22 +326 x23 +573 x24 +455
x25 +821 x26 +619 x27 +940 x28 +22 x29 +525 x30 +375 x31 +613 x32 +353
x33 +591 x34 +459 x35 +998 x36 +998 x37 +589 x38 +126 x39 +672 x40
+153 x41 +532 x42 +846 x43 +366 x44 +715 x45 +230 x46 +777 x47 +631
x48 +598 x49 +345 x50 +429 x51 +14 x52 +872 x53 +914 x54 +408 x55
+1000 x56 +689 x57 +623 x58 +409 x59 +619 x60 +822 x61 +797 x62 +910
x63 +250 x64 +237 x65 +253 x66 +499 x67 +205 x68 +124 x69 +911 x70
+410 x71 +497 x72 +124 x73 +205 x74 +957 x75 +253 x76 +661 x77 +644
x78 +910 x79 +511 x80 +999 x81 +619 x82 +329 x83 +623 x84 +689 x85
+357 x86 +408 x87 +914 x88 +814 x89 +625 x90 +896 x91 +345 x92 +426
x93 +631 x94 +777 x95 +713 x96 +715 x97 +256 x98 +98 x99 +178 x100
+638 x101 +116 x102 +230 x103 +688 x104 +998 x105 +998 x106 +190 x107
+502 x108 +353 x109 +613 x110 +238 x111 +525 x112 +22 x113 +299 x114
+588 x115 +821 x116 +968 x117 +57 x118 +117 x119 +442 x120 +142 x121
+354 x122 +836 x123 +665 x124 +355 x125 +203 x126 +77 x127 +314 x128
+584 x129 +687 x130 +837 x131 +76 x132 +132 x133 +250 x134 +2 x135
+695 x136 +887 x137 +416 x138 +649 x139 +869 x140 +1 x141 -1009 x166
-2018 x167 -4036 x168 -8072 x169 -16144 x170 -32288 x171 -64576 x172
-129152 x173 = 0;
1 x1 +857 x2 +757 x3 +73 x4 +740 x5 +809 x6 +242 x7 +210 x8 +746 x9
+354 x10 +768 x11 +759 x12 +393 x13 +967 x14 +472 x15 +230 x16 +87 x17
+706 x18 +960 x19 +305 x20 +424 x21 +169 x22 +935 x23 +9 x24 +968 x25
+567 x26 +768 x27 +426 x28 +511 x29 +107 x30 +996 x31 +954 x32 +859
x33 +811 x34 +947 x35 +763 x36 +739 x37 +59 x38 +172 x39 +461 x40 +374
x41 +620 x42 +924 x43 +139 x44 +409 x45 +520 x46 +436 x47 +25 x48 +678
x49 +779 x50 +909 x51 +432 x52 +400 x53 +762 x54 +952 x55 +135 x56
+410 x57 +596 x58 +842 x59 +525 x60 +657 x61 +590 x62 +488 x63 +880
x64 +218 x65 +114 x66 +784 x67 +783 x68 +469 x69 +441 x70 +371 x71
+517 x72 +469 x73 +783 x74 +731 x75 +114 x76 +572 x77 +6 x78 +488 x79
+221 x80 +419 x81 +525 x82 +610 x83 +596 x84 +410 x85 +109 x86 +952
x87 +762 x88 +498 x89 +672 x90 +145 x91 +779 x92 +962 x93 +25 x94 +436
x95 +57 x96 +409 x97 +304 x98 +543 x99 +608 x100 +357 x101 +411 x102
+919 x103 +832 x104 +739 x105 +763 x106 +442 x107 +679 x108 +859 x109
+954 x110 +868 x111 +107 x112 +511 x113 +877 x114 +410 x115 +567 x116
+636 x117 +734 x118 +884 x119 +778 x120 +851 x121 +566 x122 +545 x123
+922 x124 +274 x125 +249 x126 +908 x127 +285 x128 +436 x129 +51 x130
+789 x131 +352 x132 +746 x133 +210 x134 +242 x135 +809 x136 +740 x137
+73 x138 +757 x139 +857 x140 +1 x141 -997 x174 -1994 x175 -3988 x176
-7976 x177 -15952 x178 -31904 x179 -63808 x180 -127616 x181 = 0;
1 x1 +851 x2 +811 x3 +352 x4 +827 x5 +695 x6 +714 x7 +206 x8 +787 x9
+15 x10 +717 x11 +854 x12 +579 x13 +695 x14 +868 x15 +239 x16 +658 x17
+948 x18 +382 x19 +19 x20 +692 x21 +627 x22 +985 x23 +311 x24 +832 x25
+785 x26 +170 x27 +568 x28 +358 x29 +916 x30 +355 x31 +193 x32 +815
x33 +816 x34 +726 x35 +802 x36 +639 x37 +81 x38 +11 x39 +822 x40 +647
x41 +72 x42 +160 x43 +57 x44 +451 x45 +896 x46 +134 x47 +569 x48 +91
x49 +773 x50 +676 x51 +66 x52 +725 x53 +422 x54 +966 x55 +315 x56 +164
x57 +258 x58 +250 x59 +671 x60 +456 x61 +108 x62 +836 x63 +681 x64
+192 x65 +280 x66 +107 x67 +256 x68 +180 x69 +592 x70 +26 x71 +946 x72
+180 x73 +256 x74 +155 x75 +280 x76 +210 x77 +612 x78 +836 x79 +639
x80 +211 x81 +671 x82 +380 x83 +258 x84 +164 x85 +271 x86 +966 x87
+422 x88 +205 x89 +449 x90 +86 x91 +773 x92 +675 x93 +569 x94 +134 x95
+969 x96 +451 x97 +586 x98 +643 x99 +15 x100 +486 x101 +759 x102 +441
x103 +836 x104 +639 x105 +802 x106 +548 x107 +324 x108 +815 x109 +193
x110 +669 x111 +916 x112 +358 x113 +398 x114 +185 x115 +785 x116 +452
x117 +182 x118 +200 x119 +666 x120 +455 x121 +168 x122 +858 x123 +587
x124 +856 x125 +145 x126 +865 x127 +824 x128 +628 x129 +152 x130 +738
x131 +13 x132 +787 x133 +206 x134 +714 x135 +695 x136 +827 x137 +352
x138 +811 x139 +851 x140 +1 x141 -991 x182 -1982 x183 -3964 x184 -7928
x185 -15856 x186 -31712 x187 -63424 x188 -126848 x189 = 0;
1 x1 +843 x2 +883 x3 +668 x4 +713 x5 +463 x6 +887 x7 +293 x8 +904 x9
+827 x10 +689 x11 +576 x12 +75 x13 +572 x14 +449 x15 +572 x16 +29 x17
+500 x18 +272 x19 +408 x20 +971 x21 +13 x22 +826 x23 +515 x24 +9 x25
+515 x26 +269 x27 +944 x28 +194 x29 +229 x30 +434 x31 +29 x32 +295 x33
+726 x34 +92 x35 +733 x36 +512 x37 +895 x38 +134 x39 +742 x40 +817 x41
+914 x42 +769 x43 +19 x44 +452 x45 +57 x46 +931 x47 +670 x48 +807 x49
+832 x50 +58 x51 +620 x52 +183 x53 +374 x54 +205 x55 +653 x56 +294 x57
+512 x58 +253 x59 +184 x60 +57 x61 +366 x62 +847 x63 +155 x64 +172 x65
+835 x66 +866 x67 +383 x68 +136 x69 +778 x70 +817 x71 +140 x72 +136
x73 +383 x74 +470 x75 +835 x76 +515 x77 +180 x78 +847 x79 +199 x80
+931 x81 +184 x82 +860 x83 +512 x84 +294 x85 +964 x86 +205 x87 +374
x88 +789 x89 +60 x90 +561 x91 +832 x92 +456 x93 +670 x94 +931 x95 +136
x96 +452 x97 +532 x98 +786 x99 +885 x100 +574 x101 +305 x102 +808 x103
+740 x104 +512 x105 +733 x106 +390 x107 +294 x108 +295 x109 +29 x110
+557 x111 +229 x112 +194 x113 +686 x114 +367 x115 +515 x116 +347 x117
+18 x118 +469 x119 +448 x120 +624 x121 +673 x122 +764 x123 +589 x124
+277 x125 +852 x126 +207 x127 +453 x128 +132 x129 +865 x130 +710 x131
+825 x132 +904 x133 +293 x134 +887 x135 +463 x136 +713 x137 +668 x138
+883 x139 +843 x140 +1 x141 -983 x190 -1966 x191 -3932 x192 -7864 x193
-15728 x194 -31456 x195 -62912 x196 -125824 x197 = 0;
1 x1 +837 x2 +937 x3 +863 x4 +485 x5 +486 x6 +789 x7 +947 x8 +743 x9
+497 x10 +643 x11 +269 x12 +182 x13 +97 x14 +356 x15 +487 x16 +739 x17
+210 x18 +467 x19 +298 x20 +604 x21 +608 x22 +619 x23 +475 x24 +882
x25 +277 x26 +582 x27 +850 x28 +844 x29 +837 x30 +533 x31 +876 x32
+868 x33 +36 x34 +691 x35 +563 x36 +161 x37 +29 x38 +818 x39 +289 x40
+683 x41 +954 x42 +583 x43 +740 x44 +167 x45 +212 x46 +174 x47 +825
x48 +306 x49 +90 x50 +608 x51 +395 x52 +239 x53 +615 x54 +397 x55 +396
x56 +116 x57 +695 x58 +224 x59 +530 x60 +225 x61 +735 x62 +461 x63 +32
x64 +457 x65 +169 x66 +976 x67 +351 x68 +975 x69 +238 x70 +135 x71
+647 x72 +975 x73 +351 x74 +402 x75 +169 x76 +486 x77 +2 x78 +461 x79
+616 x80 +589 x81 +530 x82 +624 x83 +695 x84 +116 x85 +464 x86 +397
x87 +615 x88 +51 x89 +904 x90 +150 x91 +90 x92 +726 x93 +825 x94 +174
x95 +753 x96 +167 x97 +554 x98 +139 x99 +531 x100 +619 x101 +179 x102
+242 x103 +606 x104 +161 x105 +563 x106 +555 x107 +948 x108 +868 x109
+876 x110 +956 x111 +837 x112 +844 x113 +734 x114 +549 x115 +277 x116
+750 x117 +194 x118 +903 x119 +416 x120 +86 x121 +245 x122 +632 x123
+824 x124 +84 x125 +454 x126 +678 x127 +769 x128 +245 x129 +558 x130
+664 x131 +495 x132 +743 x133 +947 x134 +789 x135 +486 x136 +485 x137
+863 x138 +937 x139 +837 x140 +1 x141 -977 x198 -1954 x199 -3908 x200
-7816 x201 -15632 x202 -31264 x203 -62528 x204 -125056 x205 = 0;
1 x1 +831 x2 +20 x3 +51 x4 +438 x5 +321 x6 +60 x7 +516 x8 +646 x9 +555
x10 +422 x11 +98 x12 +808 x13 +703 x14 +672 x15 +148 x16 +18 x17 +64
x18 +17 x19 +261 x20 +225 x21 +765 x22 +662 x23 +648 x24 +926 x25 +552
x26 +525 x27 +117 x28 +665 x29 +838 x30 +285 x31 +383 x32 +747 x33
+811 x34 +708 x35 +452 x36 +42 x37 +22 x38 +366 x39 +766 x40 +929 x41
+242 x42 +425 x43 +476 x44 +772 x45 +395 x46 +191 x47 +603 x48 +668
x49 +51 x50 +802 x51 +765 x52 +136 x53 +506 x54 +878 x55 +832 x56 +582
x57 +352 x58 +791 x59 +168 x60 +159 x61 +378 x62 +526 x63 +633 x64
+429 x65 +84 x66 +490 x67 +294 x68 +461 x69 +752 x70 +493 x71 +770 x72
+461 x73 +294 x74 +462 x75 +84 x76 +904 x77 +474 x78 +526 x79 +847 x80
+424 x81 +168 x82 +290 x83 +352 x84 +582 x85 +265 x86 +878 x87 +506
x88 +13 x89 +610 x90 +205 x91 +51 x92 +695 x93 +603 x94 +191 x95 +277
x96 +772 x97 +790 x98 +840 x99 +154 x100 +132 x101 +623 x102 +846 x103
+58 x104 +42 x105 +452 x106 +337 x107 +819 x108 +747 x109 +383 x110
+219 x111 +838 x112 +665 x113 +208 x114 +788 x115 +552 x116 +136 x117
+36 x118 +394 x119 +560 x120 +937 x121 +234 x122 +166 x123 +208 x124
+870 x125 +689 x126 +587 x127 +212 x128 +877 x129 +387 x130 +443 x131
+553 x132 +646 x133 +516 x134 +60 x135 +321 x136 +438 x137 +51 x138
+20 x139 +831 x140 +1 x141 -971 x206 -1942 x207 -3884 x208 -7768 x209
-15536 x210 -31072 x211 -62144 x212 -124288 x213 = 0;
1 x1 +827 x2 +60 x3 +141 x4 +731 x5 +37 x6 +618 x7 +50 x8 +861 x9 +906
x10 +724 x11 +641 x12 +537 x13 +374 x14 +727 x15 +476 x16 +854 x17
+205 x18 +785 x19 +720 x20 +373 x21 +964 x22 +97 x23 +931 x24 +887 x25
+622 x26 +837 x27 +916 x28 +553 x29 +675 x30 +134 x31 +625 x32 +271
x33 +677 x34 +297 x35 +942 x36 +78 x37 +952 x38 +792 x39 +768 x40 +683
x41 +132 x42 +82 x43 +665 x44 +168 x45 +407 x46 +652 x47 +193 x48 +239
x49 +416 x50 +412 x51 +251 x52 +39 x53 +886 x54 +349 x55 +294 x56 +664
x57 +496 x58 +426 x59 +539 x60 +137 x61 +103 x62 +514 x63 +864 x64
+204 x65 +69 x66 +395 x67 +887 x68 +271 x69 +820 x70 +476 x71 +634 x72
+271 x73 +887 x74 +151 x75 +69 x76 +596 x77 +140 x78 +514 x79 +657 x80
+799 x81 +539 x82 +903 x83 +496 x84 +664 x85 +382 x86 +349 x87 +886
x88 +284 x89 +225 x90 +39 x91 +416 x92 +771 x93 +193 x94 +652 x95 +957
x96 +168 x97 +90 x98 +300 x99 +785 x100 +902 x101 +181 x102 +168 x103
+746 x104 +78 x105 +942 x106 +697 x107 +235 x108 +271 x109 +625 x110
+315 x111 +675 x112 +553 x113 +64 x114 +370 x115 +622 x116 +947 x117
+653 x118 +516 x119 +908 x120 +781 x121 +890 x122 +441 x123 +458 x124
+701 x125 +57 x126 +55 x127 +726 x128 +610 x129 +930 x130 +745 x131
+904 x132 +861 x133 +50 x134 +618 x135 +37 x136 +731 x137 +141 x138
+60 x139 +827 x140 +1 x141 -967 x214 -1934 x215 -3868 x216 -7736 x217
-15472 x218 -30944 x219 -61888 x220 -123776 x221 = 0;
1 x1 +813 x2 +200 x3 +330 x4 +610 x5 +562 x6 +697 x7 +544 x8 +486 x9
+492 x10 +438 x11 +427 x12 +872 x13 +6 x14 +40 x15 +230 x16 +832 x17
+883 x18 +666 x19 +399 x20 +907 x21 +948 x22 +732 x23 +107 x24 +493
x25 +752 x26 +944 x27 +329 x28 +582 x29 +97 x30 +594 x31 +504 x32 +490
x33 +895 x34 +136 x35 +695 x36 +896 x37 +243 x38 +21 x39 +309 x40 +898
x41 +155 x42 +637 x43 +596 x44 +705 x45 +89 x46 +673 x47 +304 x48 +524
x49 +436 x50 +860 x51 +925 x52 +750 x53 +575 x54 +282 x55 +803 x56
+918 x57 +545 x58 +485 x59 +213 x60 +661 x61 +343 x62 +259 x63 +453
x64 +224 x65 +161 x66 +30 x67 +76 x68 +504 x69 +451 x70 +47 x71 +891
x72 +504 x73 +76 x74 +13 x75 +161 x76 +575 x77 +820 x78 +259 x79 +720
x80 +222 x81 +213 x82 +136 x83 +545 x84 +918 x85 +447 x86 +282 x87
+575 x88 +945 x89 +49 x90 +942 x91 +436 x92 +331 x93 +304 x94 +673 x95
+184 x96 +705 x97 +819 x98 +539 x99 +849 x100 +532 x101 +663 x102 +660
x103 +518 x104 +896 x105 +695 x106 +254 x107 +255 x108 +490 x109 +504
x110 +491 x111 +97 x112 +582 x113 +169 x114 +150 x115 +752 x116 +382
x117 +897 x118 +49 x119 +803 x120 +796 x121 +591 x122 +102 x123 +752
x124 +292 x125 +11 x126 +712 x127 +863 x128 +6 x129 +716 x130 +459
x131 +490 x132 +486 x133 +544 x134 +697 x135 +562 x136 +610 x137 +330
x138 +200 x139 +813 x140 +1 x141 -953 x222 -1906 x223 -3812 x224 -7624
x225 -15248 x226 -30496 x227 -60992 x228 -121984 x229 = 0;
1 x1 +807 x2 +260 x3 +351 x4 +526 x5 +466 x6 +879 x7 +490 x8 +140 x9
+468 x10 +141 x11 +374 x12 +718 x13 +210 x14 +345 x15 +16 x16 +439 x17
+875 x18 +349 x19 +778 x20 +222 x21 +101 x22 +19 x23 +412 x24 +108 x25
+134 x26 +897 x27 +497 x28 +773 x29 +920 x30 +462 x31 +762 x32 +522
x33 +889 x34 +772 x35 +472 x36 +389 x37 +532 x38 +92 x39 +135 x40 +298
x41 +774 x42 +774 x43 +361 x44 +887 x45 +606 x46 +922 x47 +121 x48
+545 x49 +804 x50 +786 x51 +334 x52 +340 x53 +535 x54 +288 x55 +118
x56 +630 x57 +238 x58 +497 x59 +716 x60 +303 x61 +739 x62 +934 x63
+556 x64 +530 x65 +888 x66 +588 x67 +363 x68 +589 x69 +70 x70 +599 x71
+751 x72 +589 x73 +363 x74 +102 x75 +888 x76 +111 x77 +307 x78 +934
x79 +459 x80 +137 x81 +716 x82 +800 x83 +238 x84 +630 x85 +272 x86
+288 x87 +535 x88 +663 x89 +116 x90 +410 x91 +804 x92 +824 x93 +121
x94 +922 x95 +49 x96 +887 x97 +547 x98 +705 x99 +211 x100 +914 x101
+129 x102 +116 x103 +518 x104 +389 x105 +472 x106 +516 x107 +348 x108
+522 x109 +762 x110 +467 x111 +920 x112 +773 x113 +847 x114 +869 x115
+134 x116 +264 x117 +945 x118 +608 x119 +372 x120 +665 x121 +568 x122
+460 x123 +498 x124 +395 x125 +946 x126 +646 x127 +869 x128 +811 x129
+663 x130 +162 x131 +466 x132 +140 x133 +490 x134 +879 x135 +466 x136
+526 x137 +351 x138 +260 x139 +807 x140 +1 x141 -947 x230 -1894 x231
-3788 x232 -7576 x233 -15152 x234 -30304 x235 -60608 x236 -121216
x237 = 0;
1 x1 +801 x2 +320 x3 +336 x4 +725 x5 +41 x6 +489 x7 +318 x8 +124 x9
+373 x10 +499 x11 +495 x12 +114 x13 +806 x14 +929 x15 +508 x16 +552
x17 +254 x18 +333 x19 +521 x20 +527 x21 +402 x22 +176 x23 +570 x24
+727 x25 +668 x26 +293 x27 +921 x28 +889 x29 +664 x30 +309 x31 +143
x32 +593 x33 +89 x34 +40 x35 +903 x36 +404 x37 +186 x38 +252 x39 +595
x40 +95 x41 +939 x42 +900 x43 +531 x44 +916 x45 +342 x46 +859 x47 +125
x48 +624 x49 +4 x50 +386 x51 +557 x52 +375 x53 +818 x54 +831 x55 +799
x56 +626 x57 +109 x58 +901 x59 +813 x60 +210 x61 +154 x62 +210 x63
+419 x64 +539 x65 +853 x66 +722 x67 +844 x68 +877 x69 +97 x70 +61 x71
+58 x72 +877 x73 +844 x74 +908 x75 +853 x76 +844 x77 +622 x78 +210 x79
+919 x80 +5 x81 +813 x82 +268 x83 +109 x84 +626 x85 +153 x86 +831 x87
+818 x88 +367 x89 +402 x90 +49 x91 +4 x92 +725 x93 +125 x94 +859 x95
+237 x96 +916 x97 +576 x98 +319 x99 +900 x100 +674 x101 +617 x102 +426
x103 +420 x104 +404 x105 +903 x106 +26 x107 +833 x108 +593 x109 +143
x110 +50 x111 +664 x112 +889 x113 +836 x114 +880 x115 +668 x116 +572
x117 +487 x118 +260 x119 +542 x120 +589 x121 +390 x122 +737 x123 +723
x124 +543 x125 +597 x126 +871 x127 +326 x128 +213 x129 +784 x130 +520
x131 +371 x132 +124 x133 +318 x134 +489 x135 +41 x136 +725 x137 +336
x138 +320 x139 +801 x140 +1 x141 -941 x238 -1882 x239 -3764 x240 -7528
x241 -15056 x242 -30112 x243 -60224 x244 -120448 x245 = 0;
1 x1 +797 x2 +360 x3 +306 x4 +295 x5 +409 x6 +636 x7 +140 x8 +15 x9
+713 x10 +145 x11 +53 x12 +640 x13 +97 x14 +516 x15 +267 x16 +184 x17
+447 x18 +144 x19 +716 x20 +779 x21 +843 x22 +315 x23 +778 x24 +673
x25 +200 x26 +465 x27 +255 x28 +178 x29 +16 x30 +410 x31 +500 x32 +219
x33 +425 x34 +772 x35 +361 x36 +699 x37 +329 x38 +278 x39 +20 x40 +755
x41 +472 x42 +763 x43 +159 x44 +342 x45 +222 x46 +83 x47 +149 x48 +511
x49 +922 x50 +99 x51 +878 x52 +246 x53 +769 x54 +727 x55 +813 x56 +567
x57 +132 x58 +322 x59 +345 x60 +468 x61 +498 x62 +199 x63 +647 x64
+786 x65 +230 x66 +474 x67 +608 x68 +361 x69 +823 x70 +846 x71 +431
x72 +361 x73 +608 x74 +832 x75 +230 x76 +686 x77 +872 x78 +199 x79
+693 x80 +882 x81 +345 x82 +698 x83 +132 x84 +567 x85 +841 x86 +727
x87 +769 x88 +835 x89 +154 x90 +425 x91 +922 x92 +736 x93 +149 x94 +83
x95 +133 x96 +342 x97 +225 x98 +276 x99 +94 x100 +56 x101 +602 x102
+840 x103 +242 x104 +699 x105 +361 x106 +839 x107 +822 x108 +219 x109
+500 x110 +130 x111 +16 x112 +178 x113 +455 x114 +167 x115 +200 x116
+604 x117 +837 x118 +98 x119 +725 x120 +230 x121 +253 x122 +554 x123
+7 x124 +784 x125 +61 x126 +850 x127 +426 x128 +743 x129 +342 x130
+166 x131 +711 x132 +15 x133 +140 x134 +636 x135 +409 x136 +295 x137
+306 x138 +360 x139 +797 x140 +1 x141 -937 x246 -1874 x247 -3748 x248
-7496 x249 -14992 x250 -29984 x251 -59968 x252 -119936 x253 = 0;
1 x1 +789 x2 +440 x3 +198 x4 +186 x5 +329 x6 +494 x7 +497 x8 +679 x9
+566 x10 +39 x11 +111 x12 +499 x13 +376 x14 +413 x15 +402 x16 +333 x17
+847 x18 +75 x19 +452 x20 +643 x21 +273 x22 +51 x23 +731 x24 +671 x25
+750 x26 +593 x27 +131 x28 +640 x29 +621 x30 +592 x31 +353 x32 +619
x33 +819 x34 +799 x35 +436 x36 +318 x37 +758 x38 +298 x39 +596 x40
+128 x41 +613 x42 +572 x43 +853 x44 +675 x45 +165 x46 +460 x47 +844
x48 +577 x49 +137 x50 +606 x51 +747 x52 +54 x53 +620 x54 +831 x55 +475
x56 +722 x57 +364 x58 +734 x59 +326 x60 +472 x61 +257 x62 +783 x63
+787 x64 +902 x65 +668 x66 +375 x67 +28 x68 +203 x69 +778 x70 +59 x71
+615 x72 +203 x73 +28 x74 +84 x75 +668 x76 +909 x77 +449 x78 +783 x79
+14 x80 +731 x81 +326 x82 +530 x83 +364 x84 +722 x85 +218 x86 +831 x87
+620 x88 +797 x89 +809 x90 +915 x91 +137 x92 +404 x93 +844 x94 +460
x95 +724 x96 +675 x97 +347 x98 +57 x99 +658 x100 +309 x101 +788 x102
+475 x103 +269 x104 +318 x105 +436 x106 +242 x107 +209 x108 +619 x109
+353 x110 +455 x111 +621 x112 +640 x113 +868 x114 +864 x115 +750 x116
+757 x117 +477 x118 +337 x119 +449 x120 +250 x121 +56 x122 +862 x123
+645 x124 +12 x125 +415 x126 +602 x127 +441 x128 +610 x129 +400 x130
+60 x131 +564 x132 +679 x133 +497 x134 +494 x135 +329 x136 +186 x137
+198 x138 +440 x139 +789 x140 +1 x141 -929 x254 -1858 x255 -3716 x256
-7432 x257 -14864 x258 -29728 x259 -59456 x260 -118912 x261 = 0;
1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1
x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1
x22 +1 x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 +1 x30 +1 x31 +1
x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1
x32 +1 x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1
x42 +1 x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 +1 x51 +1
x52 +1 x53 +1 x54 +1 x55 +1 x56 +1 x57 +1 x58 +1 x59 +1 x60 +1 x61 +1
x62 +1 x63 +1 x64 +1 x65 +1 x66 +1 x67 +1 x68 +1 x69 +1 x70 +1 x71 +1
x72 +1 x73 +1 x74 +1 x75 +1 x76 +1 x77 +1 x78 +1 x79 +1 x80 +1 x81 +1
x82 +1 x83 +1 x84 +1 x85 +1 x86 +1 x87 +1 x88 +1 x89 +1 x90 +1 x91 +1
x92 +1 x93 +1 x94 +1 x95 +1 x96 +1 x97 +1 x98 +1 x99 +1 x100 +1 x101
+1 x102 +1 x103 +1 x104 +1 x105 +1 x106 +1 x107 +1 x108 +1 x109 +1
x110 +1 x111 +1 x112 +1 x113 +1 x114 +1 x115 +1 x116 +1 x117 +1 x118
+1 x119 +1 x120 +1 x121 +1 x122 +1 x123 +1 x124 +1 x125 +1 x126 +1
x127 +1 x128 +1 x129 +1 x130 +1 x131 +1 x132 +1 x133 +1 x134 +1 x135
+1 x136 +1 x137 +1 x138 +1 x139 +1 x140 +1 x141 >= 1;
1 x1 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1 x12 +1
x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1
x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 +1 x30 +1 x31 +1 x32 +1
x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1
x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1 x42 +1
x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 +1 x51 +1 x52 +1
x53 +1 x54 +1 x55 +1 x56 +1 x57 +1 x58 +1 x59 +1 x60 +1 x61 +1 x62 +1
x63 +1 x64 +1 x65 +1 x66 +1 x67 +1 x68 +1 x69 +1 x70 +1 x71 +1 x72 +1
x73 +1 x74 +1 x75 +1 x76 +1 x77 +1 x78 +1 x79 +1 x80 +1 x81 +1 x82 +1
x83 +1 x84 +1 x85 +1 x86 +1 x87 +1 x88 +1 x89 +1 x90 +1 x91 +1 x92 +1
x93 +1 x94 +1 x95 +1 x96 +1 x97 +1 x98 +1 x99 +1 x100 +1 x101 +1 x102
+1 x103 +1 x104 +1 x105 +1 x106 +1 x107 +1 x108 +1 x109 +1 x110 +1
x111 +1 x112 +1 x113 +1 x114 +1 x115 +1 x116 +1 x117 +1 x118 +1 x119
+1 x120 +1 x121 +1 x122 +1 x123 +1 x124 +1 x125 +1 x126 +1 x127 +1
x128 +1 x129 +1 x130 +1 x131 +1 x132 +1 x133 +1 x134 +1 x135 +1 x136
+1 x137 +1 x138 +1 x139 +1 x140 +1 x141 <= 139 ;
Raphael
Niklas Sörensson
Jun 14, 2011, 7:57:07 AM6/14/11
to min...@googlegroups.com
Hello,
On Tue, Jun 14, 2011 at 1:39 PM, lesshaste <drr...@gmail.com> wrote:
> Hi,
>
>> Ok, two comments.
>>
>> First, the CNF-generation of MiniSat+ is know to be buggy (this
>> feature was never tested much by us). I have started porting MiniSat+
>> to a newer MiniSat backend, and I *think* that might solve this
>> problem. If you'd like to try it out, you can download the source here
>> (choose the "next" branch!):
>>
>> https://github.com/niklasso/minisatp
>>
>> You'll need to also download the source to MiniSat separately:
>>
>> https://github.com/niklasso/minisat
>>
>
> Thanks! The addition of bignum support is a huge help and means I
> don't have to split the equality constraint up any more using the
> Chinese Remainder Theorem and converting the added integer variable to
> binary ones. The upshot is that I now have only 3 constraints but with
> big coefficients in one of them.
Bignum support has been there from the beginning, but it was possible
to compile without it. Maybe that was what you did.
Anyway, do you mind explaining how you split the constraints? This
sounds like something that MiniSat+ should be doing itself :)
>> Secondly, and maybe more importantly, even though generating
>> constraints via adders produces smaller CNFs, the performance is
>> usually very very bad. The adder method is really a last resort, that
>> sometimes works even if performance is bad. For instance, when I tried
>> to repeat your issue with the problem you posted, MiniSat simply
>> didn't terminate within 15 minutes.
>>
>> Is it possible to send an example of the real OPB-problem that you'd
>> like to solve? Then I can take a look myself and maybe come up with
>> some recommendation.
>>
>
> Sure. Here is the original formulation for one large problem with
> large coefficients.
Can you resend them as attachments? They were messed up by the email-program.
Thanks,
/Niklas
Reply all
Reply to author
Forward
0 new messages