CS1703-U201714668-葛松1

【课程设计报告】题目：基于 SAT 的数独游戏求解程序 课程设计旨在通过实践让学生掌握计算机科学中的核心技能——程序设计。在这个过程中，学生将接触到一个重要的算法——DPLL 算法，用于解决命题逻辑公式的可满足性问题（SAT问题），这在计算机科学与人工智能领域具有基础性和挑战性。作为一门综合程序设计课程，本设计任务旨在让学生通过实际操作理解并应用这一算法。 设计内容包括以下几部分： 1. 输入输出功能：设计程序需要接受命令行参数，读取CNF格式的SAT实例文件，并能够输出和保存执行结果。这是任何程序的基础，对于确保数据的正确传递至关重要。 2. 公式解析与验证：学生需编写代码读取CNF文件，解析内容并构建内部表示。解析正确性的验证通过遍历内部结构并输出与原始文件对比来完成，这是检验算法正确性的关键步骤。 3. DPLL算法实现：基于DPLL算法，实现完整的SAT求解器。DPLL算法是求解SAT问题的一种高效方法，其核心是通过回溯搜索和单元传播来决定变量的取值。 4. 性能测量：记录求解过程所花费的时间，以评估算法效率。这可以通过调用系统时间函数实现，以毫秒为单位输出，便于分析优化潜力。 5. 程序优化：对DPLL算法进行改进，例如优化存储结构或分支变元选择策略，以提升求解速度。通过比较优化前后的执行时间，计算优化率，展示优化效果。 6. SAT应用：将数独游戏转化为SAT问题，将其整合到求解器中，使得程序可以解决数独谜题，并具备一定的交互性。这个部分需要理解数独问题的逻辑结构，将其归约到SAT框架下。 参考文献提供了关于SAT问题、DPLL算法以及数独游戏转为SAT问题的深入理解，帮助学生在设计过程中有据可依，确保设计的正确性和实用性。 这个课程设计项目旨在通过实践让学生深入理解SAT问题和DPLL算法，提升程序设计和问题解决能力，同时通过数独游戏的实现，强化算法的实际应用和软件工程的实践经验。通过这样的综合训练，学生将不仅掌握理论知识，还能锻炼实际编程技能，为未来在计算机科学领域的深入学习和工作奠定坚实基础。