C++实现基于SAT的数独游戏求解程序

╰半橙微兮° 2024-04-01 13:59 72阅读 0赞

1引言 1  
1.1 课题背景与意义 1  
1.2 国内外研究现状 1  
1.3 课程设计的主要研究工作 1  
2 系统需求分析与总体设计 1  
2.1 系统需求分析 2  
2.2 系统总体设计 2  
3 系统详细设计 3  
3.1 有关数据结构的定义 3  
3.2 主要算法设计 4  
4.系统实现与测试 11  
4.1 系统实现 11  
4.2 系统测试 19  
4.3程序优化 23  
5 总结与展望 24  
5.1 全文总结 25  
5.1 工作展望 25  
6体会 26  
附录 27

1.  主程序 27
2.  文件操作 31
3.  SAT求解，DPLL算法核心框架 32
4.  数独求解模块 51  
    2 系统需求分析与总体设计  
    2.1 系统需求分析  
    本设计基于DPLL的算法与程序框架，实现一个完备SAT求解器，包括程序的改进也必须在此算法的基础上进行，对输入的CNF范式算例文件，解析并建立其内部表示；精心设计问题中变元、文字、子句、公式等有效的物理存储结构以及一定的分支变元处理策略，使求解器具有优化的执行性能；对一定规模的算例能有效求解，输出与文件保存求解结果，统计求解时间。  
    这部分应该写的是用户需求，明确你做的系统要实现的目标，能处理一些什么样的事务、事务处理流程等。  
    2.2 系统总体设计  
    这部分可根据用户需求，设计和规划一个系统，说明清楚系统应该有哪些功能模块，每个模块做什么。最后给出完整的系统模块结构图。  
    本任务只要包括六个主要的版块。  
    （1）输入输出功能，即执行参数的输入，SAT算例cnf文件的读取，执行结果的输出与文件保存；  
    （2）公式解析与验证：读取cnf算例文件，解析文件，基于裂解表的物理结构，建立公式的内部表示；并实现对解析正确性的验证功能，即遍历内部结构逐行输出与显示每个子句，与输入算例对比可人工判断解析功能的正确性。  
    （3）DPLL过程：基于DPLL算法框架，实现SAT算例的求解。  
    （4）时间性能的测量：基于相应的时间处理函数，记录DPLL过程执行时间（以毫秒为单位），并作为输出信息的一部分。  
    （5）程序优化：对基本DPLL的实现进行存储结构、分支变元选取策略\[1-3\]等某一方面进行优化设计与实现，提供较明确的性能优化率结果。优化率的计算公式为：\[(t-to)/t\]\*100%,其中t 为未对DPLL优化时求解基准算例的执行时间，to则为优化DPLL实现时求解同一算例的执行时间。  
    以下是文中有图标的形式，本文转载自http://www.biyezuopin.vip/onews.asp?id=16990要求对图标引用说明。  
    （6）SAT应用：将数独游戏问题转化为SAT问题，并集成到上面的求解器进行问题求解，游戏可玩，具有一定的/简单的交互性。  
    其完整的系统模块结构图如图2-1所示。  
    ![在这里插入图片描述][0da3b095fb6647998d5276e796938455.png]

图2-1 系统模块结构图

#include <stdio.h>
    #include <stdlib.h>
    #include <string.h>
    #include <time.h>
    #include <memory.h>
    #include <algorithm>
    #define ERROR 0
    //#define OK 1
    #define max 9
    #define min 1
    //#define ERROR 0
    #define OK 1
    #define NumClaus 20000
    #define MAXLIST 20000
    #define INITIALIZATION 9999
    #define FLEN 100
    
    typedef int status;
    typedef struct Record_Data_status
    {
        
    	status Data;//保存的数据
    	status positive_text;//正文字
    	status negative_text;//负文字
    }*Record_Data_status_list;
    typedef struct Data_status {
        
    	status Data;
    	status Data_situation;
    }Data_statusp[MAXLIST];
    typedef struct Clause {
        
    	Data_status elem;
    	struct Clause *next;
    }Clause, *ClauseList;
    //子句结点类型定义
    typedef struct LnodeClause {
        
    	Clause *firstnode;
    	int num_positive_text;//正文字个数
    	int num_negative_text;//负文字个数
    	int ClauseNum;//记录该字句的单子句数目
    	int Number_of_assigned_words;//未赋值字句数量
    	int Determine;//判断该字句的真假状态 0 为假 ，1 为真，-1 为不确定
    }LnodeClause, LnodeClausep[MAXLIST];
    typedef struct MyList {
        
    	LnodeClausep vertices;
    	int num, numLine;
    }MyList;
    typedef struct Association_Clause {
        
    	status num;
    	Association_Clause *next;
    };
    typedef struct Decide_buffer {
        //文字计数器
    	status Data;
    	status Data_status;
    	int num_positive_text;//正文字个数
    	int num_negative_text;//负文字个数
    	int total_number;//正负文字总数
    	Clause *firstnode;
    };
    typedef struct Association_Data {
        
    	status Data;
    	status mark_num;
    	int totalNum;
    };
    status creatClaus(MyList *NewList, status ID, status key, Decide_buffer *Decide_buf, Association_Data *Record_Data);
    status destoryClause(MyList *NewList, status num);//销毁单子句
    status DestoryDecide_buf(Decide_buffer *Decide_buf, int i);
    status Destory(MyList *NewList, Decide_buffer *Decide_buf, Association_Data *Record_Data);
    status isUnitClause(MyList *NewList);//判断是否为单子句*/
    status evaluateClause(MyList *NewList, status id);//评估字句的真假状态
    status evalute_All_Cluase(MyList *NewList);//判断CNF文件字句的真假状态
    										   //status variable_decided();//从子句集中选择一个没有赋值的变量为其赋值，赋值成功
    										   //返回 1 ；若所有变量均已被赋值，则说明问题可满足
    status bcp_deduce(MyList *NewList, status j_index, status p_n_text, Association_Data *Record_Data, Decide_buffer *Decide_buf);//执行BCP过程
    status Conflict(MyList *NewList);
    status DPLL(MyList *NewList, int index_j, status temp_p_n_text, Association_Data *Record_Data, Decide_buffer *Decide_buf);
    void BackTrack_Initilization(MyList *NewList, status j_index, Association_Data *Record_Data, Decide_buffer *Decide_buf);
    status Check_repet_ID(Decide_buffer *Decide_buf, status key, status ID);
    void print2(MyList *NewList, Association_Data *Record_Data, Decide_buffer *Decide_buf);
    void print3(MyList *NewList, status Data, Decide_buffer *Decide_buf);
    void print(MyList *NewList, Association_Data *Record_Data, Decide_buffer *Decide_buf, status index);

