-
基于C++和QT实现的二进制数独游戏求解
目 录
任 务 书 3
设计内容 3
设计要求 3
参考文献 4
1 引言 6
1.1 课题背景与意义 6
1.1.1 课程目标 6
1.1.2 课程任务 7
1.2 国内外研究现状 7
1.3 课程设计的主要研究工作 9
2 系统需求分析与总体设计 10
2.1 系统需求分析 10
2.2 系统总体设计 10
3 系统详细设计 12
3.1 有关数据结构的定义 12
3.2主要算法设计 13
3.2.1 CNF文件处理 13
3.2.2 DPLL算法处理 14
3.2.3 DPLL算法优化方案 17
3.2.4 二进制数独处理 17
4 系统实现与测试 20
5.总结与展望 41
5.1 全文总结 41
5.2工作展望 41
6. 体会 43
参考文献 44
附录 45
1.3 课程设计的主要研究工作本设计要求精心设计问题中变元、文字、子句、公式等有效的物理存储结构，基于DPLL过程实现一个高效SAT求解器，对于给定的中小规模算例进行求解，输出求解结果，统计求解时间。在此基础上，通过改进算法、使用不同的选择策略和物理存储结构来优化求解过程，使求解器能更快地求解。完成基于此算法的数独游戏，通过将数独归约成SAT问题进行求解。
2 系统需求分析与总体设计
2.1 系统需求分析
(1)基于DPLL算法实现一个高效的SAT求解器，对于给定的中小规模测试算例进行求解，能输出求解结果和求解时间。
a)能够读取文件, 输出执行时间和执行结果
b)能够保存文件结果
c)能够对计算出的结果进行正确性验证
d)能够输出读取的文件
(2)数独游戏。将数独游戏转化为SAT问题进行求解，并具有一定的可玩性和交互性，要求如下：
a)能够生成数独格局
b)能将数独转化为SAT文件并导出CNF文件
c)能随机生成数独格局
d)能将求解结果化为数独的解
2.2 系统总体设计
本系统主要有3个模块，如下：
(1)SAT求解模块
a)读取CNF文件并将其转化为设计的数据结构
b)可以查看并输出读入的CNF文件及相关信息(子句数，变元数)
c)保存求解结果
d)根据DPLL算法输出求解结果
(2)输出模块
a)将SAT求解结果和求解时间输出到控制台(包括是否可解)
b)将最终结果以文件形式保存
(3)数独模块
a)随机生成数独布局
b)能够选择特定空位置输入游玩
c)将数独转化为SAT问题求解
d)使用Qt实现的GUI界面，可玩性较强
http://www.biyezuopin.vip/onews.asp?id=16994
流程图如下所示：
图2-2 系统模块流程图#include "define.h" int main(void) { for(i=0;i<2000;i++) { nums[i] = 0; } char filename[200], copy_filename[200]; //cnf文件读取 与结果保存 char sudo_filename[20]; //数独文件 int op = 1, SAT = 1, SuDoKu = 1; //用于switch分支 int flag_cnf = 0; //用于判断cnf文件是否读取成功 int flag_sudo = 0; //用于判断数独文件是否读取成功 int way_sudo = 0; //sudo处理方式 struct Clause * root; while(op) { printf("|--------------------Choose SAT or BinaryPuzzle--------------------|\n"); printf("| |\n"); printf("| 1.SAT 2.BinaryPuzzle |\n"); printf("| |\n"); printf("| 0.Exit |\n"); printf("| |\n"); printf("| CopyRight @CS1906 LX |\n"); printf("| |\n"); printf("|------------------------------------------------------------------|\n"); printf("| |\n"); printf("| Make your choice ( 0 - 2 ) |\n"); printf("| |\n"); printf("|------------------------------------------------------------------|\n"); scanf("%d",&op); switch(op) { case 1: while(SAT){ printf("|-------------------------- Menu For SAT --------------------------|\n"); printf("| |\n"); printf("| 1.Readfile 2.Savefile |\n"); printf("| |\n"); printf("| 3.Traversefile 4.Dpll |\n"); printf("| |\n"); printf("| 0.Exit |\n"); printf("| |\n"); printf("| CopyRight @CS1906 LX |\n"); printf("| |\n"); printf("|------------------------------------------------------------------|\n"); printf("| |\n"); printf("| Make your choice ( 0 - 4 ) |\n"); printf("| |\n"); printf("|------------------------------------------------------------------|\n"); scanf("%d",&SAT); switch(SAT) { case 1: for(i=0;i<2000;i++) { nums[i] = 0; } printf("请输入读取的cnf文件名:\n"); scanf("%s", filename); strcpy(copy_filename, filename); root = Readfile(filename); if (root != NULL) { printf("文件读取成功\n"); flag_cnf = 1; } else { printf("文件读取失败！\n"); } getchar(); printf("请输入c继续：\n"); getchar(); break; case 2: { if (flag_cnf) { if (Savefile(root)) { printf("文件保存成功！\n"); } else { printf("文件保存失败！\n"); } } else printf("文件还未读取！\n"); getchar(); printf("请输入c继续：\n"); getchar(); break; } case 3: { if(flag_cnf) Traversefile(root); else printf("文件还未读取！\n"); getchar(); printf("请输入c继续：\n"); getchar(); break; } case 4: { if(flag_cnf) { printf("请选取求解方式:\n"); printf("1.优化前 2.优化后\n"); scanf("%d",&Way); clock_t start,end; start = clock(); if(dpll(root)==OK) { end = clock(); printf("文件有解!\n"); printf(" \n"); printf("求解时间:%d ms\n",(end-start)*1000/CLOCKS_PER_SEC); for(i=1;i<=word_number;i++) { temp = (variable[i] ==0 ?-1:1)*i; printf("%d ",temp); if(i%10==0) putchar('\n'); } putchar('\n'); writeResult(copy_filename,1,(end-start)*1000/CLOCKS_PER_SEC); } else { end = clock(); printf("文件无解！\n"); printf(" \n"); printf("求解时间:%d ms\n",(end-start)*1000/CLOCKS_PER_SEC); putchar('\n'); writeResult(copy_filename,0,(end-start)*1000/CLOCKS_PER_SEC); } flag_cnf = 0; //destroyClauses(root); } else{ printf("文件还未读取!\n"); } getchar(); printf("请输入c继续：\n"); getchar(); break; } case 0:{ break; } default: { printf("输入错误！\n"); getchar(); printf("请输入c继续：\n"); getchar(); break; } } } getchar(); printf("请输入c继续：\n"); getchar(); break; case 2: while(SuDoKu) { //system("cls"); printf("|--------------------- Menu For BinaryPuzzle --------------------|\n"); printf("| |\n"); printf("| 1.ReadSudoKuFile 2.Play |\n"); printf("| |\n"); printf("| 3.SetCNFfile 4.Dpll For Answer Check |\n"); printf("| |\n"); printf("| 5.Randomly Generate 0.Exit |\n"); printf("| |\n"); printf("| CopyRight @CS1906 LX |\n"); printf("| |\n"); printf("|------------------------------------------------------------------|\n"); printf("| |\n"); printf("| Make your choice ( 0 - 4 ) |\n"); printf("| |\n"); printf("|------------------------------------------------------------------|\n"); scanf("%d",&SuDoKu); switch(SuDoKu) { case 1: printf("请输入要读取的数独棋盘文件名:\n"); scanf("%s",sudo_filename); Readqipan(sudo_filename); Showqipan(qipan); flag_sudo = 1; getchar(); printf("请输入c继续：\n"); getchar(); break; case 2: if(flag_sudo) PlaySuDoKu(qipan); else printf("数独文件还未读取!\n"); getchar(); printf("请输入c继续：\n"); getchar(); break; case 3: if(flag_sudo) { printf("请选择:\n1.直接求解 2.检验Play后的结果！\n"); scanf("%d",&way_sudo); if(way_sudo==1) { Resetqipan(qipan); SetCNFfile(qipan); } else { if(Checkqipan(qipan)) SetCNFfile(qipan); else printf("棋盘还未填充完整,请填充完毕!\n"); } } else printf("数独文件还未读取!\n"); getchar(); printf("请输入c继续：\n"); getchar(); break; case 4: if(flag_sudo){ char filename_sudocopy[15]; strcpy(filename_sudocopy,filename_setcnf); struct Clause * root_sudo = Readfile(filename_sudocopy); clock_t t1,t2; t1 = clock(); if(dpll(root_sudo) == OK){ t2 = clock(); char file_sudoresult[15]; strcpy(file_sudoresult,filename_sudocopy); if(way_sudo == 1){ printf("Dpll求解成功！结果为:\n"); for(i = 0 ; i<36; i++) { printf("%d ", variable[i+1]); if((i+1) % 6 == 0) putchar('\n'); } } else { printf("Dpll求解成功，结果正确!\n"); writeResult(file_sudoresult,1,t2-t1); //destroyClauses(root_sudo); } } else printf("Dpll求解失败,结果错误!\n可继续尝试！\n"); } else printf("数独文件还未读取！\n"); getchar(); printf("请输入c继续：\n"); getchar(); break; case 5: { char *random_filename[]={"StanSudo_1.txt","StanSudo_2.txt","StanSudo_3.txt","StanSudo_4.txt","StanSudo_5.txt"}; srand((unsigned)time(NULL)); int z =rand()%5; RandGener(random_filename[z]); Showqipan(qipan); flag_sudo = 1; getchar(); printf("请输入c继续：\n"); getchar(); break; } case 0: break; default: printf("输入错误!\n"); getchar(); printf("请输入c继续：\n"); getchar(); break; } } case 0: break; default: printf("输入错误！\n"); getchar(); printf("请输入c继续：\n"); getchar(); break; } } printf("下次再见！\n"); return 0; }- 1
- 2
- 3
- 4
- 5
- 6
- 7
- 8
- 9
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
- 67
- 68
- 69
- 70
- 71
- 72
- 73
- 74
- 75
- 76
- 77
- 78
- 79
- 80
- 81
- 82
- 83
- 84
- 85
- 86
- 87
- 88
- 89
- 90
- 91
- 92
- 93
- 94
- 95
- 96
- 97
- 98
- 99
- 100
- 101
- 102
- 103
- 104
- 105
- 106
- 107
- 108
- 109
- 110
- 111
- 112
- 113
- 114
- 115
- 116
- 117
- 118
- 119
- 120
- 121
- 122
- 123
- 124
- 125
- 126
- 127
- 128
- 129
- 130
- 131
- 132
- 133
- 134
- 135
- 136
- 137
- 138
- 139
- 140
- 141
- 142
- 143
- 144
- 145
- 146
- 147
- 148
- 149
- 150
- 151
- 152
- 153
- 154
- 155
- 156
- 157
- 158
- 159
- 160
- 161
- 162
- 163
- 164
- 165
- 166
- 167
- 168
- 169
- 170
- 171
- 172
- 173
- 174
- 175
- 176
- 177
- 178
- 179
- 180
- 181
- 182
- 183
- 184
- 185
- 186
- 187
- 188
- 189
- 190
- 191
- 192
- 193
- 194
- 195
- 196
- 197
- 198
- 199
- 200
- 201
- 202
- 203
- 204
- 205
- 206
- 207
- 208
- 209
- 210
- 211
- 212
- 213
- 214
- 215
- 216
- 217
- 218
- 219
- 220
- 221
- 222
- 223
- 224
- 225
- 226
- 227
- 228
- 229
- 230
- 231
- 232
- 233
- 234
- 235
- 236
- 237
- 238
- 239
- 240
- 241
- 242
- 243
- 244
- 245
- 246
- 247
- 248
- 249
- 250
- 251
- 252
- 253
- 254
- 255
- 256
- 257
- 258
- 259
- 260
- 261
- 262
- 263
- 264
- 265
- 266
- 267
- 268
- 269
- 270
- 271
- 272
- 273
- 274
- 275
- 276
- 277
- 278
- 279
- 280
- 281
- 282
- 283
- 284
- 285
- 286
- 287
- 288
- 289
- 290
- 291
- 292
- 293
- 294
- 295
- 296
- 297
- 298
-
相关阅读:
哪个品牌护眼台灯最好用？书客、爱德华、雷士对比实测横评！
PMP证书在国内已经泛滥了,大家怎么看?
js数组介绍：创建、length的用法、冒泡排序法、选择排序法
游戏设计模式专栏(七）：在Cocos游戏开发中运用桥接模式
Maven程序 tomcat插件安装与web工程启动
3.2python使用 matplotlib 实现可视化_python量化实用版教程(初级)
Python 元类详解
GDB用法
【源码解读(一)】EFCORE源码解读之创建DBContext查询拦截
C++ Primer 类与构造函数 三五法则
- 原文地址：https://blog.csdn.net/newlw/article/details/127683173
