畢業(yè)論文--基于sat的數獨游戲實現

1、<p><b>　　中文摘要</b></p><p>　　本文通過結合數獨游戲和SAT求解器，對SAT求解器的作用進行了探討. SAT的計算復雜性很高，但實際中又有需求，目前很多公司已經開發(fā)了許多SAT解算器，本文采用The SAT Group at Princeton University開發(fā)完成的SAT求解器。SAT求解器的運用范圍廣泛，適合許多領域。本文通過調用SAT求解器，

2、來實現數獨游戲的功能問題。通過本文，我們將進一步了解SAT求解器的相關工作方式。</p><p>　　關鍵字：數獨，sat求解器，C++，vector容器</p><p><b>　　Abstract</b></p><p>　　This paper combines Sudoku and the SAT solver,and discuss

3、the role of the SAT solver. SAT's computational complexity is high, and it’s needed in much fields in practice. At present, many companies have developed a number of SAT solvers, this paper, we use the SAT solver dev

4、eloped by The SAT Group at Princeton University. SAT solvers are used in a wide range, suitable for many areas. In this paper, we call SAT solver to achieve the functioning of Sudoku. In this article, we will learn more

5、about </p><p>　　Key words: Sudoku，sat Solver，C++，vector</p><p><b>　　目錄</b></p><p><b>　　中文摘要1</b></p><p>　　Abstract2</p><p><b&

6、gt;　　第一章緒論5</b></p><p>　　1.1數獨介紹5</p><p>　　1.1.1數獨歷史5</p><p>　　1.1.2數獨游戲元素構成6</p><p>　　1.1.3數獨游戲規(guī)則7</p><p>　　1.2SAT介紹7</p><p&g

7、t;　　編譯SAT求解器9</p><p>　　1.3SAT求解器的移植以及安裝步驟：9</p><p>　　1.4修改SAT求解器9</p><p>　　第二章SAT算法思想13</p><p>　　SAT在數獨中的應用13</p><p>　　第三章SAT求解器在數獨游戲的實現15</p&

8、gt;<p>　　3.1SAT求解器原有函數介紹15</p><p>　　3.2SAT求解器15</p><p>　　3.3調用SAT求解器過程16</p><p>　　3.3.1步驟一：初始化數組16</p><p>　　3.3.2步驟二：初始化數獨游戲17</p><p>　　3.

9、3.3步驟：編寫變量下標與x，y，z的雙向轉化函數18</p><p>　　3.3.4步驟四：定義SAT_Manager對象18</p><p>　　3.3.5步驟五：添加clause18</p><p>　　3.3.6步驟六：檢查是否有唯一解20</p><p>　　3.3.7步驟七：進行換算，把變量下標位置轉化為x，y，

10、z20</p><p>　　3.3.8步驟八：輸出數獨的正確結果21</p><p>　　3.3.9步驟九：生產exe文件22</p><p><b>　　總結23</b></p><p><b>　　致謝25</b></p><p><b>　　緒論

11、</b></p><p><b>　　數獨介紹</b></p><p>　　數獨是一種源自18世紀末的瑞士，后在美國發(fā)展、并在日本得以發(fā)揚光大的數學智力拼圖游戲。拼圖是九宮格（即3格寬×3格高）的正方形狀，每一格又細分為一個九宮格。在每一個小九宮格中，分別填上1至9的數字，讓整個大九宮格每一列、每一行的數字都不重復。 </p>&l

12、t;p>　　數獨的玩法邏輯簡單，數字排列方式千變萬化。不少教育者認為數獨是鍛煉腦筋的好方法</p><p><b>　　數獨歷史</b></p><p>　　相傳數獨源起于拉丁方陣（Latin Square），1970年代在美國發(fā)展，改名為數字拼圖（Number Place）、之后流傳至日本并發(fā)揚光大，以數學智力游戲智力拼圖游戲發(fā)表。在1984年一本游戲雜志《パ

13、ズル通信ニコリ》正式把它命名為數獨，意思是“在每一格只有一個數字”。后來一位前任香港高等法院的新西蘭籍法官高樂德（Wayne Gould）在1997年3月到日本東京旅游時，無意中發(fā)現了。他首先在英國的《泰晤士報》上發(fā)表，不久其他報紙也發(fā)表，很快便風靡全英國，之后他用了6年時間編寫了電腦程式，并將它放在網站上，使這個游戲很快在全世界流行。</p><p>　　香港是在2003年7月30日由《AM730》引入數獨。&