![在这里插入图片描述][9f315af53fed4a14b9220f3cfc99cd82.png_pic_center]  
![在这里插入图片描述][2458778b06484b9b9f293cd89b99fbb7.png_pic_center]  
![在这里插入图片描述][1c3c2728aedc48b186c4a7ff4eeef163.png_pic_center]  
![在这里插入图片描述][a9ce675db9244e738958c24aa0388ae8.png_pic_center]  
![在这里插入图片描述][531ba908c2eb44f28531cba49a6ee980.png_pic_center]  
![在这里插入图片描述][1df5e4f6dd324e2d98f6ed8fc7d95687.png_pic_center]  
![在这里插入图片描述][a314050bda1a4ad0b5313523d1e9f845.png_pic_center]  
![在这里插入图片描述][fe47a10e5e3a4d28a955b79e86c6179a.png_pic_center]  
![在这里插入图片描述][d33227d9ed4e4dd4a76f8b4a6e9d503f.png_pic_center]  
![在这里插入图片描述][23fe8115a41446e7a3f5354d92492e0b.png_pic_center]  
![在这里插入图片描述][730be15070a343b7b89298d6d229f97a.png_pic_center]  
![在这里插入图片描述][32eeff188d4444f08e65187274a45149.png_pic_center]  
![在这里插入图片描述][62a7eafb385d4d8d837af69c6be58004.png_pic_center]  
![在这里插入图片描述][c6651b8e5d714333965cc01745781d8d.png_pic_center]  
![在这里插入图片描述][0d418538d5c947d9a8ff2925659e9d60.png_pic_center]  
![在这里插入图片描述][b3cebefb99554f7eb2aa1121d01acc35.png_pic_center]  
![在这里插入图片描述][efa1f60c8fda47b294d3aefa57cf8195.png_pic_center]

[0da3b095fb6647998d5276e796938455.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/471274c2cac84b3cb6417a8c3298df10.png
[9f315af53fed4a14b9220f3cfc99cd82.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/9b9f2c643ed54070b5763cbcfab13adb.png
[2458778b06484b9b9f293cd89b99fbb7.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/f5302752a1314f3db6947189c63e226c.png
[1c3c2728aedc48b186c4a7ff4eeef163.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/bc165f062793494c88c10d5406285421.png
[a9ce675db9244e738958c24aa0388ae8.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/968b8db4683e45c59d1e4da28cb8952e.png
[531ba908c2eb44f28531cba49a6ee980.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/08d84f865990494391d3333aebbf9e3c.png
[1df5e4f6dd324e2d98f6ed8fc7d95687.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/54d9e94cc8bf479cac0385680fcb4c2f.png
[a314050bda1a4ad0b5313523d1e9f845.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/22c03600744e4d21b1802aaca5c58d00.png
[fe47a10e5e3a4d28a955b79e86c6179a.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/4045195844fa42c9a690ed3a7fc6bbf7.png
[d33227d9ed4e4dd4a76f8b4a6e9d503f.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/acd5eed5ce30493a95ae29453dd51148.png
[23fe8115a41446e7a3f5354d92492e0b.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/7e4fcf96267348278018d51d4d0ac0a5.png
[730be15070a343b7b89298d6d229f97a.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/9a4b7715683c480184063f9ade7d9d52.png
[32eeff188d4444f08e65187274a45149.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/0e1e16c136364cd98c92386907786fc4.png
[62a7eafb385d4d8d837af69c6be58004.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/b10222b05ebc458b8091665895d0e188.png
[c6651b8e5d714333965cc01745781d8d.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/86ddafe1424b4482b70cd8e509cd9cd1.png
[0d418538d5c947d9a8ff2925659e9d60.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/6abd9362fc32489e9640fd6573f06252.png
[b3cebefb99554f7eb2aa1121d01acc35.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/8b0e5623c6a24971a25285be719d359a.png
[efa1f60c8fda47b294d3aefa57cf8195.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/fee1fa2d223b487e92b8f24acba00215.png