由SAT问题展开说（3）
附录：
1， SetTime函数如下：
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=strTime+_h.ToString()+"h "+_m.ToString()+"m "
+_s.ToString()+"s "+_ms.ToString()+"ms ";
}
2，保存子句集与计算结果的代码为：
private void saveFileDlg_FileOk(object sender, System.ComponentModel.CancelEventArgs e)
{
if(saveFileDlg.FileName!=null&&chlistBox.Items[0].ToString()!=null)
{
FileInfo theSourceFile=new FileInfo(saveFileDlg.FileName);
StreamWriter writer=new StreamWriter(saveFileDlg.FileName,true);
string text;
writer.WriteLine("子句集是：");
for(int i=0;i<maxNum;i++)
{
text=chlistBox.Items[i].ToString();
writer.WriteLine("C"+i.ToString()+" : "+text);
}
writer.WriteLine("目前结果是：");
text=oneSAT.Best.ToString();
writer.WriteLine(text);
writer.Close();
}
}
3，四次实验的子句集分别为：
（1）逻辑变量数目为200的
子句集是：
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 -x118 V -x126 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 -x171
C7 : 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 -x135 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 -x138 V x141
C25 : -x43 V x91 V -x114 V x118 V x119 V -x128 V x135 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 -x155 V x158
目前结果是：
00000000000000010000000000000000000011100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000011000000000000000000000000000000000
子句集是：
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 -x56 V -x60 V x71 V -x91 V -x103 V x104 V -x115 V x136
C5 : -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 -x130 V -x171 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 -x189 V x194 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 -x164 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
目前结果是：
00000111100100000000011110000011000000000000000110101110000000000001100000011111000000000001000000000000000000000000000000100000000000000011000000001000001100000000000001000000011110000010000001111100
（2）逻辑变量数目为300的
子句集是：
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 -x182 V x255 V x275 V x286 V x296
C3 : 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 -x181 V x245 V x286
C6 : x36 V -x74 V x105 V x108 V x135 V x146 V -x169 V -x177 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 -x146 V x149 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 V -x232 V -x260 V x263
C25 : -x6 V -x43 V x108 V -x115 V -x208 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
目前结果是：
000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000111100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
子句集是：
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 -x164 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 -x201 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 -x169 V -x194 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 -x250 V x257 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 -x229 V -x248 V x271 V -x278 V -x282
C22 : x133
C23 : x2 V -x5 V -x31 V -x141 V -x192
C24 : x113 V x118 V -x126 V x129 V x210 V x283
C25 : -x6 V -x19 V x67 V x97 V x217 V -x227 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
目前结果是：
000010000000000000000000000000000000000000001110000000000000000000000000000000000000000000000000000000010000000000000000000000000000110000000000000000000000000000000000000000000000010000000000000011110000000000000001111100000000000000000000000000000000000000000000000000010000000000000000000000000000