14、lt;/p><p>　　中國大陸是在2007年2月28日正式引入數獨. 2007年2月28日，北京晚報智力休閑數獨俱樂部(數獨聯盟前身)在新聞大廈舉行加入世界謎題聯合會的頒證儀式，會上謎題聯合會秘書長皮特-里米斯特和俱樂部會長在證書上簽字，這標志著北京晚報智力休閑俱樂部成為世界謎題聯合會的39個成員之一，這也標志著俱樂部走向國際舞臺，它將給數獨愛好者帶來更多與世界數獨愛好者們交流的機會。</p><

15、;p>　　后來更因數獨的流行衍生了許多類似的數學智力拼圖游戲，例如：數和、殺手數獨。</p><p><b>　　數獨游戲元素構成</b></p><p><b>　　數獨基本元素示意圖</b></p><p>　　單元格：數獨中最小的單元，標準數獨中共有81個；</p><p>　　行：橫向

16、9個單元格的集合；</p><p>　　列：縱向9個單元格的集合；</p><p>　　宮：粗黑線劃分的區(qū)域，標準數獨中為3×3的9個單元格的集合；</p><p>　　已知數：數獨初始盤面給出的數字；</p><p>　　候選數：每個空單元格中可以填入的數字。</p><p><b>　　數獨游戲

17、規(guī)則</b></p><p>　　標準數獨的規(guī)則為：數獨每行、每列及每宮填入數字1-9且不能重復。</p><p><b>　　SAT介紹</b></p><p>　　可滿足性(英語：Satisfiability)是用來解決給定的布爾方程式，是否存在一族變量賦值，是問題為否可滿足。布爾克滿足性問題（Boolean satisfiab

18、ility problem；SAT)屬于決定性問題，是第一個被證明的NP完全問題。為電腦科學上許多領域的重要問題，包括電腦科學基礎理論，算法，人工智能，硬件設計等等。</p><p>　　對于一個確定的邏輯電路，是否存在一種輸入使得輸出為true，是第一個被證明的NPC問題。</p><p>　　SAT：給定一個命題公式F，判斷F是否是滿足的。對于SAT求解器，有以下作用：</p&g

19、t;<p>　　如果F是可以滿足，則給出F的一個模型；</p><p>　　如果F是不可以滿足，則找到一個不可滿足的最小子集或找到一個可滿足的最大子集。</p><p>　　一般的SAT求解器以合取范式作為輸入。合取范式是子句（Clause）的合取，例如（a1∨b1）∧（-a2∨b2∨c2）∧（-a3∨-b3∨c3）∧（-a4）</p><p>　　L

20、iteral：原子或者原子的否定</p><p>　　Clause：a1∨a2∨…..∨an,其中ai是文字</p><p>　　Empty clause：子句中n=0；空子局是不可滿足的；</p><p>　　Unit clause：子句中n=1；</p><p>　　對于任意的公式F，總存在一個和它等價的合取范式F，,且F，沒有引入新的原

21、子；</p><p>　　對于任意的公式F，總是存在一個和他等價的合取范式F，，且F，的長度至多是多項式的</p><p>　　滿足性是決定如果某一布爾公式中的變量可以被分配在公式中，并使這個公式可以被證明是TRUE。同樣重要的是，它還可以確定是否存在這樣的滿足的條件，這將意味著，對于所有可能的variable assignments，通過該公式表示的函數的變量都賦值為FALSE。在后一種

22、情況下，我們會說，該函數是unsatisfiable，否則它是satisfiable。為了強調這個問題的二進制性質，因此經常被稱為布爾可滿足性命題（Boolean or propositional satisfiability）?？s寫“SAT”也常用來表示布爾可滿足性命題，以表示該函數和變量都是binary-valued。</p><p>　　在復雜性理論，可滿足性問題（SAT）的是一個決策問題，他的instan

23、ce是由and，or，not，variable和parenthese構成的布爾表達式?，F在的問題是：給出一個表達式，是否可以分配變量ture或者false，將使整個表達式為true？如果邏輯變量被分配值后，使該公式為true，則該命題邏輯公式被認為是可滿足的。布爾可滿足性問題是NP -完全問題。命題可滿足問題（PSAT），決定給定的命題公式是否可滿足的，是在計算機科學的各個領域，包括理論計算機科學，算法學，人工智能，硬件設計，電子設計自

24、動化，并核查至關重要。 </p><p>　　1個literal可以是variable，也可以是variable的negation。例如，X1是postiveliteral，not（X2）是negative literal。1個clause是literals的結合，例如X1∨not(X2)是1個clause。</p><p>　　有一些Boolean satisfiability prob

