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

【摘要】：布爾可滿足問題(SAT)作為第一個被證明的NP問題在許多方面有著重要的應用,該問題是人工智能、集成電路設計與驗證、計算機科學、數(shù)理邏輯等領域中的核心問題,并且在計算機復雜性理論中有著十分重要的地位,作為NP問題,SAT問題無法在多項式時間內求解,因此高效的SAT求解器的設計一直被世界各國的學者所重視,SAT求解算法分為完備算法和不完備算法,求解器分為軟件求解器和硬件求解器,其中硬件求解器又分為實例型求解器和應用型求解器。本文給出了兩種基于FPGA的實例型硬件求解器的求解框架,即基于電路特征的求解框架和基于DPLL算法的求解框架,通過改變基于電路特征的求解框架中的激勵模塊實現(xiàn)了三種不同的求解方法,即順序遍歷激勵求解、真隨機數(shù)激勵求解和偽隨機數(shù)激勵求解,并對三種求解方法的實驗結果進行了對比和分析。對于基于DPLL算法的求解器,本文創(chuàng)新地在求解電路生成前對變量選取順序和變量賦值順序進行了隨機排序,并對同一實例生成多個求解電路進行多次求解,對不同次數(shù)的求解結果進行了分析,并將所有實例的求解結果與其他硬件求解器及軟件求解器Minisat進行了分析和對比。
[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.
【學位授予單位】：廣西民族大學
【學位級別】：碩士
【學位授予年份】：2017
【分類號】：TN402

【參考文獻】

相關期刊論文 前10條

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

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

3 楊賢軍;;基于ChipScope的EDA實驗平臺的設計[J];通信技術;2012年10期

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

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

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

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

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

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

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

，

本文編號：1913273