c Standarized MaxSat Instance c{ c "sha1sum": "aaaceccf587d72159aa14a8aed5e4d8185ccaf7d", c "nvars": 70, c "ncls": 630, c "nhards": 560, c "nhard_len_stats": c { "min": 2, "max": 2, "ave": 2.00, c "stddev": 0.00 }, c "nsofts": 70, c "nsoft_len_stats": c { "min": 1, "max": 1, "ave": 1.00, c "stddev": 0.00 }, c "nsoft_wts": 1, c "soft_wt_stats": c { "min": 1, "max": 1, "ave": 1.00, c "stddev": 0.00 } c} c------------------------------------------------------------ c File: johnson8-4-4.clq c c Source: Panos Pardalos pardalos@math.ufl.edu c c Reference: Johnson graph: johnsona-b-c is generated by c binary vectors of length a and weight b, with c two vertices adjacent if the hamming distance c between them is at least d. c c PSEUDOBOOLEAN 70 p wcnf 70 630 71 1 -1 0 1 -2 0 1 -3 0 1 -4 0 1 -5 0 1 -6 0 1 -7 0 1 -8 0 1 -9 0 1 -10 0 1 -11 0 1 -12 0 1 -13 0 1 -14 0 1 -15 0 1 -16 0 1 -17 0 1 -18 0 1 -19 0 1 -20 0 1 -21 0 1 -22 0 1 -23 0 1 -24 0 1 -25 0 1 -26 0 1 -27 0 1 -28 0 1 -29 0 1 -30 0 1 -31 0 1 -32 0 1 -33 0 1 -34 0 1 -35 0 1 -36 0 1 -37 0 1 -38 0 1 -39 0 1 -40 0 1 -41 0 1 -42 0 1 -43 0 1 -44 0 1 -45 0 1 -46 0 1 -47 0 1 -48 0 1 -49 0 1 -50 0 1 -51 0 1 -52 0 1 -53 0 1 -54 0 1 -55 0 1 -56 0 1 -57 0 1 -58 0 1 -59 0 1 -60 0 1 -61 0 1 -62 0 1 -63 0 1 -64 0 1 -65 0 1 -66 0 1 -67 0 1 -68 0 1 -69 0 1 -70 0 71 1 2 0 71 1 3 0 71 1 4 0 71 1 5 0 71 1 6 0 71 1 7 0 71 1 8 0 71 1 9 0 71 1 16 0 71 1 17 0 71 1 18 0 71 1 19 0 71 1 36 0 71 1 37 0 71 1 38 0 71 1 39 0 71 2 3 0 71 2 4 0 71 2 5 0 71 2 6 0 71 2 10 0 71 2 11 0 71 2 12 0 71 2 16 0 71 2 20 0 71 2 21 0 71 2 22 0 71 2 36 0 71 2 40 0 71 2 41 0 71 2 42 0 71 3 4 0 71 3 5 0 71 3 7 0 71 3 10 0 71 3 13 0 71 3 14 0 71 3 17 0 71 3 20 0 71 3 23 0 71 3 24 0 71 3 37 0 71 3 40 0 71 3 43 0 71 3 44 0 71 4 5 0 71 4 8 0 71 4 11 0 71 4 13 0 71 4 15 0 71 4 18 0 71 4 21 0 71 4 23 0 71 4 25 0 71 4 38 0 71 4 41 0 71 4 43 0 71 4 45 0 71 5 9 0 71 5 12 0 71 5 14 0 71 5 15 0 71 5 19 0 71 5 22 0 71 5 24 0 71 5 25 0 71 5 39 0 71 5 42 0 71 5 44 0 71 5 45 0 71 6 7 0 71 6 8 0 71 6 9 0 71 6 10 0 71 6 11 0 71 6 12 0 71 6 16 0 71 6 26 0 71 6 27 0 71 6 28 0 71 6 36 0 71 6 46 0 71 6 47 0 71 6 48 0 71 7 8 0 71 7 9 0 71 7 10 0 71 7 13 0 71 7 14 0 71 7 17 0 71 7 26 0 71 7 29 0 71 7 30 0 71 7 37 0 71 7 46 0 71 7 49 0 71 7 50 0 71 8 9 0 71 8 11 0 71 8 13 0 71 8 15 0 71 8 18 0 71 8 27 0 71 8 29 0 71 8 31 0 71 8 38 0 71 8 47 0 71 8 49 0 71 8 51 0 71 9 12 0 71 9 14 0 71 9 15 0 71 9 19 0 71 9 28 0 71 9 30 0 71 9 31 0 71 9 39 0 71 9 48 0 71 9 50 0 71 9 51 0 71 10 11 0 71 10 12 0 71 10 13 0 71 10 14 0 71 10 20 0 71 10 26 0 71 10 32 0 71 10 33 0 71 10 40 0 71 10 46 0 71 10 52 0 71 10 53 0 71 11 12 0 71 11 13 0 71 11 15 0 71 11 21 0 71 11 27 0 71 11 32 0 71 11 34 0 71 11 41 0 71 11 47 0 71 11 52 0 71 11 54 0 71 12 14 0 71 12 15 0 71 12 22 0 71 12 28 0 71 12 33 0 71 12 34 0 71 12 42 0 71 12 48 0 71 12 53 0 71 12 54 0 71 13 14 0 71 13 15 0 71 13 23 0 71 13 29 0 71 13 32 0 71 13 35 0 71 13 43 0 71 13 49 0 71 13 52 0 71 13 55 0 71 14 15 0 71 14 24 0 71 14 30 0 71 14 33 0 71 14 35 0 71 14 44 0 71 14 50 0 71 14 53 0 71 14 55 0 71 15 25 0 71 15 31 0 71 15 34 0 71 15 35 0 71 15 45 0 71 15 51 0 71 15 54 0 71 15 55 0 71 16 17 0 71 16 18 0 71 16 19 0 71 16 20 0 71 16 21 0 71 16 22 0 71 16 26 0 71 16 27 0 71 16 28 0 71 16 36 0 71 16 56 0 71 16 57 0 71 16 58 0 71 17 18 0 71 17 19 0 71 17 20 0 71 17 23 0 71 17 24 0 71 17 26 0 71 17 29 0 71 17 30 0 71 17 37 0 71 17 56 0 71 17 59 0 71 17 60 0 71 18 19 0 71 18 21 0 71 18 23 0 71 18 25 0 71 18 27 0 71 18 29 0 71 18 31 0 71 18 38 0 71 18 57 0 71 18 59 0 71 18 61 0 71 19 22 0 71 19 24 0 71 19 25 0 71 19 28 0 71 19 30 0 71 19 31 0 71 19 39 0 71 19 58 0 71 19 60 0 71 19 61 0 71 20 21 0 71 20 22 0 71 20 23 0 71 20 24 0 71 20 26 0 71 20 32 0 71 20 33 0 71 20 40 0 71 20 56 0 71 20 62 0 71 20 63 0 71 21 22 0 71 21 23 0 71 21 25 0 71 21 27 0 71 21 32 0 71 21 34 0 71 21 41 0 71 21 57 0 71 21 62 0 71 21 64 0 71 22 24 0 71 22 25 0 71 22 28 0 71 22 33 0 71 22 34 0 71 22 42 0 71 22 58 0 71 22 63 0 71 22 64 0 71 23 24 0 71 23 25 0 71 23 29 0 71 23 32 0 71 23 35 0 71 23 43 0 71 23 59 0 71 23 62 0 71 23 65 0 71 24 25 0 71 24 30 0 71 24 33 0 71 24 35 0 71 24 44 0 71 24 60 0 71 24 63 0 71 24 65 0 71 25 31 0 71 25 34 0 71 25 35 0 71 25 45 0 71 25 61 0 71 25 64 0 71 25 65 0 71 26 27 0 71 26 28 0 71 26 29 0 71 26 30 0 71 26 32 0 71 26 33 0 71 26 46 0 71 26 56 0 71 26 66 0 71 26 67 0 71 27 28 0 71 27 29 0 71 27 31 0 71 27 32 0 71 27 34 0 71 27 47 0 71 27 57 0 71 27 66 0 71 27 68 0 71 28 30 0 71 28 31 0 71 28 33 0 71 28 34 0 71 28 48 0 71 28 58 0 71 28 67 0 71 28 68 0 71 29 30 0 71 29 31 0 71 29 32 0 71 29 35 0 71 29 49 0 71 29 59 0 71 29 66 0 71 29 69 0 71 30 31 0 71 30 33 0 71 30 35 0 71 30 50 0 71 30 60 0 71 30 67 0 71 30 69 0 71 31 34 0 71 31 35 0 71 31 51 0 71 31 61 0 71 31 68 0 71 31 69 0 71 32 33 0 71 32 34 0 71 32 35 0 71 32 52 0 71 32 62 0 71 32 66 0 71 32 70 0 71 33 34 0 71 33 35 0 71 33 53 0 71 33 63 0 71 33 67 0 71 33 70 0 71 34 35 0 71 34 54 0 71 34 64 0 71 34 68 0 71 34 70 0 71 35 55 0 71 35 65 0 71 35 69 0 71 35 70 0 71 36 37 0 71 36 38 0 71 36 39 0 71 36 40 0 71 36 41 0 71 36 42 0 71 36 46 0 71 36 47 0 71 36 48 0 71 36 56 0 71 36 57 0 71 36 58 0 71 37 38 0 71 37 39 0 71 37 40 0 71 37 43 0 71 37 44 0 71 37 46 0 71 37 49 0 71 37 50 0 71 37 56 0 71 37 59 0 71 37 60 0 71 38 39 0 71 38 41 0 71 38 43 0 71 38 45 0 71 38 47 0 71 38 49 0 71 38 51 0 71 38 57 0 71 38 59 0 71 38 61 0 71 39 42 0 71 39 44 0 71 39 45 0 71 39 48 0 71 39 50 0 71 39 51 0 71 39 58 0 71 39 60 0 71 39 61 0 71 40 41 0 71 40 42 0 71 40 43 0 71 40 44 0 71 40 46 0 71 40 52 0 71 40 53 0 71 40 56 0 71 40 62 0 71 40 63 0 71 41 42 0 71 41 43 0 71 41 45 0 71 41 47 0 71 41 52 0 71 41 54 0 71 41 57 0 71 41 62 0 71 41 64 0 71 42 44 0 71 42 45 0 71 42 48 0 71 42 53 0 71 42 54 0 71 42 58 0 71 42 63 0 71 42 64 0 71 43 44 0 71 43 45 0 71 43 49 0 71 43 52 0 71 43 55 0 71 43 59 0 71 43 62 0 71 43 65 0 71 44 45 0 71 44 50 0 71 44 53 0 71 44 55 0 71 44 60 0 71 44 63 0 71 44 65 0 71 45 51 0 71 45 54 0 71 45 55 0 71 45 61 0 71 45 64 0 71 45 65 0 71 46 47 0 71 46 48 0 71 46 49 0 71 46 50 0 71 46 52 0 71 46 53 0 71 46 56 0 71 46 66 0 71 46 67 0 71 47 48 0 71 47 49 0 71 47 51 0 71 47 52 0 71 47 54 0 71 47 57 0 71 47 66 0 71 47 68 0 71 48 50 0 71 48 51 0 71 48 53 0 71 48 54 0 71 48 58 0 71 48 67 0 71 48 68 0 71 49 50 0 71 49 51 0 71 49 52 0 71 49 55 0 71 49 59 0 71 49 66 0 71 49 69 0 71 50 51 0 71 50 53 0 71 50 55 0 71 50 60 0 71 50 67 0 71 50 69 0 71 51 54 0 71 51 55 0 71 51 61 0 71 51 68 0 71 51 69 0 71 52 53 0 71 52 54 0 71 52 55 0 71 52 62 0 71 52 66 0 71 52 70 0 71 53 54 0 71 53 55 0 71 53 63 0 71 53 67 0 71 53 70 0 71 54 55 0 71 54 64 0 71 54 68 0 71 54 70 0 71 55 65 0 71 55 69 0 71 55 70 0 71 56 57 0 71 56 58 0 71 56 59 0 71 56 60 0 71 56 62 0 71 56 63 0 71 56 66 0 71 56 67 0 71 57 58 0 71 57 59 0 71 57 61 0 71 57 62 0 71 57 64 0 71 57 66 0 71 57 68 0 71 58 60 0 71 58 61 0 71 58 63 0 71 58 64 0 71 58 67 0 71 58 68 0 71 59 60 0 71 59 61 0 71 59 62 0 71 59 65 0 71 59 66 0 71 59 69 0 71 60 61 0 71 60 63 0 71 60 65 0 71 60 67 0 71 60 69 0 71 61 64 0 71 61 65 0 71 61 68 0 71 61 69 0 71 62 63 0 71 62 64 0 71 62 65 0 71 62 66 0 71 62 70 0 71 63 64 0 71 63 65 0 71 63 67 0 71 63 70 0 71 64 65 0 71 64 68 0 71 64 70 0 71 65 69 0 71 65 70 0 71 66 67 0 71 66 68 0 71 66 69 0 71 66 70 0 71 67 68 0 71 67 69 0 71 67 70 0 71 68 69 0 71 68 70 0 71 69 70 0