25、lem的特殊例子，其中formulae要求是clauses的結合。確定一個合取范式，其中每個clause限定最多3個literals是NP完全，這樣的問題叫做"3SAT", "3CNFSAT"或者"3-satisfiability"。相似的，確定一個合取范式，其中每個clause限定最多2個literals是NP完全，這樣的問題叫做"2SAT"。確定每一個c

26、lause是Horn clause的formula的可滿足性事p-完全，這樣的問題叫做Horn-satisfiability。</p><p>　　Cook–Levin定理證明了布爾可滿足性問題是NP -完全問題，而事實上，這是第一個被證明是NP完全問題的決策問題。但是，除了這一理論外，在過去十年，有關SAT方面有效率和高級的算法不斷得到發(fā)展。正是這些發(fā)展，使得我們有能力解決涉及成千上萬的variables還有上

27、百萬的constraints的問題。例如，在電子設計自動化（EDA）包括正式等價性檢驗，模型檢驗，流水線微處理器正式驗證，自動測試模式生成，FPGA的路由等。SAT求解器解引擎被認為是在EDA工具箱中的重要組成部分。</p><p><b>　　編譯SAT求解器</b></p><p>　　通過輸入一個cnf給SAT求解器，查找我們想要的結果。由于該SAT求解器適用

28、于linux環(huán)境，必須通過移植修改，使其滿足windows環(huán)境，并且可以在visual studio 2008編譯下正確工作。</p><p>　　SAT求解器的移植以及安裝步驟：</p><p>　　在linux下，該SAT求解器應該是沒有任何問題。現在我們裝換操作系統環(huán)境，改為在windows下執(zhí)行該求解器。打開visual studio，創(chuàng)建一個新的工程，并且把以下文件添加到工程中&

29、lt;/p><p>　　zchaff_base.cpp</p><p>　　zchaff_cpp_wrapper.cpp (這個文件可以通過這樣來獲得，把zchaff_wrapper.wrp改名為zchaff_cpp_wrapper.cpp，并且刪除該文件中所有"EXTERN"關鍵字)</p><p>　　zchaff_dbase.cpp</p

30、><p>　　zchaff_solver.cpp</p><p>　　zchaff_utils.cpp</p><p>　　sat_solver.cpp</p><p>　　修改那些包括頭文件"sys/*.h"的文件。刪除那些麻煩的頭文件，用"#include <time.h>"來替換他們。然后

31、把函數get_cpu_time()替換為</p><p>　　double get_cpu_time(void) </p><p><b>　　{</b></p><p>　　return (double)clock()/(double)(CLOCKS_PER_SEC);</p><p><b>　　} &l

32、t;/b></p><p><b>　　修改SAT求解器</b></p><p>　　根據文檔修改的文件還未能在vs2008下正確運行，至少我們可以看見許多warning和error。有一些適合linux而不適合windows，現在我們應該檢查下一步的工作，確保sat求解器在vs2008中可以正常運行。我們對以下文件做下列修改：</p><p

33、><b>　　對于SAT.h文件</b></p><p>　　// get the version of the solver</p><p>　　const char * SAT_Version(SAT_Manager mng); </p><p>　　把返回類型改為char *</p><p>　　對于sat

34、_solver.h文件</p><p>　　插入#include “stdafx.h”</p><p>　　int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);</p><p>　　將函數sscanf改為sscanf_s,參數不變。</p>

35、<p>　　對函數handle_result進行修改</p><p>　　cout << "RESULT:\t”<<filemname<<”"<<result << endl;</p><p>　　插入filename</p><p>　　在main函數中if子句中刪除ret

