基于DPLL算法实现的完备SAT求解器的数独求解程序

小咪咪 2024-02-21 08:51 9阅读 0赞

目录  
任务书 I  
1.引言 1  
1.1课题背景与意义 1  
1.2国内外研究现状 2  
1.3课程设计的主要研究工作 3  
2.系统需求分析与总体设计 4  
2.1系统需求分析 4  
2.2系统总体设计 4  
3.系统详细设计 6  
3.1有关数据结构的定义 6  
3.2主要算法设计 9  
4.系统实现与测试 13  
4.1系统实现 13  
4.2系统测试 20  
5.总结与展望 32  
5.1全文总结 32  
5.2工作展望 32  
6.体会 33  
参考文献 34  
尽管SAT算法已经取得了举足轻重的改进，但是仍有一些问题没有得到高效的解决，已经解决的问题可能还存在更好的求解算法，因此研究并实现高效率的求解算法仍是当前要解决的中心问题之一。  
1.3课程设计的主要研究工作  
（1）对SAT问题的研究背景、意义及现状进行了简要总结，学习了命题逻辑可满足性问题的基本理论知识。  
（2）基于DPLL算法实现一个完备性的SAT问题求解器，能够用来求解一定规模的SAT问题。  
（3）对实现的SAT求解器进行优化，提高效率，改善其时间复杂度，从而用更少的时间求解更大规模的SAT问题。  
（4）将数独求解问题转换成SAT问题，并基于实现的SAT求解器编写一个数独求解程序。  
（5）基于数独求解程序开发出一个可以随机生成数独并具有一定可玩性的数独游戏。  
2.1系统需求分析  
（1）输入输出功能：包括程序执行参数的输入，SAT算例cnf文件的读取，执行结果的输出与文件保存等。  
（2）公式解析与验证：读取cnf算例文件，解析文件，基于一定的物理结构，建立公式的内部表示；并实现对解析正确性的验证功能，即遍历内部结构逐行输出与显示每个子句。  
（3）DPLL过程：基于DPLL算法框架，实现SAT算例的求解。  
（4）时间性能的测量：基于相应的时间处理函数，记录DPLL过程执行时间（以毫秒为单位），并作为输出信息的一部分。  
（5）SAT应用：将数独游戏问题转化为SAT问题，并集成到上面的求解器进行问题求解，游戏可玩，具有一定的/简单的交互性。

#include "sat.h"
    
    int main(int argc, char *argv[])
    {
          
        int option = -1;
        while (option) {
        
            system("cls");
            printf("请选择功能:\n"
                   "1:解析cnf文件.\n"
                   "2:求解sat问题.\n"
                   "3:求解数独.\n"
                   "4:自动生成数独并求解.\n"
                   "0:退出.\n");
            while (!scanf("%d", &option)) {
        
                printf("输入无效，请重新输入\n");
                while (getchar() != '\n');
            }
            while (getchar() != '\n');
    
            switch (option)
            {
                
            case 1: {
        
                printf("请输入cnf文件路径\n");
                char fileName[1000];
    
                //验证输入的路径，确保是有效的cnf文件路径
                do {
        
                    fgets(fileName, 1000, stdin);
                    int length = strlen(fileName);
                    if (length < 4) {
        
                        printf("请输入正确的cnf文件路径\n");
                        continue;
                    }
                    fileName[length - 1] = '\0';
                    if (fileName[length - 2] != 'f' || fileName[length - 3] != 'n' || fileName[length - 4] != 'c')
                        printf("输入的文件类型无效，请输入cnf文件的路径\n");
                    else
                        break;
                } while (TRUE);
    
                ParseCnfFile(fileName);
                break;
            }
            case 2: {
        
                SAT();
                break;
            }        
            case 3: {
        
                printf("请输入数独，未知位置请用0代替，9个数字一行\n");
                char sudoku[9][9];
                for (int i = 0; i < 9; ++i) {
        
                    for (int j = 0; j < 9; ++j)
                        sudoku[i][j] = getchar();
                    getchar();
                }
                SolveSudoku(sudoku);
                break;
            }       
            case 4: {
        
                PlaySudoku();
                break;
            }
            default: 
                break;           
            }
        }
        return 0;
    }

