資源下載地址：https://download.csdn.net/download/sheziqiong/85634352
資源下載地址：https://download.csdn.net/download/sheziqiong/85634352
目 錄
1 引言 1
1.1 課題背景與意義 1
1.2 國內外研究現狀 1
1.3 課程設計的主要研究工作 2
2 系統需求分析與總體設計 3
2.1 系統需求分析 3
2.1.1 SAT求解器 3
2.1.2 數獨游戲 3
2.2 系統總體設計 3
2.2.1 SAT求解器 3
2.1.2 數獨游戲 4
3 系統詳細設計 6
3.1 有關數據結構的定義 6
3.1.1 數據結構定義 6
3.1.2 數據結構關聯 9
3.1.3 相關常量聲明 10
3.2 主要算法設計 11
3.2.1 CNF范式操作 11
3.2.2 DPLL算法 18
3.2.3 數獨生成算法 19
3.3 程序優化 24
3.3.1 結構優化 24
3.3.2 函數遞歸轉非遞歸 24
3.3.3 文字選取策略的優化 25
3.3.4 程序優化結果測試 27
4 系統實現與測試 29
4.1 系統實現 29
4.1.1 cnf文件 29
4.1.2 DPLL文件 31
4.1.3 Sudoku文件 32
4.2 系統測試 32
4.2.1 SAT求解器模塊測試 33
4.2.2 數獨功能模塊測試 42
5 總結與展望 49
5.1 全文總結 49
5.2 工作展望 49
6 體會 51
參考文獻 52
附錄 53
1 引言
1.1 課題背景與意義
對于計算機科學與技術、信息安全與物聯網專業大二學生，在前三個學期已經學習了C語言程序設計、數據結構兩門面向編程知識與技術的基礎理論課，以及C語言程序設計實驗、數據結構實驗兩門編程實踐課程，不僅具有較為系統性的C語言、常用數據結構基本知識，而且具有初步的程序設計、數據抽象與建模、問題求解與算法設計的能力，奠定了進行復雜程序設計的知識基礎。但兩門實驗課仍屬于對基本編程模型與技術的驗證性訓練，而“綜合程序設計”課程設計正是使大家從簡單驗證到綜合應用，甚至在編程中實現智慧與風格升華的重要實踐環節，為后續學習與進行計算機系統編程打下堅實的基礎，讓綜合編程技能成為大家的固有能力與通向未來專業之門的鑰匙。
1.2 國內外研究現狀
近十多年來，可滿足性問題研究逐漸升溫，已成為了國際國內的研究熱點， 取得了一批相當重要的理論和實踐成果，應該說當前的SAT問題研究比十多年前 已取得了很大的突破，并直接或間接地推動了其他相關領域（比如形式驗證，人 工智能等領域）的發展。
國際上已提出了各種不同的局部搜索算法和回溯搜索算法，使得SAT解決器解決不同領域中的SAT問題的能力不斷增強，能解決的問題的規模不斷增大。其中局部搜索算法顯示出對于隨機的SAT問題特別有用，而回溯搜索算法則 被用來解決大規模實際應用領域中的SAT問題。事實上，國際上已提出了一大批 采用回溯搜索算法的高效的SAT問題解決器，其中絕大多數提出來的回溯搜索算 法是對原始的DPLL回溯搜索算法的改進算法。這些改進措施包括:新的 變量決策策略，新的搜索空間剪除技術，新的推理和回溯技術以及新的更快的算 法實現方案和數據結構等。當前水平的SAT問題求解器已能夠輕松解決以前傳統 SAT問題解決器完全無法解決的可滿足性問題。
盡管當前的SAT問題解決器已取得了相當重要的進步，但是研究的腳步不會停止，我們還可以提出一些值得研究的問題。比如，是否存在新的更高效的SAT 問題處理技術可以集成到DPLL算法框架內；是否可以找到除局部搜索，回溯搜 索之外的其他SAT算法來更有效地解決SAT問題；是否能提出更好的SAT改進算 法和實現方案。
1.3 課程設計的主要研究工作
本次實驗中，實驗者選擇了 “基于SAT的數獨游戲求解程序”作為實驗課題，實現SAT求解器和數獨游戲兩個功能。
SAT求解器基于DPLL的完備算法，對CNF范式算例文件進行求解，輸出答案，并可選擇遍歷驗證答案或將答案存入文件；數獨游戲可轉化為SAT問題，用本系統實現的SAT求解器可以快捷地對數獨問題轉化的CNF文件進行求解，再以變元真值數據轉化的數獨盤格式輸出求解答案。本系統具有一定的交互功能，用戶可以利用本系統進行數獨游戲，系統將自動判斷解的正確性，并輸出正確答案。
包含：文檔+任務書+源碼清單+操作手冊+項目源碼
本文轉載自：http://www.biyezuopin.vip/onews.asp?id=16238























資源下載地址：https://download.csdn.net/download/sheziqiong/85634352
資源下載地址：https://download.csdn.net/download/sheziqiong/85634352

總結

以上是生活随笔為你收集整理的基于QT实现的数独游戏DPLL的SAT求解器设计的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。