36、urn 2</p><p>　　if (argc < 2) {</p><p>　　cerr << "Z-Chaff: Accelerated SAT Solver from Princeton. " << endl;</p><p>　　cerr << "Copyright 2000-2004

37、, Princeton University." << endl << endl;;</p><p>　　cerr << "Usage: "<< argv[0] << " cnf_file [time_limit]" << endl;</p><p><b>

38、　　return 2;</b></p><p>　　刪除return 2;</p><p>　　講mian函數中的else區(qū)域改為 </p><p><b>　　else {</b></p><p>　　read_cnf (mng, argv[1] );</p><p>　　SAT

39、_SetTimeLimit(mng,atoi(argv[2]));</p><p><b>　　}</b></p><p>　　采用static_cast裝換，將SAT_SetTimeLimit(mng,atoi(argv[2]));改為SAT_SetTimeLimit (mng,static_cast<float>(atoi(argv[2])));<

40、;/p><p>　　對于zchaff_base.cpp</p><p>　　加上#include”stdafx.h”</p><p>　　對于zchaff_dbase.cpp</p><p>　　else if (current_mem < _params.mem_limit * 0.8)</p><p>　　gro

41、w_ratio=1.2;</p><p>　　加上static_cast轉化，改為grow_ratio=static_cast<float>(1.2);</p><p>　　對于zchaff_dbase.h</p><p>　　inline unsigned num_literals(void) {</p><p>　　retur

42、n _stats.num_added_literals -_stats.num_deleted_literals;</p><p><b>　　}</b></p><p>　　加上static_cast格式，改為return static_cast<unsigned int>(_stats.num_added_literals -_stats.num_de

43、leted_literals);</p><p>　　對于zchaff_solver.cpp</p><p>　　float CSolver::elapsed_cpu_time(void) {</p><p>　　return get_cpu_time()-stats.start_cpu_time;</p><p><b>　　}&

44、lt;/b></p><p>　　改為return static_cast<float>(get_cpu_time()-stats.start_cpu_time);</p><p>　　float CSolver::cpu_run_time(void) {</p><p>　　return (_stats.finish_cpu_time - _st

45、ats.start_cpu_time);</p><p><b>　　}</b></p><p>　　改為return static_cast<float>(_stats.finish_cpu_time - _stats.start_cpu_time);</p><p>　　對于zchaff_solver.h</p>

46、<p>　　inline bool cmp_var_stat(const pair<CVariable *, int> & v1,</p><p>　　const pair<CVariable *, int> & v2) {</p><p>　　return v1.second >=v2.second;</p><

47、p><b>　　}</b></p><p>　　改為return v1.second >v2.second;</p><p>　　對于zchaff_utils.cpp</p><p>　　刪除<unistd.h>頭文件</p><p>　　刪除double get_cpu_time函數的定義內容，

48、在該函數的作用域中加上</p><p>　　Return (double)clock()/(double)(CLOCKS_PER_SEC); </p><p>　　Sat_solver.cpp</p><p>　　其中，sat_solver.cpp所需要的dirent.h是gcc下的一個頭文件，而在VS2005中是沒有的。我們可以在http://softagalle

49、ria.net/download/dirent/dirent-1.8.zip下載，并且放在vs2008安裝目錄下Microsoft Visual Studio 9.0\VC\include\中。</p><p>　　自此，我們完成了SAT求解器的安裝移植。</p><p><b>　　SAT算法思想</b></p><p>　　SAT在數獨中的

50、應用</p><p>　　首先我們先確定輸入規(guī)模，即確定數獨游戲的行列數，如果輸入的規(guī)模是3，則行數為9，列數為9，每一個小宮是3*3的。如果輸入規(guī)模是4，則行數為4，列數為4，每一個小宮是4*4.以此類推。</p><p>　　確定數獨游戲的初始化數據。確定的方法有二種：</p><p>　　隨機初始化，然后調用sat求解器查看是否有唯一解，如果有，則將確定這些數

51、據為數獨游戲的初始化數據。</p><p>　　人工初始化，先把初始化數據寫在input.txt文件中，然后讀取該文件，并 根據該文件的內容進行初始化。</p><p>　　根據sat求解器的要求，我們根據滿足的條件，產生不同的clause。當我們的數獨游戲是9宮圖時，我們有9*9*9=729個原子，每一個原子我們可以用Sxyz來表示，即在方格中(x,y)填了數字z。</p>

52、<p>　　我們應該滿足以下的幾個條件，并且作為clause，添加到sat求解器。</p><p>　　數獨游戲初始化時，某些空格已經有初始數字，我們應該確定這些數字,且把Sxyz作為一個clause。即（x，y）填有z，則把Sxyz作為一個clause。</p><p>　　對于數獨游戲，每一個空格只能填寫一個數字。我們可以通過以下的方法來確定這個條件?！?x=1∧9y=1

53、∧8z=1∧9i=z+1(-Sxyz∨-Sxyi)。該公式相當于遍歷２維數組的每一個小格，然后ｚ的取值從１到８，ｉ的取值從z+1到9，以-Sxyz，-Sxyi作為clause。</p><p>　　對于數獨游戲，每個數字至少在每行出現一次。我們可以通過以下方法來確定這個條件∧9y=1∧9z=1∨9x=1Sxyz，先遍歷每一列，并且每一個空格的取值從1到9，這這個前提下，由于每一列對應著9行，每一行對應一個clau

54、se </p><p>　　對于數獨游戲，每個數字知道在每一列出現一次，這個條件和上面第三個條件類似，只要把行列轉化就可以。類似的，我們可以通過以下方法確定該條件∧9x=1∧9z=1∨9y=1Sxyz</p><p>　　對于數獨游戲，每個數字至少在每個3*3的區(qū)域中出現一次，則引入變量i，j，確定行列的定位，使每個循環(huán)作用在3*3的區(qū)域。∧2i=0∧2j=0∧3x=1∧3j=1∨9z=1

55、S（3i+x）（3J+y）z，其中（3i+x）（3J+y）確定了每個區(qū)域的各行各列范圍</p><p>　　當我們加入clause后，我們調用sat求解器查看是否有唯一解。如果有的話，我們利用sat求解器找到每一個位置的應填充數字在原子序列中的位置，并對該原子位置進行裝換，就可以得到在x行，y列的交界應該填寫的數字。</p><p>　　當我們得到正確的數獨游戲的結果后，我們可以有多重處理

56、手段：</p><p>　　將正確的數獨游戲結果寫入output.txt文件中，以便其他程序調用。</p><p>　　當玩家填入的數字與我們的結果不符合時，可以及時發(fā)出提示，提醒玩家所填入的數字錯誤。</p><p>　　當玩家在某一位置無法確定數字時，我們可以給出該位置的正確填入數字。</p><p>　　SAT求解器在數獨游戲的實現&l

57、t;/p><p>　　SAT求解器原有函數介紹</p><p>　　//該函數產生一個manager，我們可以預先設定變量原子的個數，或者調用//SAT_AddVariable函數來設定。</p><p>　　SAT_Manager SAT_InitManager(void);</p><p>　　//這個函數可以增加一個變量原子，返回新的變量原

58、子的索引</p><p>　　int SAT_AddVariable(SAT_Manager mng);</p><p>　　//這個函數是用來添加clause，每一個clause可以表示為一系列數字。</p><p>　　void SAT_AddClause(SAT_Manager mng,int * clause_lits,int num_lits,int

59、gid = 0);</p><p>　　//返回SAT_StatusT，即是否有解，SAT_StatusT是enmu類型，枚舉成員有//UNDETERMINED,UNSATISFIABL，SATISFIABLE,TIME_OUT,MEM_OUT,ABORTED</p><p>　　int SAT_Solve(SAT_Manager mng);</p><p>　　/