![在这里插入图片描述][d9313d49aff54b35a626a6dd7ec0acfe.png_pic_center]  
![在这里插入图片描述][f78e4135d22c422facbd61ba813750a8.png_pic_center]  
![在这里插入图片描述][e5741b8858ee47bfa83c1d8334690588.png_pic_center]  
![在这里插入图片描述][bb5f57e6601d46848e745ba26cb561fb.png_pic_center]  
![在这里插入图片描述][1482b6b43bce46a8b859a5ccb072a861.png_pic_center]  
![在这里插入图片描述][befcf0fc926d4a208d4d61845939f2bf.png_pic_center]  
![在这里插入图片描述][575c2aa2a83249c0a8ae32aeae34e575.png_pic_center]  
![在这里插入图片描述][35488d01fc62403a8306245dd5f3b8cf.png_pic_center]  
![在这里插入图片描述][9b6b0ec144a34a0786706affdb16b6f5.png_pic_center]  
![在这里插入图片描述][c268c2e932364bf48ddb6d60d48df71d.png_pic_center]  
![在这里插入图片描述][25dbd0467bc94c5e898751bd6324681d.png_pic_center]  
![在这里插入图片描述][4bd51b5136bc40ffa17cbc37517e4f24.png_pic_center]  
![在这里插入图片描述][3baf0690aa1b42f79249858cad1edca1.png_pic_center]  
![在这里插入图片描述][473294dedf234477a877a4f45d136933.png_pic_center]  
![在这里插入图片描述][347468b259044f57bbba77a52f58c331.png_pic_center]  
![在这里插入图片描述][774e10c649b44881b41eeaedee1be444.png_pic_center]  
![在这里插入图片描述][f587fa5d3c454551a8dbe9100490e8f4.png_pic_center]  
![在这里插入图片描述][0609ee2ea2814fd2b6309ac1062be47e.png_pic_center]  
![在这里插入图片描述][1c2469bbf6a14d8fa259d8ab496e6bad.png_pic_center]  
![在这里插入图片描述][e0bac84ca2d34ca38852ab06806e0717.png_pic_center]  
![在这里插入图片描述][ac469328867c492b8e6ea0e5e02fabed.png_pic_center]  
![在这里插入图片描述][4288cc8595ea47938b6eefdd40571d8c.png_pic_center]  
![在这里插入图片描述][72c295807a1b4c899cca17ca2d42e6d3.png_pic_center]  
![在这里插入图片描述][fd52e77d4f874418b8854f1d367c6f2f.png_pic_center]  
![在这里插入图片描述][80190f4b85ee4ffcbbfd8962f4296c88.png_pic_center]  
![在这里插入图片描述][bb991a66abea46478f82819821fc3dc0.png_pic_center]  
![在这里插入图片描述][3ad4c760b8ed4fd7a15e16f512f9db2c.png_pic_center]

[d9313d49aff54b35a626a6dd7ec0acfe.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/578e56152ab3499a8d242f5c0051d80c.png
[f78e4135d22c422facbd61ba813750a8.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/a558e1f0e77e461eaa6cec4d40538ac6.png
[e5741b8858ee47bfa83c1d8334690588.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/75fedac555f74406bc2dd8a1c97bdbe9.png
[bb5f57e6601d46848e745ba26cb561fb.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/3347edd4961d4cf49bf90418ee0bf0a1.png
[1482b6b43bce46a8b859a5ccb072a861.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/92b1e532fe2c4c279ece7a9ce34204eb.png
[befcf0fc926d4a208d4d61845939f2bf.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/d47f45480a1a4081b057fa8279b3afd2.png
[575c2aa2a83249c0a8ae32aeae34e575.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/4910f779cb924e1eae8e0923425bf904.png
[35488d01fc62403a8306245dd5f3b8cf.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/00af70138d75446da0010bbb3e90d1c7.png
[9b6b0ec144a34a0786706affdb16b6f5.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/23bdd6c62b7a42c3bbcfe312a28d3ece.png
[c268c2e932364bf48ddb6d60d48df71d.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/4824376074484deaa063aa6649c2fda7.png
[25dbd0467bc94c5e898751bd6324681d.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/ecbdd68406194f04bf88855d3fa3daa0.png
[4bd51b5136bc40ffa17cbc37517e4f24.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/8cb8f44076d54971a95709bfdee0eb4d.png
[3baf0690aa1b42f79249858cad1edca1.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/f800a23d64304375b469a881a37947f9.png
[473294dedf234477a877a4f45d136933.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/cd338d408a9a4b2f8e1890c4782be160.png
[347468b259044f57bbba77a52f58c331.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/7c27302d7c2348ec82a1f8577051963e.png
[774e10c649b44881b41eeaedee1be444.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/9df81276fb1a4d76bade5257d5d83937.png
[f587fa5d3c454551a8dbe9100490e8f4.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/83afe54b471f49f8b89c29202037e6df.png
[0609ee2ea2814fd2b6309ac1062be47e.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/5e94e083df0645a9bc32166377a5e859.png
[1c2469bbf6a14d8fa259d8ab496e6bad.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/6066548dde024159b85a2a4b7ecc3ae2.png
[e0bac84ca2d34ca38852ab06806e0717.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/48b83b49d02b4488920f501bd54f5def.png
[ac469328867c492b8e6ea0e5e02fabed.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/3c9d680475a94f548850bd61dc63787e.png
[4288cc8595ea47938b6eefdd40571d8c.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/16b77867429347db8317216b1cf676f3.png
[72c295807a1b4c899cca17ca2d42e6d3.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/dfca52c5d40540eeab6d7b6055be09ff.png
[fd52e77d4f874418b8854f1d367c6f2f.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/8af8509b91f042a1b491948990c45d06.png
[80190f4b85ee4ffcbbfd8962f4296c88.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/5614a9cdc4c945f492844c423480b3d7.png
[bb991a66abea46478f82819821fc3dc0.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/28ba713952c44ec29a2036282915b711.png
[3ad4c760b8ed4fd7a15e16f512f9db2c.png_pic_center]: https://image.dandelioncloud.cn/pgy_files/images/2024/02/21/e5ab2fbf3b664b02aedede39ff02baf1.png