邏輯公式的可滿足性問題在工程技術(shù)、交通運(yùn)輸、軍事及自然科學(xué)等領(lǐng)域有著廣泛的應(yīng)用。隨著計(jì)算機(jī)求解問題容量的逐漸增大、求解的問題愈加復(fù)雜,命題邏輯中邏輯公式的冗余越來(lái)越多,浪費(fèi)大量的儲(chǔ)存空間和計(jì)算時(shí)間。檢測(cè)并消除邏輯公式中的冗余可以有效的提高計(jì)算機(jī)儲(chǔ)存空間利用效率和削減計(jì)算時(shí)間。本文研究邏輯公式的冗余性質(zhì)及其判定,以期為冗余的消除提供一定的理論基礎(chǔ)。主要的研究工作如下:一、研究冗余子句的性質(zhì),提出冗余子句的判定方法。首先,引用二元子句定義的隱藏文字及其相關(guān)性質(zhì)提出邏輯公式中冗余子句的概念。然后,分別得到子句集中是否存在單元子句的判定方法;基于冗余子句的概念,討論了邏輯公式中子句冗余的問題,推導(dǎo)出冗余子句與其相對(duì)應(yīng)的子句集的可滿足性的等價(jià)條件。最后,利用子句集間的等價(jià)性,得到了冗余子句的相應(yīng)判定條件。二、研究了冗余文字的性質(zhì),提出冗余文字的判定方法。首先,根據(jù)二元子句中隱藏文字的添加規(guī)則,提出了子句集中冗余文字的概念,并得到冗余文字與其相對(duì)應(yīng)的子句集的可滿足性之間的關(guān)系。然后,根據(jù)冗余子句的相關(guān)性質(zhì),推導(dǎo)出冗余子句與冗余文字的相互關(guān)系。最后,根據(jù)子句集間的等價(jià)性,提出了判定冗余子句和冗余文字... 

【文章來(lái)源】：西南交通大學(xué)四川省 211工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：68 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
abstract
常用子句集
第1章 緒論
    1.1 研究背景及意義
    1.2 國(guó)內(nèi)外研究現(xiàn)狀
    1.3 研究的內(nèi)容及方法
第2章 預(yù)備知識(shí)
    2.1 命題邏輯中邏輯公式的基本概念
    2.2 命題邏輯中邏輯公式的化簡(jiǎn)規(guī)則
    2.3 本章小結(jié)
第3章 命題邏輯中子句集的冗余子句的判定方法
    3.1 子句集的冗余子句
    3.2 子句集中冗余子句的判定
    3.3 本章小結(jié)
第4章 命題邏輯中子句集的冗余文字的判定方法
    4.1 子句集的冗余文字
    4.2 子句集中冗余文字的判定
    4.3 本章小結(jié)
總結(jié)與展望
致謝
參考文獻(xiàn)
附錄 文字冗余性的判定程序
碩士學(xué)位期間發(fā)表的論文和研究工作


【參考文獻(xiàn)】：
期刊論文
[1]求解MinSAT問題的加強(qiáng)式格局檢測(cè)與子句加權(quán)算法[J]. 周俊萍,任雪亮,殷茜,李睿智,殷明浩.  計(jì)算機(jī)學(xué)報(bào). 2018(04)
[2]移動(dòng)網(wǎng)絡(luò)服務(wù)信息傳輸中冗余量消除方法研究[J]. 顧愛華.  計(jì)算機(jī)仿真. 2016(11)
[3]基于子句文字長(zhǎng)度動(dòng)態(tài)約束的變量消除算法[J]. 鄧曉瑤,馮志勇,饒國(guó)政,王鑫.  計(jì)算機(jī)科學(xué)與探索. 2014(11)
[4]命題邏輯公式中的冗余子句及冗余文字[J]. 翟翠紅,秦克云.  計(jì)算機(jī)科學(xué). 2013(05)
[5]格值邏輯公式中短語(yǔ)和文字的可消性[J]. 徐揚(yáng),宋振明.  數(shù)學(xué)季刊. 1990(Z1)
[6]布爾邏輯公式中文字和小項(xiàng)的可消性[J]. 徐揚(yáng),鄒開其.  西南交通大學(xué)學(xué)報(bào). 1990(01)

博士論文
[1]基于分治的布爾可滿足性判定[D]. 范全潤(rùn).西安電子科技大學(xué) 2015

碩士論文
[1]命題邏輯中子句集的分類研究[D]. 鄧鵬.西南交通大學(xué) 2015
[2]應(yīng)用線性代數(shù)求解可滿足性問題的研究與實(shí)現(xiàn)[D]. 丁志宇.中山大學(xué) 2014
[3]命題邏輯中子句集的冗余性研究[D]. 唐仕輝.西南交通大學(xué) 2014



本文編號(hào)：3536999