60、/我們調用SAT_GetVarAsgnment(sudoku_manager, i)函數返回的值是o或者1，表示變量i的真假，如果返回的是1，則我們可以利用i值，在后續(xù)工作中，算出x行y列應該存放的數字。</p><p>　　int SAT_GetVarAsgnment(SAT_Manager mng,int v_idx);</p><p><b>　　SAT求解器</b&

61、gt;</p><p>　　以下使用sat_solver的頭文件，一些典型的使用步驟以及注意事項</p><p>　　調用SAT_InitManager，可以得到一個manager對象，我們可以預先設variables的數目，或者你可以調用SAT_AddVariable來添加variables。Variables的下標是從1開始，而不是從0開始.</p><p>　

62、　調用SAT_AddClause添加clauses，Clause表示為一序列的integers，每一個literal表示為2 * VarIndex + Sign，當Sign為0時，表示literal是positive，而當sign為1時，表示literals是negative，例如，clause (3 -5 11 -4 )應該表示為{ 6, 11, 22, 9 }。注意：在一個clause中，每一個variable可以出現多次。如果一個

63、variable在兩個phase出現，則這個clause自動滿足。如果variable在同一個phase出現多次，則他們應該結合為一個。調用者應該確定每一個clause不是多余的，否則sat_solver無法正確的運行。</p><p>　　Zchaff擴展了SAT的功能，每次運行后，我們可以從數據庫中添加或者刪除Clauses。為了達到這個目標，每一個clause都有一個Group ID。如果有多個clause

64、共享同一個Group ID，則我們在每次運行后調SAT_DeleteClauseGroup從數據庫中刪除共享GID的clause group。在重新運行時，我們需要調用SAT_Reset來重置solver的狀態(tài)。例如，前10個clause共享GID 1，我們添加其他兩個共享GID 2的clause，再解決這12個clause的instance之后，或許我們希望刪除后面2個clause，并且添加其他3個clause。我們用GID 2做參數

65、，調用SAT_DeleteClauseGroup，然后增添3個clause。（這3個clause可以有任意的GID，有以下幾種可能：1你以后不想刪除它們，2你希望把這幾個clause與GID 1區(qū)別。然后調用SAT_Reset()重置solver的狀態(tài)，再次調用SAT_Solve()解決新的例子（13個clause）。我們調用SAT_AllocClauseGroupID可獲得clau</p><p>　　當調用S

