File: bug-1.opb

package info (click to toggle)
sat4j 2.3.5-0.3
  • links: PTS
  • area: main
  • in suites: bookworm, bullseye, buster, sid, trixie
  • size: 90,260 kB
  • sloc: java: 50,309; xml: 1,491; lisp: 95; makefile: 36; sh: 35
file content (46 lines) | stat: -rw-r--r-- 4,218 bytes parent folder | download | duplicates (5)
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
* #variable= 89 #constraint= 39
****************************************
* begin normalizer comments
* category= OPT-BIGINT
* end normalizer comments
****************************************
min: +1 x59 +2 x60 +4 x61 +8 x62 +16 x63 +32 x64 +64 x65 +128 x66 +256 x67 +512 x68 +1024 x69 +2048 x70 +4096 x71 +8192 x72 +16384 x73 +32768 x74 +65536 x75 +131072 x76 +262144 x77 +524288 x78 +1048576 x79 +2097152 x80 +4194304 x81 +8388608 x82 +16777216 x83 +33554432 x84 +67108864 x85 +134217728 x86 +268435456 x87 +536870912 x88 +1073741824 x89 ;
-112640 x3 -112640 x4 -481280 x5 -481280 x6 -256000 x7 -256000 x8 -209920 x9 -209920 x10 -112640 x11 -112640 x12 -486400 x15 -486400 x16 -322560 x17 -322560 x18 -143360 x19 -143360 x20 -481280 x21 -481280 x22 -486400 x23 -486400 x24 -296960 x27 -296960 x28 -363520 x29 -363520 x30 -256000 x31 -256000 x32 -322560 x33 -322560 x34 -296960 x35 -296960 x36 -291840 x39 -291840 x40 -209920 x41 -209920 x42 -143360 x43 -143360 x44 -363520 x45 -363520 x46 -291840 x47 -291840 x48 -307200 x51 -307200 x52 -76800 x53 -76800 x54 -76800 x55 -76800 x56 -76800 x57 -76800 x58 +1 x59 +2 x60 +4 x61 +8 x62 +16 x63 +32 x64 +64 x65 +128 x66 +256 x67 +512 x68 +1024 x69 +2048 x70 +4096 x71 +8192 x72 +16384 x73 +32768 x74 +65536 x75 +131072 x76 +262144 x77 +524288 x78 +1048576 x79 +2097152 x80 +4194304 x81 +8388608 x82 +16777216 x83 +33554432 x84 +67108864 x85 +134217728 x86 +268435456 x87 +536870912 x88 +1073741824 x89 = 1073740800 ;
+1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 = 1 ;
+1 x11 +1 x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 = 1 ;
+1 x21 +1 x22 +1 x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 +1 x30 = 1 ;
-1 x1 -1 x3 -1 x5 -1 x7 -1 x9 -1 x11 -1 x13 -1 x15 -1 x17 -1 x19 -1 x21 -1 x23 -1 x25 -1 x27 -1 x29 >= -2 ;
-1 x2 -1 x4 -1 x6 -1 x8 -1 x10 -1 x12 -1 x14 -1 x16 -1 x18 -1 x20 -1 x22 -1 x24 -1 x26 -1 x28 -1 x30 >= -2 ;
+1 x3 +1 x4 +1 x5 +1 x6 +1 x33 +1 x34 +1 x35 +1 x36 +1 x43 +1 x44 +1 x45 +1 x46 >= 1 ;
+1 x11 +1 x12 +1 x15 +1 x16 +1 x31 +1 x32 +1 x35 +1 x36 +1 x41 +1 x42 +1 x45 +1 x46 >= 1 ;
+1 x5 +1 x6 +1 x15 +1 x16 +1 x35 +1 x36 +1 x45 +1 x46 >= 1 ;
+1 x21 +1 x22 +1 x23 +1 x24 +1 x31 +1 x32 +1 x33 +1 x34 +1 x41 +1 x42 +1 x43 +1 x44 >= 1 ;
+1 x3 +1 x4 +1 x23 +1 x24 +1 x33 +1 x34 +1 x43 +1 x44 >= 1 ;
+1 x11 +1 x12 +1 x21 +1 x22 +1 x31 +1 x32 +1 x41 +1 x42 >= 1 ;
+1 x31 +1 x32 +1 x33 +1 x34 +1 x35 +1 x36 +1 x41 +1 x42 +1 x43 +1 x44 +1 x45 +1 x46 >= 1 ;
+1 x3 +1 x5 +1 x7 +1 x9 -1 x11 -1 x21 -1 x31 -1 x41 = 0 ;
-1 x3 +1 x11 +1 x15 +1 x17 +1 x19 -1 x23 -1 x33 -1 x43 = 0 ;
-1 x5 -1 x15 +1 x21 +1 x23 +1 x27 +1 x29 -1 x35 -1 x45 = 0 ;
-1 x7 -1 x17 -1 x27 +1 x31 +1 x33 +1 x35 +1 x39 -1 x47 = 0 ;
-1 x9 -1 x19 -1 x29 -1 x39 +1 x41 +1 x43 +1 x45 +1 x47 = 0 ;
+1 x4 +1 x6 +1 x8 +1 x10 -1 x12 -1 x22 -1 x32 -1 x42 = 0 ;
-1 x4 +1 x12 +1 x16 +1 x18 +1 x20 -1 x24 -1 x34 -1 x44 = 0 ;
-1 x6 -1 x16 +1 x22 +1 x24 +1 x28 +1 x30 -1 x36 -1 x46 = 0 ;
-1 x8 -1 x18 -1 x28 +1 x32 +1 x34 +1 x36 +1 x40 -1 x48 = 0 ;
-1 x10 -1 x20 -1 x30 -1 x40 +1 x42 +1 x44 +1 x46 +1 x48 = 0 ;
-1 x7 -1 x9 -1 x17 -1 x19 -1 x27 -1 x29 >= -1 ;
-1 x8 -1 x10 -1 x18 -1 x20 -1 x28 -1 x30 >= -1 ;
+3 x51 -1 x53 -1 x55 -1 x57 >= 0 ;
+3 x52 -1 x54 -1 x56 -1 x58 >= 0 ;
-1 x1 -1 x3 -1 x5 -1 x7 -1 x9 -1 x31 -1 x33 -1 x35 -1 x37 -1 x39 +1 x53 >= -1 ;
-1 x2 -1 x4 -1 x6 -1 x8 -1 x10 -1 x32 -1 x34 -1 x36 -1 x38 -1 x40 +1 x53 >= -1 ;
-1 x1 -1 x3 -1 x5 -1 x7 -1 x9 -1 x41 -1 x43 -1 x45 -1 x47 -1 x49 +1 x54 >= -1 ;
-1 x2 -1 x4 -1 x6 -1 x8 -1 x10 -1 x42 -1 x44 -1 x46 -1 x48 -1 x50 +1 x54 >= -1 ;
-1 x11 -1 x13 -1 x15 -1 x17 -1 x19 -1 x31 -1 x33 -1 x35 -1 x37 -1 x39 +1 x55 >= -1 ;
-1 x12 -1 x14 -1 x16 -1 x18 -1 x20 -1 x32 -1 x34 -1 x36 -1 x38 -1 x40 +1 x55 >= -1 ;
-1 x11 -1 x13 -1 x15 -1 x17 -1 x19 -1 x41 -1 x43 -1 x45 -1 x47 -1 x49 +1 x56 >= -1 ;
-1 x12 -1 x14 -1 x16 -1 x18 -1 x20 -1 x42 -1 x44 -1 x46 -1 x48 -1 x50 +1 x56 >= -1 ;
-1 x21 -1 x23 -1 x25 -1 x27 -1 x29 -1 x31 -1 x33 -1 x35 -1 x37 -1 x39 +1 x57 >= -1 ;
-1 x22 -1 x24 -1 x26 -1 x28 -1 x30 -1 x32 -1 x34 -1 x36 -1 x38 -1 x40 +1 x57 >= -1 ;
-1 x21 -1 x23 -1 x25 -1 x27 -1 x29 -1 x41 -1 x43 -1 x45 -1 x47 -1 x49 +1 x58 >= -1 ;
-1 x22 -1 x24 -1 x26 -1 x28 -1 x30 -1 x42 -1 x44 -1 x46 -1 x48 -1 x50 +1 x58 >= -1 ;