mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
422 lines
11 KiB
INI
422 lines
11 KiB
INI
c File: pret150_25.cnf
|
|
c
|
|
c SOURCE: Daniel Pretolani (daniele@crt.umontreal.ca)
|
|
c
|
|
c DESCRIPTION: Unsatisfiable instances of a graph 2-coloring with
|
|
c parity constraints.
|
|
c
|
|
c ----------- DIMACS Challenge - CNF format -----------
|
|
c
|
|
c TRISAT Generator (Pretolani 1990)
|
|
c
|
|
c (Even) number of nodes ==> 100
|
|
c Charge ( 0 = sat. / 1 = unsat. ) ==> 1
|
|
c Horn Percentage (min -> 25; max -> 75) ==> 25
|
|
c Number of Propositional variables ==> 150
|
|
c Number of Clauses ==> 400
|
|
c Nodes with Charge = 1 ==> 1
|
|
c Horn Percentage (exact) ==> 24.000
|
|
c
|
|
c -----------------------------------------------------
|
|
p cnf 150 400
|
|
-3 -2 -1 0
|
|
3 2 -1 0
|
|
2 1 -3 0
|
|
3 1 -2 0
|
|
-6 -5 -4 0
|
|
6 5 -4 0
|
|
5 4 -6 0
|
|
6 4 -5 0
|
|
-9 -8 -7 0
|
|
9 8 -7 0
|
|
8 7 -9 0
|
|
9 7 -8 0
|
|
-12 -11 -10 0
|
|
12 11 -10 0
|
|
11 10 -12 0
|
|
12 10 -11 0
|
|
-15 -14 -13 0
|
|
15 14 -13 0
|
|
14 13 -15 0
|
|
15 13 -14 0
|
|
-18 -17 -16 0
|
|
18 17 -16 0
|
|
17 16 -18 0
|
|
18 16 -17 0
|
|
-21 -20 -19 0
|
|
21 20 -19 0
|
|
20 19 -21 0
|
|
21 19 -20 0
|
|
-24 -23 -22 0
|
|
24 23 -22 0
|
|
23 22 -24 0
|
|
24 22 -23 0
|
|
-27 -26 -25 0
|
|
27 26 -25 0
|
|
26 25 -27 0
|
|
27 25 -26 0
|
|
-30 -29 -28 0
|
|
30 29 -28 0
|
|
29 28 -30 0
|
|
30 28 -29 0
|
|
-33 -32 -31 0
|
|
33 32 -31 0
|
|
32 31 -33 0
|
|
33 31 -32 0
|
|
-36 -35 -34 0
|
|
36 35 -34 0
|
|
35 34 -36 0
|
|
36 34 -35 0
|
|
-39 -38 -37 0
|
|
39 38 -37 0
|
|
38 37 -39 0
|
|
39 37 -38 0
|
|
-42 -41 -40 0
|
|
42 41 -40 0
|
|
41 40 -42 0
|
|
42 40 -41 0
|
|
-45 -44 -43 0
|
|
45 44 -43 0
|
|
44 43 -45 0
|
|
45 43 -44 0
|
|
-48 -47 -46 0
|
|
48 47 -46 0
|
|
47 46 -48 0
|
|
48 46 -47 0
|
|
-51 -50 -49 0
|
|
51 50 -49 0
|
|
50 49 -51 0
|
|
51 49 -50 0
|
|
-54 -53 -52 0
|
|
54 53 -52 0
|
|
53 52 -54 0
|
|
54 52 -53 0
|
|
-57 -56 -55 0
|
|
57 56 -55 0
|
|
56 55 -57 0
|
|
57 55 -56 0
|
|
-60 -59 -58 0
|
|
60 59 -58 0
|
|
59 58 -60 0
|
|
60 58 -59 0
|
|
-63 -62 -61 0
|
|
63 62 -61 0
|
|
62 61 -63 0
|
|
63 61 -62 0
|
|
-66 -65 -64 0
|
|
66 65 -64 0
|
|
65 64 -66 0
|
|
66 64 -65 0
|
|
-69 -68 -67 0
|
|
69 68 -67 0
|
|
68 67 -69 0
|
|
69 67 -68 0
|
|
-72 -71 -70 0
|
|
72 71 -70 0
|
|
71 70 -72 0
|
|
72 70 -71 0
|
|
-75 -74 -73 0
|
|
75 74 -73 0
|
|
74 73 -75 0
|
|
75 73 -74 0
|
|
-78 -77 -76 0
|
|
78 77 -76 0
|
|
77 76 -78 0
|
|
78 76 -77 0
|
|
-81 -80 -79 0
|
|
81 80 -79 0
|
|
80 79 -81 0
|
|
81 79 -80 0
|
|
-84 -83 -82 0
|
|
84 83 -82 0
|
|
83 82 -84 0
|
|
84 82 -83 0
|
|
-87 -86 -85 0
|
|
87 86 -85 0
|
|
86 85 -87 0
|
|
87 85 -86 0
|
|
-90 -89 -88 0
|
|
90 89 -88 0
|
|
89 88 -90 0
|
|
90 88 -89 0
|
|
-93 -92 -91 0
|
|
93 92 -91 0
|
|
92 91 -93 0
|
|
93 91 -92 0
|
|
-96 -95 -94 0
|
|
96 95 -94 0
|
|
95 94 -96 0
|
|
96 94 -95 0
|
|
-99 -98 -97 0
|
|
99 98 -97 0
|
|
98 97 -99 0
|
|
99 97 -98 0
|
|
-101 -100 -97 0
|
|
101 100 -97 0
|
|
100 97 -101 0
|
|
101 97 -100 0
|
|
-102 -36 -7 0
|
|
102 36 -7 0
|
|
36 7 -102 0
|
|
102 7 -36 0
|
|
-102 -35 -31 0
|
|
102 35 -31 0
|
|
35 31 -102 0
|
|
102 31 -35 0
|
|
-104 -103 -3 0
|
|
104 103 -3 0
|
|
103 3 -104 0
|
|
104 3 -103 0
|
|
-103 -40 -2 0
|
|
103 40 -2 0
|
|
40 2 -103 0
|
|
103 2 -40 0
|
|
-106 -105 -39 0
|
|
106 105 -39 0
|
|
105 39 -106 0
|
|
106 39 -105 0
|
|
-105 -104 -38 0
|
|
105 104 -38 0
|
|
104 38 -105 0
|
|
105 38 -104 0
|
|
-107 -42 -16 0
|
|
107 42 -16 0
|
|
42 16 -107 0
|
|
107 16 -42 0
|
|
-107 -41 -37 0
|
|
107 41 -37 0
|
|
41 37 -107 0
|
|
107 37 -41 0
|
|
-109 -108 -15 0
|
|
109 108 -15 0
|
|
108 15 -109 0
|
|
109 15 -108 0
|
|
-108 -46 -14 0
|
|
108 46 -14 0
|
|
46 14 -108 0
|
|
108 14 -46 0
|
|
-111 -110 -45 0
|
|
111 110 -45 0
|
|
110 45 -111 0
|
|
111 45 -110 0
|
|
-110 -109 -44 0
|
|
110 109 -44 0
|
|
109 44 -110 0
|
|
110 44 -109 0
|
|
-112 -106 -48 0
|
|
112 106 -48 0
|
|
106 48 -112 0
|
|
112 48 -106 0
|
|
-112 -47 -43 0
|
|
112 47 -43 0
|
|
47 43 -112 0
|
|
112 43 -47 0
|
|
-114 -113 -18 0
|
|
114 113 -18 0
|
|
113 18 -114 0
|
|
114 18 -113 0
|
|
-113 -52 -17 0
|
|
113 52 -17 0
|
|
52 17 -113 0
|
|
113 17 -52 0
|
|
-115 -51 -10 0
|
|
115 51 -10 0
|
|
51 10 -115 0
|
|
115 10 -51 0
|
|
-115 -114 -50 0
|
|
115 114 -50 0
|
|
114 50 -115 0
|
|
115 50 -114 0
|
|
-116 -54 -13 0
|
|
116 54 -13 0
|
|
54 13 -116 0
|
|
116 13 -54 0
|
|
-116 -53 -49 0
|
|
116 53 -49 0
|
|
53 49 -116 0
|
|
116 49 -53 0
|
|
-118 -117 -6 0
|
|
118 117 -6 0
|
|
117 6 -118 0
|
|
118 6 -117 0
|
|
-117 -58 -5 0
|
|
117 58 -5 0
|
|
58 5 -117 0
|
|
117 5 -58 0
|
|
-120 -119 -57 0
|
|
120 119 -57 0
|
|
119 57 -120 0
|
|
120 57 -119 0
|
|
-119 -118 -56 0
|
|
119 118 -56 0
|
|
118 56 -119 0
|
|
119 56 -118 0
|
|
-121 -60 -22 0
|
|
121 60 -22 0
|
|
60 22 -121 0
|
|
121 22 -60 0
|
|
-121 -59 -55 0
|
|
121 59 -55 0
|
|
59 55 -121 0
|
|
121 55 -59 0
|
|
-123 -122 -21 0
|
|
123 122 -21 0
|
|
122 21 -123 0
|
|
123 21 -122 0
|
|
-122 -64 -20 0
|
|
122 64 -20 0
|
|
64 20 -122 0
|
|
122 20 -64 0
|
|
-125 -124 -63 0
|
|
125 124 -63 0
|
|
124 63 -125 0
|
|
125 63 -124 0
|
|
-124 -123 -62 0
|
|
124 123 -62 0
|
|
123 62 -124 0
|
|
124 62 -123 0
|
|
-126 -120 -66 0
|
|
126 120 -66 0
|
|
120 66 -126 0
|
|
126 66 -120 0
|
|
-126 -65 -61 0
|
|
126 65 -61 0
|
|
65 61 -126 0
|
|
126 61 -65 0
|
|
-128 -127 -24 0
|
|
128 127 -24 0
|
|
127 24 -128 0
|
|
128 24 -127 0
|
|
-127 -70 -23 0
|
|
127 70 -23 0
|
|
70 23 -127 0
|
|
127 23 -70 0
|
|
-129 -69 -1 0
|
|
129 69 -1 0
|
|
69 1 -129 0
|
|
129 1 -69 0
|
|
-129 -128 -68 0
|
|
129 128 -68 0
|
|
128 68 -129 0
|
|
129 68 -128 0
|
|
-130 -72 -19 0
|
|
130 72 -19 0
|
|
72 19 -130 0
|
|
130 19 -72 0
|
|
-130 -71 -67 0
|
|
130 71 -67 0
|
|
71 67 -130 0
|
|
130 67 -71 0
|
|
-132 -131 -9 0
|
|
132 131 -9 0
|
|
131 9 -132 0
|
|
132 9 -131 0
|
|
-131 -76 -8 0
|
|
131 76 -8 0
|
|
76 8 -131 0
|
|
131 8 -76 0
|
|
-134 -133 -75 0
|
|
134 133 -75 0
|
|
133 75 -134 0
|
|
134 75 -133 0
|
|
-133 -132 -74 0
|
|
133 132 -74 0
|
|
132 74 -133 0
|
|
133 74 -132 0
|
|
-135 -78 -28 0
|
|
135 78 -28 0
|
|
78 28 -135 0
|
|
135 28 -78 0
|
|
-135 -77 -73 0
|
|
135 77 -73 0
|
|
77 73 -135 0
|
|
135 73 -77 0
|
|
-137 -136 -27 0
|
|
137 136 -27 0
|
|
136 27 -137 0
|
|
137 27 -136 0
|
|
-136 -82 -26 0
|
|
136 82 -26 0
|
|
82 26 -136 0
|
|
136 26 -82 0
|
|
-138 -111 -81 0
|
|
138 111 -81 0
|
|
111 81 -138 0
|
|
138 81 -111 0
|
|
-138 -137 -80 0
|
|
138 137 -80 0
|
|
137 80 -138 0
|
|
138 80 -137 0
|
|
-139 -134 -84 0
|
|
139 134 -84 0
|
|
134 84 -139 0
|
|
139 84 -134 0
|
|
-139 -83 -79 0
|
|
139 83 -79 0
|
|
83 79 -139 0
|
|
139 79 -83 0
|
|
-141 -140 -30 0
|
|
141 140 -30 0
|
|
140 30 -141 0
|
|
141 30 -140 0
|
|
-140 -88 -29 0
|
|
140 88 -29 0
|
|
88 29 -140 0
|
|
140 29 -88 0
|
|
-142 -87 -4 0
|
|
142 87 -4 0
|
|
87 4 -142 0
|
|
142 4 -87 0
|
|
-142 -141 -86 0
|
|
142 141 -86 0
|
|
141 86 -142 0
|
|
142 86 -141 0
|
|
-143 -90 -25 0
|
|
143 90 -25 0
|
|
90 25 -143 0
|
|
143 25 -90 0
|
|
-143 -89 -85 0
|
|
143 89 -85 0
|
|
89 85 -143 0
|
|
143 85 -89 0
|
|
-145 -144 -12 0
|
|
145 144 -12 0
|
|
144 12 -145 0
|
|
145 12 -144 0
|
|
-144 -94 -11 0
|
|
144 94 -11 0
|
|
94 11 -144 0
|
|
144 11 -94 0
|
|
-146 -101 -93 0
|
|
146 101 -93 0
|
|
101 93 -146 0
|
|
146 93 -101 0
|
|
-146 -145 -92 0
|
|
146 145 -92 0
|
|
145 92 -146 0
|
|
146 92 -145 0
|
|
-147 -96 -34 0
|
|
147 96 -34 0
|
|
96 34 -147 0
|
|
147 34 -96 0
|
|
-147 -95 -91 0
|
|
147 95 -91 0
|
|
95 91 -147 0
|
|
147 91 -95 0
|
|
-149 -148 -33 0
|
|
149 148 -33 0
|
|
148 33 -149 0
|
|
149 33 -148 0
|
|
-148 -100 -32 0
|
|
148 100 -32 0
|
|
100 32 -148 0
|
|
148 32 -100 0
|
|
-150 -125 -99 0
|
|
150 125 -99 0
|
|
125 99 -150 0
|
|
150 99 -125 0
|
|
150 149 98 0
|
|
150 -149 -98 0
|
|
149 -150 -98 0
|
|
98 -150 -149 0
|
|
|