66、AT_DeleteClauseGroup，我們可以刪除GID，而當我們再次調用SAT_AllocClauseGroupID時，GID又可以再次使用。我們可以調用相關函數，合并兩個group的clauses。</p><p>　　你可以設置solver的時間限制和內存限制。Note：時間限制和內存限制是不精確的，你可以像clause deletion設置其他參數。</p><p>　　在一些

67、decisions后，我們可以添加一些Hook函數去來實現額外的工作。Hook函數接受一個manager為參數，沒有返回值。</p><p>　　調用SAT_Solve解決問題，該函數的返回值是solver的狀態(tài)，即是否有解</p><p>　　如果problem是可滿足的，調用SAT_GetVarAsgnment得到一個滿足problem的variable assignment。<

68、/p><p>　　我們也可以從solver得到一些統計數據，例如運行時間，mem用法等。</p><p>　　Release the manager by calling SAT_ReleaseManager.</p><p>　　調用SAT_ReleaseManager釋放manager</p><p>　　你需要鏈接庫libsat.a，當你使

69、用這個sat solver求解器時，即使你可以在C編譯器編譯你的C程序，你也需要c++ linker連接庫。</p><p>　　調用SAT求解器過程</p><p><b>　　步驟一：初始化數組</b></p><p>　　根據用戶輸入確定數獨游戲的二維數組。如果用戶輸入是3，則我們生成4*4的數組，該二維數組初始化為0.為了計算的方面，第

70、一行第一列不用，我們的索引從下標1開始。其中al_row_num表示總行數，al_col_num表示總列數，al_number表示每個小格可以填寫數字的選擇數。（例如，9*9的數獨游戲中，有9行9列，且每一個小格的數字可以從1到9）</p><p><b>　　//產生數獨游戲</b></p><p>　　int** p=new int*[al_row_num+1];

71、</p><p>　　for(int i=0;i!=al_row_num+1;++i)</p><p>　　p[i]=new int[al_col_num+1];</p><p><b>　　//全部初始化為0</b></p><p>　　for(int i=0;i!=al_row_num+1;++i)</p>

72、;<p>　　for(int j=0;j!=al_col_num+1;++j)</p><p>　　p[i][j]=0;</p><p>　　步驟二：初始化數獨游戲</p><p>　　對數組的隨意個元素，進行隨機初始化</p><p><b>　　//隨機初始化</b></p><p&

73、gt;　　for(int i=1;i<=1+rand()%(al_row_num);++i)</p><p>　　for(int j=1;j<=1+rand()%(al_col_num);++j)</p><p>　　p[i][j]=1+rand()%(al_number);</p><p>　　另一種初始化方法，編寫函數，用于讀取input.txt文件

74、的初始化數據來初始化數獨游戲</p><p>　　//從文件讀取數獨游戲的初始化元素</p><p>　　void input(int** p)</p><p><b>　　{</b></p><p>　　ifstream myfile; </p><p>　　myfile.open("

75、;c:\\input.txt"); </p><p>　　int x=0,y=0,z=0,count=0;</p><p>　　if(!myfile) </p><p><b>　　{ </b></p><p>　　cout<<"文件讀錯誤"; </p>&

76、lt;p>　　system("pause"); </p><p>　　exit(1); </p><p><b>　　} </b></p><p>　　while(myfile){</p><p>　　myfile>>x>>y>>z;</p>

77、<p>　　p[x][y]=z;</p><p><b>　　}</b></p><p>　　myfile.clear();</p><p>　　myfile.close(); </p><p><b>　　}</b></p><p>　　步驟：編寫變量下標與

78、x，y，z的雙向轉化函數</p><p>　　編寫函數，計算出處于x行y列的z元素的原子編號</p><p>　　//寫一個函數S，算出Sxyz對應的變量編號</p><p>　　int S(int x,int y,int z,int al_row_num,int al_col_num)</p><p><b>　　{</b&

79、gt;</p><p>　　return ((x-1)*al_row_num+(y-1))*al_col_num+z;</p><p><b>　　}</b></p><p>　　編寫函數，計算出某一個具體原子編號對應的x，y，z，這樣我們可以把原子編號轉化為具體的x行y列，并且可是直到在該位置存放什么數字</p><p&g

80、t;　　//寫一個函數，將變量的原子編號換回本來的x,y,z就可以知道每個位置，即x行y列應存放的數字，并且把該數字放在x行y列中</p><p>　　void RS(int SS,int al_row_num,int al_col_num,int al_number,int** p )</p><p><b>　　{</b></p><p&g

81、t;　　for(int x=1;x<=al_row_num;++x)</p><p>　　for(int y=1;y<=al_col_num;++y)</p><p>　　for(int z=1;z<=al_number;++z)</p><p>　　if(SS==S(x,y,z,al_row_num,al_col_num))</p>

