畢業(yè)論文--基于sat的數(shù)獨游戲?qū)崿F(xiàn)

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

2、來實現(xiàn)數(shù)獨游戲的功能問題。通過本文，我們將進一步了解SAT求解器的相關(guān)工作方式。</p><p>　　關(guān)鍵字：數(shù)獨，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數(shù)獨介紹5</p><p>　　1.1.1數(shù)獨歷史5</p><p>　　1.1.2數(shù)獨游戲元素構(gòu)成6</p><p>　　1.1.3數(shù)獨游戲規(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在數(shù)獨中的應(yīng)用13</p><p>　　第三章SAT求解器在數(shù)獨游戲的實現(xiàn)15</p&

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

9、3.3步驟：編寫變量下標與x，y，z的雙向轉(zhuǎn)化函數(shù)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步驟七：進行換算，把變量下標位置轉(zhuǎn)化為x，y，

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

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

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

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

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

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

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

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

18、ility problem；SAT)屬于決定性問題，是第一個被證明的NP完全問題。為電腦科學(xué)上許多領(lǐng)域的重要問題，包括電腦科學(xué)基礎(chǔ)理論，算法，人工智能，硬件設(shè)計等等。</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，通過該公式表示的函數(shù)的變量都賦值為FALSE。在后一種

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

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

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

25、lem的特殊例子，其中formulae要求是clauses的結(jié)合。確定一個合取范式，其中每個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完全問題的決策問題。但是，除了這一理論外，在過去十年，有關(guān)SAT方面有效率和高級的算法不斷得到發(fā)展。正是這些發(fā)展，使得我們有能力解決涉及成千上萬的variables還有上

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

28、于linux環(huán)境，必須通過移植修改，使其滿足windows環(huán)境，并且可以在visual studio 2008編譯下正確工作。</p><p>　　SAT求解器的移植以及安裝步驟：</p><p>　　在linux下，該SAT求解器應(yīng)該是沒有任何問題。現(xiàn)在我們裝換操作系統(tǒng)環(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"關(guān)鍵字)</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、把函數(shù)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>　　根據(jù)文檔修改的文件還未能在vs2008下正確運行，至少我們可以看見許多warning和error。有一些適合linux而不適合windows，現(xiàn)在我們應(yīng)該檢查下一步的工作，確保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>　　將函數(shù)sscanf改為sscanf_s,參數(shù)不變。</p>

35、<p>　　對函數(shù)handle_result進行修改</p><p>　　cout << "RESULT:\t”<<filemname<<”"<<result << endl;</p><p>　　插入filename</p><p>　　在main函數(shù)中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函數(shù)中的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轉(zhuǎn)化，改為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函數(shù)的定義內(nèi)容，

48、在該函數(shù)的作用域中加上</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在數(shù)獨中的

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

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

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

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

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

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

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

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

58、子的索引</p><p>　　int SAT_AddVariable(SAT_Manager mng);</p><p>　　//這個函數(shù)是用來添加clause，每一個clause可以表示為一系列數(shù)字。</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、/我們調(diào)用SAT_GetVarAsgnment(sudoku_manager, i)函數(shù)返回的值是o或者1，表示變量i的真假，如果返回的是1，則我們可以利用i值，在后續(xù)工作中，算出x行y列應(yīng)該存放的數(shù)字。</p><p>　　int SAT_GetVarAsgnment(SAT_Manager mng,int v_idx);</p><p><b>　　SAT求解器</b&

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

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

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

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

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

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

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

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

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

70、一行第一列不用，我們的索引從下標1開始。其中al_row_num表示總行數(shù)，al_col_num表示總列數(shù)，al_number表示每個小格可以填寫數(shù)字的選擇數(shù)。（例如，9*9的數(shù)獨游戲中，有9行9列，且每一個小格的數(shù)字可以從1到9）</p><p><b>　　//產(chǎn)生數(shù)獨游戲</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>　　步驟二：初始化數(shù)獨游戲</p><p>　　對數(shù)組的隨意個元素，進行隨機初始化</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>　　另一種初始化方法，編寫函數(shù)，用于讀取input.txt文件

74、的初始化數(shù)據(jù)來初始化數(shù)獨游戲</p><p>　　//從文件讀取數(shù)獨游戲的初始化元素</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的雙向轉(zhuǎn)化函數(shù)</p><p>　　編寫函數(shù)，計算出處于x行y列的z元素的原子編號</p><p>　　//寫一個函數(shù)S，算出Sxyz對應(yīng)的變量編號</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>　　編寫函數(shù)，計算出某一個具體原子編號對應(yīng)的x，y，z，這樣我們可以把原子編號轉(zhuǎn)化為具體的x行y列，并且可是直到在該位置存放什么數(shù)字</p><p&g

80、t;　　//寫一個函數(shù)，將變量的原子編號換回本來的x,y,z就可以知道每個位置，即x行y列應(yīng)存放的數(shù)字，并且把該數(shù)字放在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>　　調(diào)用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>　　//找到那些已經(jīng)隨機填充的數(shù)字，然后計算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>　　//每一個格內(nèi)的數(shù)字最多只能填一個數(shù)字</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>　　//每個數(shù)字至少在每行出現(xiàn)一次</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>　　//每個數(shù)字至少在每列出現(xiàn)一次</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>　　//每個數(shù)字至少在每個n*n的區(qū)域中出現(xiàn)一次</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后，調(diào)用SAT_Solve(sudoku_manager)，該

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

99、GetVarAsgnment(mng, i)可以得到每個變量（原子）的值，如果我們的數(shù)獨游戲是9宮圖，則其中i是從1-729。將變量i的編號換回本來的x,y,z就可以知道每個位置應(yīng)該是什么數(shù)了。</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>　　步驟八：輸出數(shù)獨的正確結(jié)果</p><p>　　編

102、寫函數(shù)，講數(shù)獨游戲的正確結(jié)果寫到output.txt</p><p>　　//把數(shù)獨結(jié)果輸出為txt，該txt的內(nèi)容格式為x（行），y（列），z（數(shù)字）</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>　　或者編寫函數(shù)，對整個數(shù)獨游戲的正確結(jié)果進行預(yù)覽</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>　　步驟九：生產(chǎn)exe文件</p><p>　　在項目工程下的Debug目錄下，生成exe文件，可以供其他程序調(diào)用。并把輸出

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

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

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>　　在追求技術(shù)的道路上，我們并不孤獨。</p><p>　　在這次設(shè)計中，xx老師不厭其煩地指導(dǎo)我，直到每一個

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