本文選題：布爾可滿足 + 現(xiàn)場(chǎng)可編程門陣列��； 參考：《廣西民族大學(xué)》2017年碩士論文

【摘要】：布爾可滿足問(wèn)題(SAT)作為第一個(gè)被證明的NP問(wèn)題在許多方面有著重要的應(yīng)用,該問(wèn)題是人工智能、集成電路設(shè)計(jì)與驗(yàn)證、計(jì)算機(jī)科學(xué)、數(shù)理邏輯等領(lǐng)域中的核心問(wèn)題,并且在計(jì)算機(jī)復(fù)雜性理論中有著十分重要的地位,作為NP問(wèn)題,SAT問(wèn)題無(wú)法在多項(xiàng)式時(shí)間內(nèi)求解,因此高效的SAT求解器的設(shè)計(jì)一直被世界各國(guó)的學(xué)者所重視,SAT求解算法分為完備算法和不完備算法,求解器分為軟件求解器和硬件求解器,其中硬件求解器又分為實(shí)例型求解器和應(yīng)用型求解器。本文給出了兩種基于FPGA的實(shí)例型硬件求解器的求解框架,即基于電路特征的求解框架和基于DPLL算法的求解框架,通過(guò)改變基于電路特征的求解框架中的激勵(lì)模塊實(shí)現(xiàn)了三種不同的求解方法,即順序遍歷激勵(lì)求解、真隨機(jī)數(shù)激勵(lì)求解和偽隨機(jī)數(shù)激勵(lì)求解,并對(duì)三種求解方法的實(shí)驗(yàn)結(jié)果進(jìn)行了對(duì)比和分析。對(duì)于基于DPLL算法的求解器,本文創(chuàng)新地在求解電路生成前對(duì)變量選取順序和變量賦值順序進(jìn)行了隨機(jī)排序,并對(duì)同一實(shí)例生成多個(gè)求解電路進(jìn)行多次求解,對(duì)不同次數(shù)的求解結(jié)果進(jìn)行了分析,并將所有實(shí)例的求解結(jié)果與其他硬件求解器及軟件求解器Minisat進(jìn)行了分析和對(duì)比。
[Abstract]:As the first proven NP problem, Boolean satisfiability problem has important applications in many fields. It is the core problem in the fields of artificial intelligence, integrated circuit design and verification, computer science, mathematical logic, etc. And it plays an important role in the theory of computer complexity. As a NP problem, the SAT problem can not be solved in polynomial time. Therefore, the design of efficient SAT solver has been paid much attention by scholars all over the world. The algorithm is divided into complete algorithm and incomplete algorithm, and solver is divided into software solver and hardware solver. The hardware solver is divided into example solver and application solver. In this paper, two kinds of hardware solver based on FPGA are presented, which are based on circuit characteristics and DPLL algorithm. By changing the excitation module of the circuit characteristic based solution framework, three different solutions are realized, namely, sequential traversal excitation solution, true random number excitation solution and pseudo random number excitation solution. The experimental results of the three methods are compared and analyzed. For the solver based on DPLL algorithm, this paper innovatively sorts the variable selection order and the variable assignment order before the generation of the solving circuit. The solution results of different times are analyzed and compared with other hardware solver and software solver Minisat.
【學(xué)位授予單位】：廣西民族大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：TN402

【參考文獻(xiàn)】

相關(guān)期刊論文 前10條

1 吳飛;李艷萍;;基于FPGA一種真隨機(jī)數(shù)生成器的設(shè)計(jì)和實(shí)現(xiàn)[J];計(jì)算機(jī)應(yīng)用與軟件;2013年11期

2 羅春麗;林勝釗;張鴻飛;崔珂;王堅(jiān);;基于FPGA的真隨機(jī)數(shù)產(chǎn)生器后處理算法的研究[J];核電子學(xué)與探測(cè)技術(shù);2013年02期

3 楊賢軍;;基于ChipScope的EDA實(shí)驗(yàn)平臺(tái)的設(shè)計(jì)[J];通信技術(shù);2012年10期

4 周進(jìn);趙希順;;基于硬件可編程邏輯(FPGA)的SAT算法的綜述[J];電子世界;2012年06期

5 張聰;于忠臣;;一種基于FPGA的真隨機(jī)數(shù)發(fā)生器設(shè)計(jì)與實(shí)現(xiàn)[J];電子設(shè)計(jì)工程;2011年10期

6 張雪鋒;范九倫;;基于線性反饋移位寄存器和混沌系統(tǒng)的偽隨機(jī)序列生成方法[J];物理學(xué)報(bào);2010年04期

7 王瀾濤;王友仁;張砦;;基于m序列的可重構(gòu)線性反饋移位寄存器研究[J];電腦與信息技術(shù);2009年02期

8 王星;沈小林;;基于FPGA的同步并聯(lián)LFSR序列生成器設(shè)計(jì)[J];現(xiàn)代電子技術(shù);2008年10期

9 曾祥萍;趙海全;;ISE集成開發(fā)環(huán)境下基于FPGA的數(shù)字設(shè)計(jì)[J];電腦知識(shí)與技術(shù);2006年35期

10 束禮寶,宋克柱,王硯方;偽隨機(jī)數(shù)發(fā)生器的FPGA實(shí)現(xiàn)與研究[J];電路與系統(tǒng)學(xué)報(bào);2003年03期

，

本文編號(hào)：1913273