82、<p><b>　　{</b></p><p>　　p[x][y]=z;</p><p><b>　　}</b></p><p><b>　　}</b></p><p>　　步驟四：定義SAT_Manager對象</p><p>　　調用SA

83、T_InitManager初始化一個SAT_Manager對象</p><p>　　//初始化manager</p><p>　　SAT_Manager sudoku_manager=SAT_InitManager(); </p><p>　　步驟五：添加clause</p><p>　　添加clause，clause都是放在vector容器

84、中，</p><p>　　//找到那些已經隨機填充的數字，然后計算Sxyz，每一個Sxyz就是一個clause，放進vector中</p><p>　　for(int x=1;x<=al_row_num;++x)</p><p>　　for(int y=1;y<=al_col_num;++y)</p><p><b>　

85、　{</b></p><p><b>　　int z=0;</b></p><p>　　if(p[x][y]!=0)</p><p><b>　　{</b></p><p>　　z=p[x][y];</p><p>　　temp.clear();</p>

86、;<p>　　temp.push_back(2*S(x,y,z,al_row_num,al_col_num));</p><p>　　SAT_AddClause(sudoku_manager, & temp.begin()[0], temp.size());</p><p><b>　　}</b></p><p><

87、b>　　}</b></p><p>　　//每一個格內的數字最多只能填一個數字</p><p>　　for(int x=1;x<=al_row_num;++x)</p><p>　　for(int y=1;y<=al_col_num;++y)</p><p>　　for(int z=1;z<=al_numb

88、er-1;++z)</p><p><b>　　{</b></p><p>　　for(int i=z+1;i<=al_number;++i)</p><p><b>　　{</b></p><p>　　temp.clear();</p><p>　　temp.push

89、_back(2*S(x,y,z,al_row_num,al_col_num)+1);</p><p>　　temp.push_back(2*S(x,y,i,al_row_num,al_col_num)+1);</p><p>　　SAT_AddClause(sudoku_manager, &temp.begin()[0], temp.size()); </p><

90、;p><b>　　}</b></p><p><b>　　}</b></p><p>　　//每個數字至少在每行出現一次</p><p>　　for(int y=1;y<=al_col_num;++y)</p><p>　　for(int z=1;z<=al_number;++z)

91、</p><p><b>　　{</b></p><p>　　temp.clear();</p><p>　　for(int x=1;x<=al_row_num;++x)</p><p>　　temp.push_back(2*S(x,y,z,al_row_num,al_col_num));</p>&

92、lt;p>　　SAT_AddClause(sudoku_manager, & temp.begin()[0], temp.size());</p><p><b>　　}</b></p><p>　　//每個數字至少在每列出現一次</p><p>　　for(int x=1;x<=al_row_num;++x)</p&

93、gt;<p>　　for(int z=1;z<=al_number;++z)</p><p><b>　　{</b></p><p>　　temp.clear();</p><p>　　for(int y=1;y<=al_col_num;++y)</p><p>　　temp.push_back

94、(2*S(x,y,z,al_row_num,al_col_num));</p><p>　　SAT_AddClause(sudoku_manager, & temp.begin()[0], temp.size());</p><p><b>　　}</b></p><p>　　//每個數字至少在每個n*n的區(qū)域中出現一次</p&g

95、t;<p>　　for(int i=0;i<=(number-1);++i)</p><p>　　for(int j=0;j<=(number-1);++j)</p><p>　　for(int x=1;x<=number;++x)</p><p>　　for(int y=1;y<=number;++y)</p>

96、<p><b>　　{</b></p><p>　　temp.clear();</p><p>　　for(int z=1;z<=al_number;++z)</p><p>　　temp.push_back(2*S(number*i+x,number*j+y,z,al_row_num,al_col_num));</p&g

97、t;<p>　　SAT_AddClause(sudoku_manager, & temp.begin()[0], temp.size())</p><p><b>　　}</b></p><p>　　步驟六：檢查是否有唯一解</p><p>　　加完clause后，調用SAT_Solve(sudoku_manager)，該

98、函數可以說明是否找到一個解。</p><p>　　int result = SAT_Solve(sudoku_manager);</p><p>　　如果result的結果是如果result的結果是SATISFIBALE，說明找到了一個解。</p><p>　　步驟七：進行換算，把變量下標位置轉化為x，y，z</p><p>　　通過SAT_

