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

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

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

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

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

10、z20</p><p>　　3.3.8步驟八：輸出數(shù)獨(dú)的正確結(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ù)獨(dú)介紹</b></p><p>　　數(shù)獨(dú)是一種源自18世紀(jì)末的瑞士，后在美國(guó)發(fā)展、并在日本得以發(fā)揚(yáng)光大的數(shù)學(xué)智力拼圖游戲。拼圖是九宮格（即3格寬×3格高）的正方形狀，每一格又細(xì)分為一個(gè)九宮格。在每一個(gè)小九宮格中，分別填上1至9的數(shù)字，讓整個(gè)大九宮格每一列、每一行的數(shù)字都不重復(fù)。 </p>&l

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

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

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

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

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

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

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

19、t;<p>　　如果F是可以滿足，則給出F的一個(gè)模型；</p><p>　　如果F是不可以滿足，則找到一個(gè)不可滿足的最小子集或找到一個(gè)可滿足的最大子集。</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>　　對(duì)于任意的公式F，總存在一個(gè)和它等價(jià)的合取范式F，,且F，沒(méi)有引入新的原

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

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

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

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

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

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

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

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

29、lt;/p><p>　　zchaff_base.cpp</p><p>　　zchaff_cpp_wrapper.cpp (這個(gè)文件可以通過(guò)這樣來(lái)獲得，把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>"來(lái)替換他們。然后

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下正確運(yùn)行，至少我們可以看見(jiàn)許多warning和error。有一些適合linux而不適合windows，現(xiàn)在我們應(yīng)該檢查下一步的工作，確保sat求解器在vs2008中可以正常運(yùn)行。我們對(duì)以下文件做下列修改：</p><p

33、><b>　　對(duì)于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>　　對(duì)于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>　　對(duì)函數(shù)handle_result進(jìn)行修改</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>　　對(duì)于zchaff_base.cpp</p><p>　　加上#include”stdafx.h”</p><p>　　對(duì)于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>　　對(duì)于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>　　對(duì)于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>　　對(duì)于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>　　對(duì)于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下的一個(gè)頭文件，而在VS2005中是沒(méi)有的。我們可以在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ù)獨(dú)中的

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

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

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

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

54、se </p><p>　　對(duì)于數(shù)獨(dú)游戲，每個(gè)數(shù)字知道在每一列出現(xiàn)一次，這個(gè)條件和上面第三個(gè)條件類似，只要把行列轉(zhuǎn)化就可以。類似的，我們可以通過(guò)以下方法確定該條件∧9x=1∧9z=1∨9y=1Sxyz</p><p>　　對(duì)于數(shù)獨(dú)游戲，每個(gè)數(shù)字至少在每個(gè)3*3的區(qū)域中出現(xiàn)一次，則引入變量i，j，確定行列的定位，使每個(gè)循環(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）確定了每個(gè)區(qū)域的各行各列范圍</p><p>　　當(dāng)我們加入clause后，我們調(diào)用sat求解器查看是否有唯一解。如果有的話，我們利用sat求解器找到每一個(gè)位置的應(yīng)填充數(shù)字在原子序列中的位置，并對(duì)該原子位置進(jìn)行裝換，就可以得到在x行，y列的交界應(yīng)該填寫(xiě)的數(shù)字。</p><p>　　當(dāng)我們得到正確的數(shù)獨(dú)游戲的結(jié)果后，我們可以有多重處理

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

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

58、子的索引</p><p>　　int SAT_AddVariable(SAT_Manager mng);</p><p>　　//這個(gè)函數(shù)是用來(lái)添加clause，每一個(gè)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的頭文件，一些典型的使用步驟以及注意事項(xiàng)</p><p>　　調(diào)用SAT_InitManager，可以得到一個(gè)manager對(duì)象，我們可以預(yù)先設(shè)variables的數(shù)目，或者你可以調(diào)用SAT_AddVariable來(lái)添加variables。Variables的下標(biāo)是從1開(kāi)始，而不是從0開(kāi)始.</p><p>　

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

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

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

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

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

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

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

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

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

74、的初始化數(shù)據(jù)來(lái)初始化數(shù)獨(dú)游戲</p><p>　　//從文件讀取數(shù)獨(dú)游戲的初始化元素</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<<"文件讀錯(cuò)誤"; </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>　　步驟：編寫(xiě)變量下標(biāo)與

78、x，y，z的雙向轉(zhuǎn)化函數(shù)</p><p>　　編寫(xiě)函數(shù)，計(jì)算出處于x行y列的z元素的原子編號(hào)</p><p>　　//寫(xiě)一個(gè)函數(shù)S，算出Sxyz對(duì)應(yīng)的變量編號(hào)</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>　　編寫(xiě)函數(shù)，計(jì)算出某一個(gè)具體原子編號(hào)對(duì)應(yīng)的x，y，z，這樣我們可以把原子編號(hào)轉(zhuǎn)化為具體的x行y列，并且可是直到在該位置存放什么數(shù)字</p><p&g

80、t;　　//寫(xiě)一個(gè)函數(shù)，將變量的原子編號(hào)換回本來(lái)的x,y,z就可以知道每個(gè)位置，即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對(duì)象</p><p>　　調(diào)用SA

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

84、中，</p><p>　　//找到那些已經(jīng)隨機(jī)填充的數(shù)字，然后計(jì)算Sxyz，每一個(gè)Sxyz就是一個(gè)clause，放進(jìn)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>　　//每一個(gè)格內(nèi)的數(shù)字最多只能填一個(gè)數(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>　　//每個(gè)數(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>　　//每個(gè)數(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>　　//每個(gè)數(shù)字至少在每個(gè)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ù)可以說(shuō)明是否找到一個(gè)解。</p><p>　　int result = SAT_Solve(sudoku_manager);</p><p>　　如果result的結(jié)果是如果result的結(jié)果是SATISFIBALE，說(shuō)明找到了一個(gè)解。</p><p>　　步驟七：進(jìn)行換算，把變量下標(biāo)位置轉(zhuǎn)化為x，y，z</p><p>　　通過(guò)SAT_

99、GetVarAsgnment(mng, i)可以得到每個(gè)變量（原子）的值，如果我們的數(shù)獨(dú)游戲是9宮圖，則其中i是從1-729。將變量i的編號(hào)換回本來(lái)的x,y,z就可以知道每個(gè)位置應(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ù)獨(dú)的正確結(jié)果</p><p>　　編

102、寫(xiě)函數(shù)，講數(shù)獨(dú)游戲的正確結(jié)果寫(xiě)到output.txt</p><p>　　//把數(shù)獨(dú)結(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)//或者寫(xiě)成myfile.fail() </p><p><b>　　{ </b></p><p>　　cout<<"文件打開(kāi)失敗，目標(biāo)文件狀態(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>　　或者編寫(xiě)函數(shù)，對(duì)整個(gè)數(shù)獨(dú)游戲的正確結(jié)果進(jìn)行預(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>　　在項(xiàng)目工程下的Debug目錄下，生成exe文件，可以供其他程序調(diào)用。并把輸出

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

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

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++標(biāo)準(zhǔn)程序庫(kù) >></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ù)的道路上，我們并不孤獨(dú)。</p><p>　　在這次設(shè)計(jì)中，xx老師不厭其煩地指導(dǎo)我，直到每一個(gè)

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