8 á) Demonstrative example:
In each of the following four explanatory samples showed below there
are:
1) Original CNF;
2) Received as a result of transformation supergiven CNF, equivalent
original;
3) Result of reduction CNF in the form DNF.
Equivalence is understood as identity of carrying out sets.
For CNF it is accepted:
P - variable,
S - inverted variable.
They stand after an index variable, each line is a disjunction.
For DNF it is accepted:
D - variable,
N - inverted variable.
They stand after an index variable, each line is a conjunction.
Now we will mark the following: if in original CNF the definition Satisfiability is a hard problem, for superreducten CNF if it in easier one. That means that in it the fact of Satisfiability is accepted as linear time from dimension n * m of the problem.
The comparison of the logic circuits realizing CNF and superreducten CNF, shows the advantage of Superreduction.
Strictly speaking, in practical activity the application of the programs Superreduction allows on a design stage by systems CAD (computer-aided design) to receive only easier of a task.
EXAMPLE N 1
I Original CNF:
0) 1P 3P 8S
1) 0P 12S 19P
2) 5P 9P 24S
3) 5P 26S 27S
4) 21P 22S 27S
5) 14P 17S 22P
6) 6S 8P 13P
7) 3P 23S 26P
8) 20S 23S 24P
9) 7P 25P 28S
10) 9S 13P 24S
11) 10S 16S 17P
12) 6S 12S 25P
13) 6S 12P 24P
14) 1S 11S 19P
15) 5P 13S 24P
16) 1S 9S 21S
17) 5S 23S 27S
18) 3S 4P 18P
19) 10P 26S 28S
20) 1P 23S 26P
21) 6P 10S 25S
22) 9S 12P 20S
23) 4P 5P 25P
24) 6P 9P 13P
25) 3P 5S 13P
26) 3S 23P 29P
27) 16P 26S 28S
28) 6P 7S 17P
29) 14S 23S 28P
30) 15P 26P 29P
31) 18P 19P 25S
32) 6P 16P 21P
33) 0S 9P 27S
34) 5P 11S 12S
35) 4P 7S 22S
36) 2P 16S 28P
37) 2S 11P 18P
38) 11S 18S 19S
39) 5P 21P 24S
40) 9S 10S 12P
41) 5S 11P 22S
42) 20P 26P 27P
43) 10S 13P 23S
44) 1P 6S 29S
45) 17S 20P 22P
46) 1S 12P 15P
47) 5P 12S 19P
48) 7S 21P 24P
49) 20P 22S 29S
50) 15S 20P 25S
51) 19P 23P 28P
52) 0S 9P 14P
53) 9P 16S 29P
54) 11S 17P 19S
55) 17S 23P 29S
56) 4P 6P 22P
57) 7P 22S 23S
58) 4S 15S 25S
59) 6P 8P 18S
60) 6P 11P 18P
61) 0S 13S 17P
62) 8S 15P 22S
63) 2S 19P 24S
64) 9P 12S 21S
65) 18S 22P 23P
66) 2P 19P 25P
67) 2S 18P 27S
68) 10P 15S 25P
69) 1S 5P 14P
70) 5S 27P 29P
71) 6P 11P 17P
72) 5P 17P 26P
73) 6S 9S 18S
74) 8P 12P 19S
75) 1S 27S 28P
76) 1S 9S 16P
77) 1S 3P 26P
78) 3P 10S 16S
79) 18S 22P 29S
80) 2S 6S 15P
81) 0P 19P 23P
82) 4P 10P 14P
83) 13P 24S 29P
84) 3P 4P 9S
85) 5S 28S 29S
86) 6P 17S 22P
87) 9S 16S 22S
88) 4P 6S 15S
89) 4S 12P 18S
90) 0P 9P 24S
91) 5P 8P 25S
92) 7S 19P 20P
93) 3P 17P 26P
94) 6P 7P 11P
95) 1P 10S 29P
96) 3P 16S 17S
97) 8S 17S 26P
98) 2S 15S 16P
99) 7S 15P 22S
100) 0S 12P 18P
101) 12S 16S 17P
102) 13P 15P 19S
103) 1P 23P 27P
104) 7S 14P 17P
105) 8P 13P 17P
106) 2S 8P 18S
107) 2S 6P 19S
108) 13P 20S 28P
109) 10P 15S 23P
110) 6S 14P 21S
111) 1S 11P 19S
112) 13P 19S 21S
113) 7P 11S 23P
114) 4P 21S 25P
115) 19P 22P 23S
116) 6P 8P 24S
117) 12P 15S 28S
118) 3P 13S 24P
119) 1P 4P 28P
120) 8S 9P 11P
121) 8P 12S 29S
122) 9S 14S 20P
123) 4S 7P 28S
124) 2P 9P 28P
125) 15P 17S 29P
126) 12P 28P 29P
127) 1S 7S 23S
128) 13S 20P 29P
EXAMPLE N 1
The result of Superreduction
I original CNF:
0) 26P
1) 24P
2) 20P
3) 19P
4) 16S
5) 13P
6) 12P
7) 9P
8) 4P
9) 2S
10) 1S
11) 5S 7S 14P 27S
12) 18S 27S
13) 18S 25S
14) 18S 23P
15) 18S 22P
16) 18S 21P
17) 17P 18S
18) 15P 18S
19) 14S 18S
20) 11S 18S
21) 10P 18S
22) 8P 18S
23) 7P 18S
24) 6S 18S
25) 5S 18S
26) 3P 18S
27) 5P 18P
28) 28S
29) 5S 27S 29S
30) 5S 25S 29S
31) 5S 23P 29S
32) 5S 22P 29S
33) 5S 21P 29S
34) 5S 17P 29S
35) 5S 15P 29S
36) 5S 14S 29S
37) 5S 11P 29S
38) 5S 10P 29S
39) 5S 8P 29S
40) 5S 7P 29S
41) 5S 6S 29S
42) 3P 5S 29S
43) 5S 27P 29P
44) 5S 25P 27S
45) 5S 23S 27S
46) 5S 22S 27S
47) 5S 17S 27S
48) 5S 15S 27S
49) 5S 11S 27S
50) 5S 10S 27S
51) 5S 8S 27S
52) 5S 6P 27S
53) 3S 5S 27S
54) 0S 5S 27S
55) 5S 14P 21S 27S
56) 18S 29P
EXAMPLE N 1
The result of reduction I CNF in the form DNF
0) 0N 1N 2N 3N 4D 5D 6D 8N 9D 10N 11N 12D 13D 14D 15N 16N 17N 18N 19D
20D 22N 23N 24D 25D 26D 27D 28N 29N
1) 0N 1N 2N 3N 4D 5D 6D 7N 8N 9D 10N 11N 12D 13D 15N 16N 17N 18N 19D 20D 21N 22N 23N 24D 25D 26D 27D 28N 29N
2) 1N 2N 3D 4D 5D 6N 7D 8D 9D 10D 11D 12D 13D 14N 15D 16N 17D 18N 19D 20D 21D 22D 23D 24D 25N 26D 27N 28N 29D
3) 1N 2N 3D 4D 5N 6N 7D 8D 9D 10D 11N 12D 13D 14N 15D 16N 17D 18D 19D 20D 21D 22D 23D 24D 25N 26D 27N 28N 29D
EXAMPLE N 2
II original CNF:
0 1S 2S 7S 21S
1 0P 13S 15S 23P
2 4P 6P 7P 11P
3 0S 14P 22S 29S
4 10S 11S 26P 29P
5 7P 20P 24P 27S
6 1P 20P 21S 28S
7 7S 14S 19S 26S
8 0P 4P 7S 29S
9 4P 8P 10S 18P
10 8S 23P 28P 29P
11 0P 4P 13P 24P
12 4S 15S 19P 26S
13 1S 11S 13P 26S
14 1S 9P 28P 29P
15 2P 5S 16P 22P
16 0S 3S 26P 28P
17 2S 11P 25S 28S
18 3P 5P 9S 14S
19 18S 19S 26S 28P
20 7P 13S 27P 28P
21 2S 10P 11P 12P
22 15P 17S 19S 26P
23 1P 8P 10P 23S
24 2S 14P 15S 22P
25 15P 22S 26P 28P
26 0P 10P 13S 26S
27 9S 20P 22P 23P
28 6P 13P 23S 25P
29 5P 12P 18P 19P
30 2P 5S 19S 27P
31 6S 15S 19P 24P
32 0S 20S 22P 29P
33 9S 14P 17S 19P
34 5P 7P 15P 26P
35 0S 2S 5P 8S
36 2P 9S 10P 18S
37 0P 5S 8P 9S
38 2P 6S 18P 19P
39 9P 22P 25P 28P
40 11S 22S 23S 28P
41 3S 6S 8P 22S
42 9P 11P 25P 27P
43 8S 15S 24S 27P
44 1P 2S 11P 19S
45 2S 6S 25S 28P
46 9P 12P 20P 29P
47 2P 6P 24P 26S
48 3S 20P 24S 27P
49 3P 18P 25S 28P
50 2S 13P 15S 27S
51 1P 4S 12P 16S
52 1P 4S 8P 9S
53 1P 2P 11P 16P
54 1P 3S 12S 18P
55 0P 9P 15P 26S
56 7S 11S 15P 23S
57 12S 21S 23S 28S
58 0P 1P 16P 22P
59 6S 7P 24S 27P
60 0P 7S 9S 26P
61 1S 12S 22S 23S
62 6S 11S 20S 22P
63 4P 9S 13P 27P
64 1S 9P 10P 23S
65 5P 15P 18S 26P
66 9S 16S 19P 25S
67 5S 18P 20S 22S
68 1P 5P 12S 19S
69 6P 15S 22S 23P
70 12S 16S 21S 24P
71 1S 6S 9P 10S
72 7P 10S 11P 26P
73 8P 12P 17S 18S
74 3S 17P 26S 28P
75 11P 14P 27P 29S
76 0P 4S 14S 23S
77 0P 1S 13S 27P
78 4P 11P 12S 27P
79 2P 11P 18P 19P
80 4S 23S 25S 27P
81 11S 16S 17S 20P
82 11S 16P 22S 28S
83 18P 21P 26S 27S
84 1S 4P 26P 27P
85 6S 18S 25S 29S
86 1P 9S 15S 28P
87 10S 11P 15S 24P
88 11P 17S 25S 26P
89 1P 13P 26P 28S
90 0P 3S 5S 20P
91 5P 6S 18S 28P
92 2P 11S 15P 24S
93 1P 13P 16S 23S
94 2S 6S 10P 12P
95 12S 15P 21P 24P
96 4S 9S 14S 18P
97 6P 10S 17P 21P
98 1S 8S 19S 21P
99 14P 15S 21P 24P
100 6S 9P 11P 16S
101 5S 18P 22S 27P
102 2S 11S 18P 24S
103 9S 10P 18S 22S
104 10P 15P 27S 29P
105 3P 9S 10P 27P
106 4S 6P 16P 17S
107 18P 23S 28P 29P
108 1P 2P 9S 28S
109 1P 4S 23S 28S
110 1P 6S 15S 24S
111 2P 12P 23S 28P
112 1P 9S 17S 29S
113 11S 14S 25P 27S
114 13S 14S 15P 27S
115 8S 10P 13S 26P
116 1P 6P 9S 20S
117 12S 14S 17P 21P
118 9S 16S 19P 22P
119 3P 5P 8S 12S
120 3S 16P 19P 27S
121 6P 14P 26S 28P
122 7P 12S 15S 18P
123 7S 12P 15S 26S
124 8S 11S 12P 14P
125 10P 20S 26S 29P
126 16P 17S 19P 23S
127 7S 13P 14S 20P
128 8S 20P 21S 28S
129 10P 11P 20P 24P
130 3S 5S 8P 25S
131 7P 9S 10P 12S
132 15S 18S 20P 27P
133 6S 7P 17S 23P
134 17P 18P 21P 24P
135 9S 12P 18S 19S
136 0S 9S 10S 25S
137 1P 5P 18P 27P
138 2S 5P 10P 13S
139 1P 2P 21S 27P
140 2P 18P 21P 24S
141 1P 4P 7S 17P
142 10S 12P 22S 26S
143 2P 8P 10S 19P
144 5S 7P 9S 20P
145 11P 19P 21S 22P
146 4S 7S 18P 22S
147 3S 7P 19P 29S
148 6P 12S 18S 26S
149 12S 14P 17S 18P
150 5S 8P 24S 29P
151 6S 12P 21P 23S
152 3P 9P 15P 20S
153 2P 11P 21P 22S
154 14S 18S 19S 22P
155 0P 16P 22P 27S
156 9P 15P 18P 23P
157 9P 11P 19S 21P
158 0S 3S 27S 28P
159 7P 13S 14P 28S
160 5S 10S 11P 17P
161 2P 3S 19P 25P
162 10P 17P 24P 26P
163 6S 7S 10P 21P
164 22P 24P 26P 27S
165 0S 5P 11P 25S
166 2S 8P 14S 25S
167 11S 12S 20S 25S
168 10S 18S 21P 22P
169 8S 17P 21P 27P
170 0S 7P 26P 28P
171 3P 13P 15S 22P
172 9P 12P 22S 29S
173 2S 6S 15S 19S
174 8S 19S 23S 28P
175 0S 7S 22S 29S
176 5P 27S 28P 29S
177 1S 8P 12S 14S
178 2S 10P 22S 25P
179 4S 7P 22S 28P
180 4P 21P 23P 24S
181 11P 15P 17P 20P
182 5S 13P 21P 28P
183 7P 15S 23P 29P
184 2P 7P 17P 28P
185 19S 21S 24P 27S
186 0S 16S 18P 23S
187 16S 21P 22P 28P
188 2P 3P 25S 26S
189 9P 10S 27S 29P
190 0S 2P 13S 29P
191 9P 12S 20S 25S
192 9P 14S 17S 25P
193 10P 11P 17S 25P
194 11S 12S 13P 15P
195 8S 19P 26P 27P
196 3P 14S 26P 28P
197 3S 20S 23S 27S
198 0P 6S 21S 23S
199 20P 22P 28S 29S
200 0S 11P 18S 29S
201 0S 17S 27S 29S
202 4S 18P 24S 27P
203 2P 3P 6S 20S
204 12P 21S 24P 27S
205 12P 15P 26S 29S
206 5P 7P 24S 27S
207 1S 17S 21P 23S
208 18P 20P 21S 22P
209 0P 1P 15P 16P
210 9S 11S 12P 25P
211 1S 3P 13S 28P
212 4S 9S 19P 25S
213 2S 20S 23P 28S
214 12P 18P 19S 24S
215 4S 5P 11S 17P
216 6P 20S 22S 29P
217 8P 16P 18P 27P
218 21P 22P 24P 25S
219 16P 18P 19P 25P
220 7P 8S 11S 20P
221 10P 20P 25P 29P
222 24S 26S 28P 29P
223 3S 10S 13P 26P
224 1S 8S 23S 25P
225 12P 13S 23S 25P
226 0P 3S 11S 23P
227 7P 9S 15P 22P
228 4S 8S 14S 23P
229 7S 8S 12P 21S
230 1P 3P 4S 24S
231 7S 12S 22P 24S
232 5P 8S 20P 28S
233 11S 17S 22S 29S
234 10P 20P 26P 28S
235 3P 11S 14P 16S
236 2S 12P 13P 23P
237 5S 7P 8P 15P
238 1P 4P 7S 16P
239 6S 8P 22P 27S
240 2S 8S 14P 22S
241 2P 4P 7P 15P
242 9S 16P 24S 27P
243 10P 12S 15P 25S
244 3S 12S 14P 28S
245 11S 20S 23P 27S
246 0S 2S 3P 4S
247 1P 7S 19P 26S
248 1S 6S 8S 24P
249 1P 10P 12P 15S
250 5S 6P 14P 18S
251 8S 9P 12P 21P
252 4S 13S 24S 27P
253 2P 6P 15P 16S
254 5P 8P 11S 15S
255 10S 20S 23P 25S
256 7P 11S 16S 29P
257 4S 11S 13P 21P
258 8P 18S 21S 29S
259 13P 16P 24P 29P
260 1S 3P 4P 10P
261 2P 18S 24P 27S
262 1S 13S 20S 25P
263 3P 16S 17P 22S
264 6P 8P 23P 26P
265 10S 12S 17P 22S
266 7S 13S 22S 25P
267 8S 16P 17S 28S
268 2S 18P 19P 23S
269 9S 11P 22S 24S 25P
270 1P 3S 8P 19S 29S
271 4P 11S 13S 24P 25S
272 10S 13P 14P 20S 25S
273 15S 19S 20P 21S 27S
274 2P 6S 14P 15P 16S
275 7S 19P 22P 24P 29P
276 0S 1S 6P 7S 11S
277 0P 4S 12P 15P 21P
278 2P 3S 10P 12P 17S
279 8S 12P 16P 18S 19S
280 8P 9P 11P 20S 25S
281 0P 3P 7P 13S 23S
282 5S 14S 16P 19S 23S
283 0S 4P 5S 13P 27S
284 3P 6P 10S 17P 22S
285 3P 10S 13P 16S 28P
286 1S 4S 9P 19S 25P
287 1P 8S 16P 17S 19S
288 2P 12S 17P 25P 26S
289 8P 10S 11P 16S 27S
290 11P 14P 19S 21P 24P
291 0S 6S 7S 14P 24S
292 5P 9P 24S 27P 29S
293 12P 21S 24S 26S 29S
294 0P 6S 18P 19S 27S
295 4S 6S 7P 10S 29P
296 1S 3P 8S 10P 12P
297 2S 10P 12P 16P 22P
298 9P 17S 22S 24P 26S
299 2S 11P 22S 25S 28P
300 1P 7P 16S 24P 25P
301 7S 8S 17S 18P 22P
302 7P 20S 22P 26S 29S
303 7P 10P 16S 27P 28S
304 13S 15P 19S 22P 23P
305 0P 5S 21P 22S 24P
306 6S 17S 21P 24P 27P
307 3S 4P 5P 10S 12P
308 3S 9P 10S 18P 20P
309 5S 14P 18P 20S 26S
310 2P 8P 13P 14S 27S
311 1S 10S 21S 22P 24S
312 0S 13S 20S 26S 28P
313 4P 6P 16S 18S 26S
314 2S 11S 15S 23P 26S
315 4P 5S 9S 19P 24S
316 5S 9S 13P 15P 17P
317 0P 4P 7P 23P 28P
318 6P 8P 16S 22P 26S
319 19P 21S 22P 24S 27S
320 5S 6P 9P 17P 22P
321 1P 5P 7S 10P 23P
322 0P 13P 16S 22S 25P
323 17S 20S 23P 25P 26S
324 0P 5P 14S 20S 26P
325 5P 18P 25S 28P 29P
326 0P 8S 9P 12S 22S
327 15S 17P 21S 23S 25P
328 0S 3S 15P 20P 25S
329 1P 7P 20S 24S 28S
330 2S 4P 12S 21P 24S
331 5S 13P 21S 22P 28S
332 5P 8P 11P 12S 23S
333 6P 7P 13S 14P 22P
334 0S 3P 12S 19P 21P
335 5S 12S 18P 21P 26P
336 2S 7P 10P 13P 25S
337 1S 9P 13P 18P 19S
338 6P 14S 22P 28S 29S
339 6S 14S 16S 24P 27P
340 3S 8S 11S 12P 20S
341 10P 12S 13P 15S 18P
342 8S 10P 13S 23S 25S
343 13S 15P 19S 26P 28S
344 5S 9P 15P 24P 29P
EXAMPLE N 2
The result of Super-reduction
II original CNF:
0 28P
1 27P
2 26S
3 25S
4 24P
5 23S
6 22P
7 21P
8 20P
9 19P
10 18P
11 17S
12 16S
13 15P
14 14P
15 13S
16 12P
17 11S
18 10S
19 9S
20 8P
21 7P
22 6P
23 5S
24 4S
25 3P
26 2S
27 1P
28 0P
29 29S
EXAMPLE N 2
The result of reduction
II CNF in the form DNF:
0) 0D 1D 2N 3D 4N 5N 6D 7D 8D 9N 10N 11N 12D 13N 14D 15D 16N 17N 18D
19D 20D 21D 22D 23N 24D 25N 26N 27D 28D 29N
EXAMPLE N 3
III original CNF:
0 2P 26S 28P 29S
1 14P 20S 22P 24P
2 2S 14S 22P 27S
3 9S 14S 16P 27S
4 9P 19P 20P 23S
5 5S 17S 18P 25P
6 0P 17S 26S 28S
7 10S 11S 20P 22P
8 1P 10P 21S 22P
9 1S 12P 23P 27S
10 7S 8P 9S 13P
11 1P 3S 18P 25P
12 2S 4P 23S 26S
13 5P 9S 13P 20P
14 7P 19P 23S 25P
15 4S 7P 23S 24P
16 8P 9S 16P 19S
17 2S 9S 11P 25S
18 8S 9P 10S 19S
19 3S 8P 24S 28S
20 3S 7S 15S 16S
21 14S 17P 19P 29S
22 6S 9P 19P 28P
23 11P 12P 18P 20S
24 10S 14S 21P 24S
25 13S 17P 22P 27S
26 3P 6P 13P 14P
27 2P 3P 5P 16P
28 10P 14S 15P 21P
29 0P 2P 19S 23P
30 4P 5P 19P 21P
31 9P 22P 23S 24P
32 1S 2P 5S 16S
33 0P 16P 20S 26P
34 11S 12P 27S 28S
35 13S 19S 22S 24S
36 2P 15P 18P 29P
37 10P 19S 20S 24P
38 4S 14P 19S 27P
39 12P 14S 26S 28S
40 4P 8P 10P 25S
41 0P 23P 25S 26S
42 9S 10P 13S 17S
43 7S 15P 22P 26P
44 8S 9P 13P 14P
45 12P 13S 18P 22P
46 1P 13P 20P 29S
47 6S 7S 20P 21P
48 6S 24S 25S 28S
49 14P 16P 18S 29P
50 0P 2P 5S 18P
51 2P 5S 11P 13P
52 13S 15S 16P 29P
53 8S 11S 14P 23S
54 2S 16S 21S 23P
55 12S 19S 25P 27S
56 8P 11S 18P 19S
57 9S 17S 18P 25S
58 5S 14S 16S 19S
59 1S 11S 15P 20P
60 6P 7S 10S 26P
61 8S 9P 24P 27P
62 1S 8S 22S 24S
63 2S 12P 18P 22P
64 0P 4S 15P 23S
65 0S 8P 11S 21S
66 4P 11P 12P 24S
67 8S 20P 25S 26S
68 0S 10S 16S 19P
69 3S 7S 18S 20S
70 19P 23S 25P 28S
71 8P 10S 18P 19P
72 0S 3S 5P 23P
73 3P 14S 23S 28S
74 0S 3S 17S 27S
75 1P 4P 5P 7S
76 16S 20P 27P 28P
77 1S 11S 19P 27P
78 7P 17P 22S 25S
79 4P 11P 19S 25S
80 15P 19S 24P 28S
81 1P 15S 18P 29S
82 18P 21S 25P 28P
83 1S 25S 27S 28S
84 5S 17P 19P 20S
85 2S 5P 12P 29S
86 1S 11P 12S 13P
87 13P 19S 20S 28S
88 13S 15P 16P 25P
89 8P 18P 27S 29S
90 1P 4S 15P 25P
91 1P 10P 11P 16S
92 11P 21P 25P 28P
93 2S 10P 13P 29P
94 5S 10P 14P 21P
95 5P 8S 14P 16S
96 5P 23S 24S 27S
97 4P 19P 24S 27S
98 15P 18P 22S 23S
99 7S 12S 19S 22S
100 0S 7P 23P 29S
101 3S 12P 18P 23S
102 2P 7P 17S 26S
103 9P 13S 17P 22P
104 12P 15S 19S 25P
105 0S 1P 2S 3P
106 4S 21S 25S 29P
107 3P 16P 19S 26S
108 0S 4P 20P 22P
109 21S 22P 23S 24S
110 1P 3P 4S 22S
111 9P 19S 26P 28S
112 4S 5P 8S 20S
113 2P 4P 17S 19S
114 3P 11P 12S 13P
115 12P 18S 21S 27P
116 0P 16P 28P 29S
117 2S 8S 19S 21P
118 14P 15P 17P 23S
119 0S 2P 19S 22P
120 0P 16P 18P 20S
121 7P 13S 26P 27S
122 12P 14S 25P 26S
123 10P 11S 18P 23P
124 2S 7P 19S 24P
125 8S 10S 12S 25P
126 12P 13S 21S 22S
127 17P 20S 22S 25P
128 3S 11P 16P 18P
129 0P 9P 13S 16S
130 5P 6P 10P 15S
131 6P 12P 16P 24P
132 6S 13P 16P 26P
133 6P 9S 21S 29P
134 2S 7S 10P 26S
135 12P 13P 26P 28S
136 5S 16P 25P 26P
137 0S 8P 9P 22P
138 0P 1S 13S 20P
139 1P 11P 15P 21S
140 3P 8S 14S 23S
141 3S 13P 24S 25S
142 0S 16S 23P 26S
143 1P 13S 22S 29S
144 1S 3P 6P 15S 29P
145 12S 18P 21S 23P 29S
146 13S 14P 25S 28S 29S
147 6P 9S 14P 18P 19P
148 4P 12S 16P 23S 29S
149 2P 6P 7S 13S 19P
150 4P 6P 16P 23P 27S
151 2S 13S 25S 28S 29P
152 13P 15P 17S 21S 25S
153 4P 6S 12P 14P 27P
154 3S 12S 13P 22P 26P
155 1S 7S 15P 27S 28P
156 0P 4P 7P 23S 29P
157 3P 8P 14P 17S 24P
158 5P 6S 8S 20P 29P
159 0S 3S 9S 26S 29S
160 1P 10S 13P 17P 21S
161 5S 12P 14S 21P 24P
162 2P 18S 20P 24S 29P
163 1S 4S 19S 24P 29P
164 6P 7S 10P 12P 27P
165 1P 2S 11P 13P 18P
166 0P 8S 19P 22S 25S
167 1P 6S 7P 21S 24S
168 7S 15S 18S 24P 26S
169 0S 5S 7P 23S 25P
170 3P 8S 14P 19S 28P
171 15P 17P 23P 24S 28P
172 10S 11P 24P 27S 29P
173 7S 8S 9P 17P 19S
174 1S 4P 16S 18S 27P
175 6S 7S 9P 16P 23S
176 3P 8S 14P 15S 22P
177 2S 3S 7S 12P 27P
178 1P 7P 15S 21P 26P
179 16P 17P 23P 26P 28P
180 0P 1S 8S 10S 29S
181 3S 7S 19S 21S 27P
182 1S 10P 22S 24P 27P
183 10P 13S 14S 16P 24P
184 7S 19S 23S 26S 29S
185 9S 10S 11S 18P 27S
186 2S 6P 10S 19S 29P
187 0P 5P 9P 21P 26S
188 9P 14P 15S 17P 23S
189 1S 3S 5S 12P 26P
190 2P 4P 10P 15S 18P
191 0S 7S 10P 18P 23S
192 3P 7S 16S 18S 29P
193 4S 7P 10S 13S 29P
194 4S 13S 15S 27P 28P
195 3S 5P 11P 17S 22S
196 0P 4S 15P 16P 21S
197 5P 9S 16P 18P 27P
198 1S 13S 20P 26P 28S
199 8S 13S 20S 21S 28P
200 2P 5S 11S 19P 28P
201 8S 16P 21S 26S 27P
202 0S 1S 22S 23P 24S
203 1P 6S 14S 22S 25S
204 6S 8P 12S 15P 27S
205 0P 2P 15P 17P 24P
206 9P 18S 23S 25S 29S
207 7P 8P 15P 16S 22S
208 4S 10P 11S 20P 24S
209 6S 9P 16S 17S 22P
210 4P 5S 14P 19S 24S
211 3S 8S 11S 16P 23P
212 1S 3S 5S 7S 10S
213 6P 7P 8S 19S 21S
214 0S 9S 17P 25P 27P
215 1P 2S 10P 20P 27P
216 3S 17S 19P 26P 28P
217 2S 6P 20P 22S 28P
218 0P 14S 22S 26S 27P
219 3P 11S 15P 17P 19P
220 7S 9S 12S 15P 22P
221 6S 7P 9S 20P 28P
222 5S 9P 11P 19P 26P
223 8S 9S 11S 12S 20S
224 5S 13S 18P 22S 27P
225 0P 5S 18S 22P 23S
226 3S 7P 12P 17S 23P
227 7S 9S 17P 21S 26S
228 1P 22P 25S 28S 29S
229 0P 3S 8P 12S 29S
230 1S 5P 8P 9P 16S
231 5S 13P 16P 20S 22S
232 9S 11P 12S 14P 23S
233 9S 10P 12P 13P 29P
234 2S 3S 4S 26P 28P
235 2S 19P 20S 25S 29P
236 0P 4P 6P 8S 25P
237 6P 8P 26S 27P 29P
238 10S 17S 19S 23S 27S
239 2S 3P 16P 17S 29S
240 0S 9P 12S 25P 26P
241 6S 13S 22P 23S 29P
242 1P 7S 19P 23S 24S
243 0P 16S 17S 26P 27P
244 2P 8S 13P 21P 25P
245 3S 15S 16S 17P 27P
246 4P 10P 24P 25P 27P
247 0S 1S 6S 14P 28P
248 4S 5S 11P 20S 22S
249 3P 6P 16S 22S 27S
250 5S 8S 17S 21P 22S
251 1S 10S 12S 19P 27P
252 11S 12S 13P 21P 25S
253 7P 8P 14S 24P 28P
254 5P 7S 12S 18S 25P
255 0S 2S 7P 9S 22P
256 1S 7P 12S 24P 26S
257 7P 10S 17S 18P 28S
258 9P 13S 15P 17P 28S
259 15P 16P 20P 24P 28P
260 13P 19P 23S 28S 29P
261 1P 5P 12S 18S 25P
262 0S 11S 19S 26S 27S
263 2S 3S 6P 16P 26P
264 2P 4S 7P 21P 28P
265 4P 7P 10P 23S 28P
266 3S 13P 23S 25P 28S
267 2P 5P 7P 27P 28P
268 3P 8S 14S 16P 26P
269 2S 3S 7P 18P 25P
270 0P 4S 16P 19P 26S
271 9S 16S 17P 18S 26P
272 1P 8S 14P 20S 28P
273 3P 13P 26P 27S 29S
274 1S 15P 21S 26P 27P
275 3P 11P 13P 22P 28S
276 5S 15S 19P 25S 26P
277 5P 6S 8S 10S 14P
278 8S 9P 16S 23S 27S
279 2P 11S 17S 23S 26P
280 11S 15P 20P 25S 27P
281 3S 15S 16P 18P 21S
282 2P 4S 8P 9P 14S
283 4S 5S 12P 18P 22S
284 1S 10S 14S 18S 23P
285 0S 6S 8P 22P 28P
286 1S 8P 9P 12S 18S
287 0P 3S 22P 25P 29P
288 5S 6S 12P 13P 15P
289 8S 10S 13P 15P 16P
290 0P 1S 2S 7P 23S
291 3P 4P 5S 6S 11P
292 1P 2P 4S 25P 29P
293 1P 5S 11P 15S 29P
294 8P 9S 12P 25P 28S
295 0P 6S 7S 15S 19S
296 2S 5S 11S 15S 19S
297 12P 17P 20P 25P 27P
298 9S 12P 17S 19P 21P
299 16S 21S 24P 25P 26S
300 4P 11P 17P 24P 28P
301 5S 16S 20S 22S 25S
302 13P 14S 19S 20P 26S
303 0S 7S 10S 16P 26P
304 11P 21S 22S 26S 28S
305 7S 16S 19P 23S 27S
306 4S 14P 21S 24S 29S
307 1P 4S 7P 14P 18S
308 1S 18P 20P 25S 27P
309 0S 2S 17S 21P 23S
310 2P 4P 6P 11P 12P
311 1P 7S 10P 24P 29P
312 5S 19P 21S 27S 29P
313 3S 6P 18S 25S 28P
314 16S 17P 20S 25P 29S
315 1S 7P 9S 19P 25S
316 5P 8S 17P 18S 22P
317 23P 24S 25S 26P 29P
318 1P 7S 12P 23P 29P
319 5P 6S 10P 14P 23P
320 9P 15S 16S 19P 23S
321 6P 7S 11P 13P 29P
322 11S 17P 20P 21S 29S
323 3S 8P 13P 16P 18S
324 1P 4S 12S 16P 19S
325 0P 5P 12S 17P 18P
326 0P 3P 13S 23P 26S
327 7S 13S 14P 23P 24S
328 0P 12S 20S 25S 28S
329 9P 11P 12S 21P 27S
330 2S 3P 10P 15P 24S
331 4S 6S 12S 18S 25P
332 13S 19S 21S 24P 28P
333 9P 10S 23P 27P 29P
334 8S 10P 16P 22P 24S
335 9S 12P 17S 22P 26P
336 5S 17P 24S 25S 26S
337 3P 14S 24S 25S 27S
338 7S 18P 19S 24S 26S
339 1S 12S 17S 19S 27S
340 3S 19P 20S 26S 29S
341 17P 20S 21P 26S 28S
342 10P 16S 24P 25P 28S
343 2P 9S 11S 25S 27P
344 1S 9P 10S 15S 27S
345 1S 2P 13P 21P 23P
346 11P 13S 20P 22P 27S
347 8P 16S 18P 20S 27P
348 0S 5P 7P 10P 15P
349 7S 13S 15P 25P 29P
350 11S 18P 20S 25P 28P
351 3P 10S 12S 13P 29S
352 13P 14P 19S 25S 28P
353 6P 18P 19S 21P 23S
354 14S 19P 20S 24S 29S
355 1P 10S 18P 21P 28P
356 0S 1S 3S 10P 12S
357 0P 8P 11P 13P 20S
358 0S 1S 2P 12S 17S
359 0P 9P 18P 19S 25P
360 15P 17P 19P 20S 25S
361 4P 11S 18S 19P 25P
362 5S 9P 10S 13P 27P
363 5S 6S 17S 24P 25P
364 3S 7P 12S 15P 20P
365 3S 17P 21S 24P 27S
366 3S 9P 14S 20S 25S
367 0P 4S 9S 16S 19S
368 7P 9P 13P 15P 16P
369 5P 8P 11P 14P 19S
370 0S 4P 10S 21S 23P
371 1S 2S 5P 21S 28S
372 14P 15P 20S 23S 26S
373 1P 7P 9S 17S 20S
374 1S 2S 17S 23S 25S
375 1P 2S 16P 27P 29P
376 5P 13P 21P 24P 26P
377 11P 12P 14P 17S 25P
378 0S 2P 12P 15S 27S
379 4S 10S 14P 23P 29P
380 7S 10P 16S 20S 22P
381 3P 16P 26P 27S 29P
382 2S 7P 11S 13S 27P
383 0P 3P 10S 22P 25P
384 3S 5S 8S 13P 26P
385 1S 2P 8P 15S 19P
386 2P 6S 7P 11P 18P
387 6P 8P 10P 26S 27S
388 3P 4S 14P 22P 29P
389 3S 7P 21S 22P 23P
390 5P 9P 16S 19P 21P
391 0P 6S 7P 12P 23P
392 1S 3P 10S 24S 25S
393 8P 10P 21S 24S 25S
394 9P 11P 14P 23P 24P
395 0S 10S 15S 19S 25S
396 0P 2S 10S 13S 20S
397 4P 12P 21P 22P 24S
398 2P 3P 9S 21S 25P
399 1S 10S 11S 18P 28P
400 5S 10P 22P 23S 25P
401 2S 12S 20P 23P 28P
402 12P 20P 21S 24P 25P
403 1S 2S 5P 18S 22P
404 7P 17S 20P 21S 24P
405 0P 13S 15S 28P 29S
406 12P 13P 17S 21P 28P
407 5P 15S 17P 21P 27P
408 1S 9S 10S 12P 20S
409 2P 10S 16S 20P 22S
410 17S 19S 22S 23P 26P
411 7S 19S 23S 26P 28P
412 1P 2S 7S 14P 28S
413 4P 13S 14P 28S 29S
414 0S 10S 12P 15P 27P
415 4P 6S 8P 13S 18P
416 0P 2S 8P 11P 14S
417 3S 14S 17S 24S 28S
418 1S 4S 7P 10P 13P
419 10P 11S 21P 22P 24S
420 2P 9S 17S 19S 26S
421 2P 4S 9S 15P 21P
422 3S 6S 10P 12S 26P
423 24P 25S 26P 27P 28S
424 1P 2S 9P 23P 24P
425 5P 7P 20P 24S 29P
426 4P 16P 18P 21S 28S
427 6S 13P 21S 24S 29P
428 2P 11S 14S 16S 27P
429 0S 10S 11S 16S 28S
430 2S 5S 9S 13S 15P
431 8P 10P 14P 17S 23P
432 7S 10S 15S 23S 27S
433 6P 11S 19P 20S 25P
434 10S 13S 15P 28P 29S
435 0P 17P 26P 27P 28S
436 0S 7S 13S 15P 16P
437 4P 6P 15P 18P 20P
438 3S 6S 8S 15S 27P
439 0S 2P 14P 17S 24S
440 2S 7S 11S 13S 17S
441 1S 11P 17S 20P 23S
442 3P 4P 18P 19P 27S
443 11P 16S 22S 26S 28S
EXAMPLE N 3
The result of Superreduction
III original CNF:
0 27P
1 24S
2 23S
3 19S
4 18P
5 16P
6 15P
7 14P
8 13S
9 11P
10 10P
11 7S
12 6S
13 1S
14 0S
15 29S
16 25S 28S
17 22P 28S
18 21S 28S
19 20S 28S
20 17S 28S
21 12P 28S
22 9P 28S
23 8S 28S
24 5P 28S
25 4P 28S
26 3P 28S
27 2P 28S
28 26S 28P
29 25P 26P
30 22S 26P
31 21P 26P
32 20P 26P
33 17P 26P
34 9S 26P
35 8P 26P
36 5S 26P
37 4S 26P
38 3S 26P
39 2S 26P
40 26P 28S
EXAMPLE N 3
The result of reduction
III CNF in the form DNF:
0) 0N 1N 2D 3D 4D 5D 6N 7N 8N 9D 10D 11D 12D 13N 14D 15D 16D 17N 18D 19N 20N 21N 22D 23N 24N 25N 26D 27D 28D 29N
1) 0N 1N 2N 3N 4N 5N 6N 7N 8D 9N 10D 11D 13N 14D 15D 16D 17D 18D 19N 20D 21D 22N 23N 24N 25D 26N 27D 28N 29N
EXAMPLE N 4
IV original CNF:
0 1P 7S 11S
1 5S 11P 21S
2 4S 12P 18P
3 17S 21P 23P
4 14S 16S 25S
5 9P 16S 18P
6 9S 19S 27P
7 10S 22P 27P
8 0S 12P 20P
9 3S 19S 28P
10 2P 3S 28P
11 7P 18P 27S
12 2P 17S 21S
13 1P 22S 24P
14 10S 16P 25P
15 14P 16S 29S
16 11S 15P 22P
17 6S 11P 14S
18 6S 22S 28P
19 10P 13P 20S
20 0P 16P 19P
21 3S 18S 23S
22 8P 11P 22P
23 2S 16P 20P
24 5S 28P 29P
25 16P 23S 29P
26 0S 4P 12S
27 2P 22S 23P
28 5S 19P 26P
29 10S 19S 23P
30 0P 5P 14S
31 13S 16P 25S
32 0P 25S 28S
33 0S 8P 17P
34 5S 23S 24S
35 2P 4S 25P
36 9S 19P 25S
37 0S 7S 25P
38 10S 11S 18P
39 5S 12P 15S
40 7P 12S 21S
41 0S 1P 23S
42 2S 3S 20S
43 2P 7P 19P
44 10P 21P 26P
45 1P 12P 27S
46 0P 6S 12P
47 3P 6P 25S
48 4P 13P 17P
49 12S 17S 21P
50 23S 26P 29S
51 3P 10S 20P
52 3P 19S 29P
53 7S 9P 10S
54 4P 17P 19P 27P
55 1P 15P 20S 21P
56 4P 14S 18S 24S
57 2S 18S 22P 26S
58 0S 11S 15S 29P
59 0P 16S 24P 25S
60 9P 17S 22P 27S
61 20S 22S 25P 26P
62 3S 8S 10P 28P
63 1S 2P 11P 20P
64 4P 9S 10S 22S
65 5S 19P 24P 26P
66 6S 19S 24S 28P
67 9P 14P 20P 24P
68 2S 8S 9S 16S
69 0S 10P 12P 29P
70 6S 7S 26S 28S
71 11S 13P 18S 22P
72 0S 18S 22S 25S
73 0S 3P 23P 24S
74 4P 14P 21P 29P
75 10S 14P 20P 25P
76 6P 11P 18P 21P
77 17P 19S 24P 29S
78 1P 4S 7S 10S
79 2S 13S 21S 29S
80 2P 3S 12P 24P
81 2S 11P 20S 25S
82 2S 3S 7P 10P
83 1P 5P 27S 29S
84 3S 15S 25S 29P
85 6S 9S 17P 25S
86 14S 15P 17S 26P
87 4S 10S 11S 24S
88 9S 21P 22P 28P
89 7P 9S 10P 11S
90 9S 18P 23S 28P
91 6S 18S 20P 26P
92 1S 3S 6S 25P
93 1P 5S 9S 15P
94 7P 9P 20S 22S
95 12S 14S 17S 27P
96 12S 13P 16S 23P
97 10P 19P 20P 26S
98 0S 1P 4S 24S
99 0S 2S 3S 10P
100 1S 10S 20P 26S
101 1S 3P 20S 29P
102 7P 11S 14P 28P
103 6P 18P 24P 29P
104 2S 16S 18S 27P
105 6P 14S 22S 23S
106 4S 7P 14S 23P
107 3P 9P 15P 21S
108 7P 19S 26S 29S
109 1P 3P 16P 20P
110 9S 12P 21P 23S
111 4S 8P 24P 25S
112 3S 13S 27P 28P
113 1P 12S 22P 27P
114 1P 7S 9S 28S
115 6P 11P 21S 26P
116 2S 5P 6P 20P
117 9P 12S 27S 29P
118 5S 13P 15P 23S
119 1P 2S 4P 9P
120 6S 13P 16S 21P
121 5S 11P 19P 20S
122 3P 15S 20P 23S
123 3S 10P 12P 18P
124 5S 8P 22P 24P
125 2P 11S 19P 28S
126 12S 13P 22S 29S
127 5P 20S 23S 26S
128 8P 19S 21P 25P
129 0P 3S 9P 14P
130 3P 15S 18P 21P
131 2P 13S 22S 24P
132 3S 7P 21P 28P
133 6P 18S 22S 27S
134 3S 9S 19P 29S
135 6S 13P 15S 26S
136 14P 17S 25P 28S
137 16P 18S 22P 29S
138 4P 14P 18S 26P
139 3P 14S 20S 22P
140 12P 19S 26P 28S
141 9P 17P 21P 28S
142 5S 6S 11P 23S
143 0P 2P 9S 23S
144 10P 13P 22S 23S
145 2P 5P 25S 29P
146 20S 22S 27S 29S
147 0S 4P 9P 23P
148 4P 5P 19P 22S
149 12P 24S 25P 27S
150 1S 4S 10S 23P
151 3P 5S 6P 28S
152 0S 3S 19P 22S
153 4S 11P 17S 27S
154 7P 12S 23S 25S
155 2P 7P 8P 26P
156 2P 3P 4S 24P
157 0P 11S 12S 16P
158 7P 19P 26P 28P
159 1P 9P 16S 18P
160 10S 12P 17S 20S
161 1P 2S 3P 16S
162 12P 13P 16P 27S
163 4S 6P 8P 11P
164 5P 8S 13P 17P
165 1P 4S 16S 19P
166 9S 18P 19S 20P
167 9P 11S 22P 23S
168 1S 9S 21P 25S
169 6P 15P 17S 29P
170 2S 3S 11S 27S
171 12P 16S 19S 21S
172 2S 9P 13S 22S
173 4S 18P 21S 24S
174 7P 11P 12P 29P
175 13S 17S 18P 28P
176 10S 13S 14S 16P
177 16S 19P 20S 23S
178 9P 19S 26S 27P
179 1S 9P 12S 16S
180 20S 23S 25S 27P
181 15S 17P 20P 24S
182 0P 5P 16S 21S
183 2P 6S 7S 8S
184 0S 19P 21S 29P
185 5S 10S 11P 23S
186 2S 6P 15P 25P
187 4S 5P 11S 28S
188 0P 4S 10S 29P
189 1S 2S 4S 15S
190 1S 11P 15S 18S
191 11P 12P 27P 28P
192 4S 10P 16S 19P
193 2P 3P 11P 14P
194 3S 5S 7S 22P
195 4S 16S 21P 27P
196 1P 5S 6P 11S
197 9P 16S 22S 25S
198 14P 23P 26P 28S
199 4P 6P 10P 14P
200 20S 23S 26P 28S
201 2P 4P 14S 25S
202 0P 19S 28P 29S
203 0S 1S 8P 12S
EXAMPLE N 4
The result of Super-reduction
IV original CNF:
0 25S
1 24S
2 23S
3 21S
4 17S
5 13P
6 11S
7 10S
8 8P
9 7S
10 1P 9S 15P 27S
11 27S 28P
12 22S 28P
13 20P 28P
14 19S 28P
15 18S 28P
16 16S 28P
17 15S 28P
18 14S 28P
19 12P 28P
20 9S 28P
21 6P 28P
22 5S 28P
23 4P 28P
24 3S 28P
25 2P 28P
26 1P 28P
27 0P 28P
28 9P 28S
29 26P
30 9S 18P 29P
31 9S 18P 27S
32 9S 18P 20P
33 9S 18P 19S
34 9S 16S 18P
35 9S 15S 18P
36 9S 14S 18P
37 9S 12P 18P
38 6P 9S 18P
39 5S 9S 18P
40 4P 9S 18P
41 3S 9S 18P
42 2P 9S 18P
43 1P 9S 18P
44 0P 9S 18P
45 9S 27S 29S
46 9S 18S 22P 29S
47 9S 20P 22S 29S
48 9S 19S 22S 29S
49 9S 16S 22S 29S
50 9S 15S 22S 29S
51 9S 14S 22S 29S
52 6P 9S 22S 29S
53 5S 9S 22S 29S
54 4P 9S 22S 29S
55 3S 9S 22S 29S
56 2P 9S 22S 29S
57 1P 9S 22S 29S
58 0P 9S 22S 29S
59 9S 27P 29P
60 9S 22S 27S
61 9S 19P 27S
62 9S 14P 27S
63 9S 12P 27S
64 6S 9S 27S
65 5P 9S 27S
66 4S 9S 27S
67 3P 9S 27S
68 2S 9S 27S
69 0S 9S 27S
70 1S 9S 15S 27S
71 9S 15P 20P 27S
72 28P 29P
EXAMPLE N 4
The result of reduction
IV CNF in the form DNF:
0) 0D 1D 2D 3N 4D 5N 6D 7N 8D 9N 10N 11N 12D 13D 14N 15N 16N 17N 18N 19N 20D 21N 22N 23N 24N 25N 26D 27N 28N 29D
1) 0D 1D 2D 3N 4D 5N 6D 7N 8D 9D 10N 11N 13D 14N 15N 16N 17N 18D 19N
20D 21N 22D 23N 24N 25N 26D 27N 28D 29D
2) 0D 1D 2D 3N 4D 5N 6D 7N 8D 9D 10N 11N 12D 13D 14N 15N 16N 17N 18N 19N 20D 21N 23N 24N 25N 26D 27N 28D 29D
3) 0N 1N 2N 3D 4N 5D 6N 7N 8D 9D 10N 11N 12D 13D 14D 15D 17N 18D 19D 21N 22N 23N 24N 25N 26D 27D 28D 29N
4) 0N 1D 2N 3D 4N 5D 6N 7N 8D 9D 10N 11N 12D 13D 14D 15N 17N 18D 19D 20D 21N 22N 23N 24N 25N 26D 27D 28D 29N