99、GetVarAsgnment(mng, i)可以得到每個變量（原子）的值，如果我們的數獨游戲是9宮圖，則其中i是從1-729。將變量i的編號換回本來的x,y,z就可以知道每個位置應該是什么數了。</p><p>　　if(result==SATISFIABLE){ </p><p>　　verify_solution(sudoku_manager);</p><p>

100、;　　for (int i=1, sz = SAT_NumVariables(sudoku_manager); i<= sz; ++i) </p><p><b>　　{</b></p><p>　　int var_value = SAT_GetVarAsgnment(sudoku_manager,i);</p><p>　　if(va

101、r_value==1)</p><p>　　RS(i,al_row_num,al_col_num,al_number,p);</p><p><b>　　}</b></p><p><b>　　}</b></p><p>　　步驟八：輸出數獨的正確結果</p><p>　　編

102、寫函數，講數獨游戲的正確結果寫到output.txt</p><p>　　//把數獨結果輸出為txt，該txt的內容格式為x（行），y（列），z（數字）</p><p>　　void output(int al_row_num,int al_col_num,int** p)</p><p><b>　　{</b></p><

103、p>　　ofstream myfile("c://output.txt"); </p><p>　　if(!myfile)//或者寫成myfile.fail() </p><p><b>　　{ </b></p><p>　　cout<<"文件打開失敗，目標文件狀態(tài)可能為只讀！";

104、 </p><p>　　system("pause"); </p><p>　　exit(1); </p><p><b>　　} </b></p><p>　　for(int i=1;i<=al_row_num;++i)</p><p>　　for(int j=

105、1;j<=al_col_num;++j)</p><p>　　myfile<<i<<" "<<j<<" "<<p[i][j]<<endl; </p><p>　　myfile.close(); </p><p><b>　　}</

106、b></p><p>　　或者編寫函數，對整個數獨游戲的正確結果進行預覽</p><p><b>　　//輸出</b></p><p>　　void output_sudoku(int al_row_num,int al_col_num,int** q)</p><p><b>　　{</b>

107、</p><p>　　for(int i=1;i<=al_row_num;++i)</p><p><b>　　{</b></p><p>　　for(int j=1;j<=al_col_num;++j)</p><p>　　cout<<q[i][j]<<" ";&

108、lt;/p><p>　　cout<<endl;</p><p><b>　　}</b></p><p><b>　　}</b></p><p>　　步驟九：生產exe文件</p><p>　　在項目工程下的Debug目錄下，生成exe文件，可以供其他程序調用。并把輸出

109、結果寫到output文件上。</p><p><b>　　總結</b></p><p>　　通過這段時間的學習，我充分掌握了SAT求解器的運用。在實際解決問題中，算法的效率讓我驚訝。寫一個回溯法的數獨游戲，如果是9*9規(guī)模，則效率方面是SAT求解器的效率沒有太大區(qū)別，但是如果規(guī)模幾何級增加的話，SAT求解器的算法的效率明顯比回溯法高效得多。對于程序員來說，算法就是靈魂

110、，高效，健壯性強的程序，需要算法來支持。</p><p>　　除此之外，我在本次畢業(yè)設計中，深刻體會到團隊合作的重要性，對于一個團隊而言，良好的溝通和理解非常重要。默契的合作，對產品的開發(fā)至關重要。參考文獻</p><p>　　Ines Lynce，Joel Ouaknine，Sudoku as a SAT Problem</p><p>　　閔應驊，布爾可滿足性問

111、題，2009-9-11</p><p>　　Mattew W.Moskewicz，Chaff:Engineering an efficient SAT Solver </p><p>　　San Jose，Efficient conflict driven learning in a Boolean satisfiability solver</p><p>　　N

112、icolai M.Josuttis，侯捷譯， <<C++標準程序庫 >></p><p>　　Stanley B.Lippman，<<C++ primer>></p><p>　　http://en.wikipedia.org/wiki/Boolean_satisfiability_problem 2009-12-24</p&

113、gt;<p>　　http://blog.51xuewen.com/jokeduck/article_17109.htm 2009-12-24</p><p><b>　　致謝</b></p><p>　　在追求技術的道路上，我們并不孤獨。</p><p>　　在這次設計中，xx老師不厭其煩地指導我，直到每一個

114、問題的解決。他在這段時間，不斷指出我工作的不足之處，并給與寶貴的意見，在我的畢業(yè)設計上花費大量時間和精力。xx老師的敬業(yè)精神和負責的態(tài)度讓我感動不已。借此畢業(yè)論文完成之際，衷心向我的指導老師xx老師表示我個人最高敬意的感謝！</p><p>　　歲月如歌，光陰似箭，回首大學歷程，對那些引導我、幫助我、激勵我的老師和同學，我心中充滿了感激。謝謝你們！</p><p>　　感謝院領導，感謝xx