SAAT issues (3) [Appendix]

By the SAT problem, say (3)

appendix:

1, the settime function is as follows:

Private void settime ()

{

Double _h, _m, _s, _ms;

_H = datetime.now.Hour-hh;

_M = datetime.now.minute-mm;

_S = datetime.now.second-ss;

_ms = datetime.now.millisecond-ms;

IF (_ms <0)

{

_ms = 1000;

_S- = 1;

}

IF (_s <0)

{

_S = 60;

_M- = 1;

}

IF (_m <0)

{

_M = 60;

_H- = 1;

}

IF (_H <0)

{

_H = 24;

}

SPTime.text = start _h.tostring () "h" _m.tostring () "m"

_s.tostring () "s" _ms.tostring () "ms";

}

2. The code for saving the subsequence and the calculation result is:

Private void savefiledlg_fileok (Object sender, system.componentmodel.canceleventargs e)

{

IF (SavefileDlg.FileName! = null && chlistbox.items [0] .tostring ()! = null)

{

FileInfo SHESOUREFILE = New FileInfo (Savefiledlg.FileName);

Streamwriter Writer = new streamwriter (Savefiledlg.FileName, true);

String text;

Writer.writeline ("subsequence is:");

For (int i = 0; i

{

Text = chaistbox.items [i] .tostring ();

Writer.writeline ("C" i.toString () ":" text);

}

Writer.writeline ("Current result is:");

Text = onesat.best.toString ();

Writer.writeLine (text);

Writer.close ();

}

}

3, the subserators of the four experiments are:

(1) The number of logical variables is 200

The subsequence is:

C0: X3 V-x26 V x39 V-x69 V x72 V -X84 V-X86 V -X140

C1: X3 V X7 V -X89 V -X103 V x143 V x172

C2: X34 V X36 V X57 V X73 V X75 V-x77 V X85 V -X116 V X136 V x138 V-x161 V x194

C3: -X52 V -X100 V -X146 V -X154 V x160 V-x162 V x170

C4: -X6 V-x92 V x126 v x128 v x182

C5: X15 V X41 V X45 V-X82 V X102 V X158 V-x165 V-x179 V x190

C6: X67 V-x69 V -X88 V X108 V-X140 V x166 V-X171C7: X4 V-x5 V-x11 V-x56 V x69 v x191

C8: -X33 V-x36 V X71 V X97 V-x115 V x133 V x149 V-x162

C9: -X2 V X34 V -X48 V-x54 V X56 V -X102 V-X135 V-X144 V-X147

C10: X3 V-x5 V-x88 V x101 V x139 v x192

C11: X7 V-x12 V X45 V -X120 V -X135 V-x137 V-x147 V x179 v x186

C12: -X10 V-x17 V X93 V X94 V x133 V-x164 V-x165 v x176

C13: -X24 V-x90 V-x118 V x120 V -X167

C14: X31 V X46 V -X58 V-x72 V X96 V -X108 V X114 V -X148

C15: -X8 V-X16 V X37 V X39 V X52 V X59 V X100 V X104 V X167 V-X178 V-X199

C16: -X19 V-x31 V X40 V-x74 V-X86 V X89 V -X100 V X141 V X156 V X177 V-X187 V x191

C17: -X5 V-x85 V X114 V X119 V x166 V x196 V-x199

C18: -X20 v -x192

C19: X20 V X83 V X107 V X119 V -X127 V X163 V-X165

C20: -X24 V -X59 V X106 V -X128 V X138 V-X147 V X157 V-x191 V-x194 v x196

C21: -X74 V -X102 V X118 V X169 V-X178

C22: -X7 V-x16 V X25 V X52 V X89 V-x142 V X153 V X161 V-X173

C23: -X10 V-x51 V-x52 V x85 V x106 v x159 v x197

C24: X17 V -X40 V -X57 V X58 V -X79 V X111 V-X138V X141

C25: -X43 V X91 V-x114 V X118 V X119 V X182 V x193

C26: -X10 V X20 V X151 V-x192 V-x196

C27: -X15 V X47 V -X71 V X120 V X144 V-X178 V-X184 V-X193

C28: X38

C29: X37 V X99 V -X117 V-x137 V-X150 V X152 V-X155V X158

The result is:

0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000

The subsequence is:

C0: -X8 V-x23 V x39 V-x74 v x182

C1: -X63 V-x113 V x123 V-x136

C2: x36 v-x42 V x57 v x67 v x71

C3: X55 V -X65 V -X84 V -X87 V -X146 V-X183

C4: -X49 V-x50 V X71 Vx91 V -X103 V X104 V-x115 V x136c5: -x25 V x75 V-x93 V X107 V-X118 V x121 V-X163

C6: -X37 V X42 V -X54 V X99 V X149 V-X183

C7: -X14 V -X49 V x63 V-x122 V x130 v x155

C8: X5 V-x67 V-x70 V-x85 V X108 V X111 V-X177

C9: X154

C10: -X125 V -X127 V-X135 V -X196

C11: -X62 V -X81 V X102 V x124 V-X179

C12: -X8 V-X35 V x73 V-x121 V X180 V X183 V X192 V-X193

C13: X40 V-x65 V -X86 V -X126 V x129 v x150

C14: X21 V X73 V -X75 V X104 V -X129 V x148 V x170 v x175

C15: X2 V X35 V X102 V-x174

C16: X121 V X133 V -X144 V-X169 V-X192

C17: X37 V-x43 V x47 V x68 V x76 V-x80 V-x84 V-x88 V-x98 V x116 V x122 V x199

C18: X7 V X83 V X92 V X98 V X131 V-X193

C19: -X23 V X46 V -X91 V-x95 V -X101 V X110 V-x112 V-x129 V x148 V x179

C20: -X18 V-x66 V-x94 V x133 V x139 v x172

C21: X25 V X58 V X74 V x135 V-x166 v x168

C22: -X6 V x27 V-x30 V x67 V x159 v x188

C23: X7 V X27 V-x63 V X77 V -X106 V x167 V x185 V-X188

C24: -X23 V X42 V X46 V X148 V-X155 V X172 V X168 V X172 V-x187

C25: -X10 V X19 V -X79 V-X80

C26: -X14 V-x33 V x37 V-x58 V-x86 V x138 V-X179

C27: X22 V-x38 V -X61

C28: X24 V X30 V -X54 V -X61 V-x77 V -X129 V X134 V -X148 V-X160 V-X190 V-X195

C29: X48 V x98 V x104 v x135

The result is:

00000111100100000000011110000011000000000000000110101110000000000001100000011111000000000001000000000000000000000000000000100000000000000011000000001000001100000000000001000000011110000010000001111100

(2) The number of logical variables is 300

The subsequence is:

C0: X87 V-X175 V -X181 V-X238

C1: X1 V X52 V X58 V X74 V X99 V X119 V-X194

C2: -X46 V-x82 V x100 V X103 V X108 V X130 V X136 V X275 V X286 V X296C3: X4 V-x11 V-x127 V-X147 V-X149 V-X173 V-x200 V -X218 V-x283 V-x294

C4: -X23 V-x76 V x161 V-x189 V x219

C5: X36 V X37 V X40 V-x58 V -X69 V -X114 V x133 V X158 V X286

C6: X36 V-x74 V X105 V X108 V X135 V X146 V X186 V X225 V-x285

C7: -X36 V-x38 V x154 V x225 V-x268

C8: -X20 V X58 V -X156 V X260 V x293 V-x297

C9: X13 V-x50 V x68 V x97 V-x177 V-x216 V-x228 V-x259 v x266 v x281

C10: -X71 V -X141 V x151 V x210

C11: X190 V x234 V-x280

C12: X25 V-x28 V-x29 V X93 V -X150

C13: X15 V X18 V-x54 V-x66 V x152 V-x174 V x187 V-x195 v x237 v x281

C14: -X0 V x4 v x237 v x244

C15: X111 V X151 V x198

C16: -X25 V X41 V -X64 V-x91 V-x137 V x140 V x181 v x225

C17: X71 V X72 V X77 V X130 V X144 V-x264 V x290 V-x293

C18: -X36 V-x51 V X116 V X150 V-x156 V x167 V x215 v x281 V-x296

C19: X42 V X53 V X66 V X71 V-x73 V X103 V X169

C20: X9 V X52 V-x116 V-x188 V x199 V-x227 V x228 V-x231

C21: X11 V X37 V -X48 V x73 V x102 v x153

C22: X37 V -X43 V -X62 V X71 V-x76 V x95 V-x125 V x195 V x232 V-x259 v x297

C23: X25 V-X37 V X105 V x137 V-x182 V x189 V-x212 V x216 V-x252 V-x278

C24: -X83 V X84 V X97 V X108 V-x125 V X183 V X184 VX232 V-x260 V x263

C25: -X6 V-x43 V X108 V X235 V x247 V x286 v x289

C26: X38 V X81 V-x116 V X249 V X250 V X259 V x289 V-x295

C27: -X25 V -X59 V-x96 V-x122 V x131 V x179 V x190 V-x292

C28: -X55 V -X89 V X109 V-X151 V x197 V-x264 V-x289

C29: X24 V-x38 V x84 V-x178 v x194

The result is:

000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000111100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 clause set is:

C0: X58 V -X79 V X109 V-x179 v x298

C1: -X23 V X43 V -X52 V-x87 V-x222 V x258 V-x284 V x288

C2: -X38 V-x59 V x67 V-x71 V-x99 V x123 V-x278

C3: X1 v-x3 V-x11 V X42 V-x97 V x137 V-x143 V x152

C4: X30 V-x43 V -X81 V X141 V-x149 V x164 V x186 V-x191 V x261

C5: -X8 V-x10 V-x46 V-x47 V x147 V x234 V x250 v x271

C6: -X8 V-x25 V-x53 V-x64 V x267 V-x273

C7: -X56 V X87 V X101 V X151 V X160 V X167 V X181 V X189 V-x214 V x226

C8: X8 V-x28 V x47 V x85 V x118 V-x220 v x268

C9: -X33 V-x98 V -X136 V X142 V -X208 V X218 V-x260 V x286 V x290

C10: -X18 V X40 V -X42 V x87 V-x107 V x114 V x128 v x138 v x197

C11: X33 V-x46 V -X76 V X113 V -X198 V-x232 V x255

C12: -X18 V X66 V -X207 V-x233 V x236 v x254

C13: -X10 V-x63 V-x79 V x82 V-x190 V x198 V x288

C14: -X70 V-x74 V x88 v x166

C15: -X8 V-x28 V X51 V X103 V X106 V X152 V X157 V X191 V X252 V X259 V X268 V X280 V X291 V X296

C16: -X1 V X9 V -X24 V x137 V X142 V X146 V X154 V X222 V x226 V x239

C17: -X25 V X90 V -X94 V-X185 V x269 V-x284

C18: X69 V-x210 V x232 V x266 v x273

C19: X22 V -X41 V-x50 V-x57 V X112 V X191 V X195 V-X203 V-x262

C20: -X30 V-x79 V X157 V X182 V-x214 V x274 V -X281

C21: -X26 V X110 V X127 V X159 V X206 V X220 V-x225 V X271 V-x278 V-x282

C22: x133

C23: X2 V-x5 V -X31 V-X141 V-X192

C24: X113 V X118 V X210 V X283C25: -X6 V X254 V X271 V X254 V X271 V X254 V X271 V X273

C26: -X144 V x191 V x194 V x251 V-x262

C27: X27 V X113 V -X151 V-X167 V -X174 V x202

C28: X5 V X6 V X106 V X160 V X165 V-X171 V X211 V-x255 V x265

C29: -X83 V X105 V -X157 V -X248 V-x268 V-x284

The result is:

000010000000000000000000000000000000000000001110000000000000000000000000000000000000000000000000000000010000000000000000000000000000110000000000000000000000000000000000000000000000010000000000000011110000000000000001111100000000000000000000000000000000000000000000000000010000000000000000000000000000