首页 | 本学科首页   官方微博 | 高级检索  
检索     
共有20条相似文献,以下是第1-20项 搜索用时 593 毫秒

1.  SMT求解器理论组合技术研究  被引次数:2
   李婧  刘万伟《计算机工程与科学》,2011年第33卷第10期
   可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎。理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景。因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术。通过对照实验,评估各组合判定方法的优缺点以及目前流行的支持理论组合SMT求解器在工业应用中的性能。    

2.  基于模糊命题模态逻辑的形式推理系统  被引次数:4
   张再跃  眭跃飞  曹存根《软件学报》,2005年第16卷第8期
   探讨基于可信度的模糊命题模态逻辑的形式推理,给出相关的模糊Kripke语义描述.其研究目的旨在解决基于模态命题逻辑的模糊推理的能行问题.在研究过程与方法上,以完全形式化的方法将模糊模态逻辑语法和语义统一在一个形式系统中,以模糊约束作为基本表达式,给出推理规则,建立了相应的模糊推理形式系统,并以形式系统中模糊约束集的可满足性来表示模糊推理的有效性,使模糊推理过程变得容易,为最终在计算机上实现基于模态逻辑的模糊推理打下了一定的基础.主要结论是证明了基于可满足性的模糊推理形式系统的可靠性与完备性.    

3.  求解#SMT问题的局部搜索算法  
   周俊萍  李睿智  曾志勇  殷明浩《软件学报》,2016年第27卷第9期
   #SMT问题是SMT问题的扩展,它需要计算一阶逻辑公式F所有可满足解的个数.目前,该问题已被广泛应用于编译器优化、硬件设计、软件验证和自动化推理等领域.随着#SMT问题的广泛应用,设计可以求解较大规模#SMT实例的求解器亟待解决.基于以上原因,设计了一种求解较大规模#SMT实例的近似求解器——VolComputeWithLocalSearch.它在现有的#SMT精确求解算法的基础上加入差分进化算法,通过调用体积计算工具qhull,进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数,差分进化方法快速地枚举各个有解的区域.另外,从理论上证明了VolComputeWithLocalSearch求解器可以得到精确解的下界,使其可以应用在软件测试等只需要知道问题下界的领域.实验结果表明:VolComputeWithLocalSearch求解器是稳定的、具有快速的求解能力,并在高维问题上具有很好的表现.    

4.  基于模型检测的命题动态逻辑规划  
   韦林  古天龙  常亮《桂林电子科技大学学报》,2010年第30卷第2期
   命题动态逻辑是对动作进行刻画和推理,并在此基础上进行规划求解的一种有效工具.PDL规划问题一般通过逻辑推演进行求解,其本质是将规划问题转化为PDL公式的可满足性问题,相应的推理复杂度为EXP-完全.与可满足性推理相对应,PDL模型检测问题具有多项式级别的时间复杂度.鉴于PDL模型检测的高效,对基于模型检测的PDL规划求解进行研究,从PDL规划语义的角度证明了PDL规划可以通过模型检测的方法求解,在这基础上给出基于模型检测的PDL规划算法,结合实例验证了算法的正确性.    

5.  描述逻辑的粗糙扩展研究  
   王岁花  赵爱玲  魏涛《计算机工程与科学》,2011年第33卷第2期
   由于传统的描述逻辑系统不适于表示不确定的、模糊的知识,本文将基于粗糙集语义的下近似和上近似引入描述逻辑系统中,使用一种简单的方法将传统描述逻辑进行扩展,介绍了粗糙描述逻辑的概念,在粗糙描述逻辑系统中我们可以使用适当的子概念和超概念来对某些模糊的知识进行约束表示。本文主要讨论描述逻辑ALC的粗糙扩展,介绍扩展后所得到的粗糙描述逻辑RALC的语法、语义和相关推理问题,探讨了使用粗糙描述逻辑来对不精确概念进行建模的基本思想,最后提出了一个RALC的可满足性问题的推理算法。本文的工作可以使得在描述逻辑中对不确定的知识进行形式化描述和推理更加方便。    

6.  基于树状线性规划搜索的单调速率优化设计  
   陈力  王永吉  吴敬征  吕荫润《软件学报》,2015年第26卷第12期
   改善单调速率(rate monotonic,简称RM)可调度性判定算法的效率,是过去40年计算机实时系统设计的重要问题.最近,研究人员把可调度性判定问题扩展到了更一般的优化设计问题,即,如何调节在区间可选择情况下的任务运行时间,使得:(1)系统RM可调度;(2)系统的某个性能(如CPU利用率)达到最优.在已有的求解实时系统RM优化设计问题的方法中,都是先把原问题建模成广义约束优化问题,然后再对广义约束优化问题进行求解.但现有方法的求解速度较慢,任务数较多时不再适用.提出一种求解优化问题的方法——基于树状的线性规划搜索(linearprogramming search,简称LPS)方法.该方法先将实时系统RM优化设计问题建模成广义约束优化问题,再将其分拆成若干线性规划子问题,然后构造线性规划搜索树,利用剪枝搜索算法求解部分线性规划子问题,最后得到优化解.实验结果表明:LPS方法相比于已有的方法能够节省20%~70%的求解时间,任务数越多,节省时间越多.该研究成果可以与计算机可满足性模定理(satisfiability modulo theories,简称SMT)领域的多个研究热点问题联系起来,并可望改善SMT问题的求解效率.    

7.  基于布尔可满足性的逻辑电路等价性验证方法  
   刘歆  熊有伦《微电子学与计算机》,2007年第24卷第11期
   提出了基于布尔可满足性(Boolean Satisfiability,SAT)的逻辑电路等价性验证方法。这一验证方法把每个电路抽象成一个有穷自动机(FSM),为两个待验证的电路构造积机,把等价性验证问题转换成了积机的断言判定问题。改进了Tseitin变换方法,并将其用于把电路约束问题变换成(Conjunctive Normal Form,CNF)公式。之后则用先进的CNF SAT求解器zChaff判定积机所生成的布尔公式的可满足性。事例电路验证说明了该方法的有效性。    

8.  求解极小SMT不可满足子式的宽度优先搜索算法  
   张建民  沈胜宇  李思昆《计算机辅助设计与图形学学报》,2009年第21卷第7期
   极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition 2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.    

9.  基于支持度理论的广义Modus Ponens问题的最优解  被引次数:1
   李骏  王国俊《软件学报》,2007年第18卷第11期
   为了将模糊推理纳入逻辑的框架并从语构和语义两个方面为模糊推理奠定严格的逻辑基础,通过将模糊推理形式化的方法移植到经典命题逻辑系统中,把FMP(fuzzy modus ponens)问题转化为GMP(generalized modus ponens)问题,并基于公式的真度概念提出了公式之间的支持度,进一步利用支持度的思想引入了GMP问题以及CGMP(collective generalized modus ponens)问题的一种新型最优求解机制.证明了最优解的存在性,同时指出,在经典命题逻辑系统中存在着与模糊逻辑完全相似的推理机制.该方法是一种程度化的方法,这就使得求解过程从算法上实现成为可能,并对知识的程度化推理有所启示.    

10.  SMT求解技术简述  被引次数:2
   金继伟  马菲菲  张健《计算机科学与探索》,2015年第7期
   SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术,着重介绍并分析了这些技术,包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点,包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望,量词的处理、优化问题和解空间大小的计算等尤其值得关注。    

11.  基于动态描述逻辑的Web服务自动组合技术  
   陈立民  王竹晓  史忠植《高技术通讯》,2011年第21卷第1期
   提出了一种利用动态描述逻辑(DDL)的动态推理自动组合Web服务的方法.DDL是描述逻辑(DL)的一种动态扩展,它结合本体提供的静态信息与Web服务提供的计算,统一地描述和推理Web环境中静态信息与动态知识.该方法充分利用Web服务组合中涉及的静态知识(如描述逻辑知识库刻画的领域公理、具体环境和用户需求等)和动态知识(DDL中动作刻画的Web服务的功能),将Web服务组合的问题归约为DDL公式的可满足性问题,并通过一个可判的表扩展算法解决.开发了基于动态描述逻辑D-ALCHOQ的原型系统,并针对旅行代理问题的实验初步证实了该方法的可行性及潜在的应用前景.    

12.  一种求解布尔不可满足子式的局部搜索算法  
   张建民  沈胜宇  李思昆《计算机工程与科学》,2009年第31卷第4期
   解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由。近年来涌现了许多基于SAT求解器DPLL回溯搜索过程的完全算法,但关于不完全方法提取不可满足子式的研究相对较少。因此,本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法。该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列,并融合了布尔推理技术以提高搜索效率;而后通过一个递归过程遍历证明序列从而得到不可满足子式。通过实验与贪心遗传算法进行对比,结果表明本文提出的算法优于贪心遗传算法。    

13.  自动逻辑综合系统中的几个覆盖问题及其求解  
   刘明业  洪恩宇《计算机学报》,1986年第5期
   本文阐明将硬件逻辑翻译器产生的布尔方程集合划分成子集后,转换成多维体列阵。然后,首先寻求输入变量最小集(消去冗余输入变量),再进行逻辑最小化,并且如果必要还可将一个较大的逻辑列阵分解成较小的列阵,以满足工程设计的约束条件。 上述三个问题都可归结为求解覆盖问题,并且其规模可能很大。本文给出用覆盖矩阵取补(锐积运算)法求解这些问题的大循环覆盖表的方法。其特点是完全不存储覆盖矩阵,可以很快给出最佳解。 上述工作是为了建立一个将寄存器传输级语言描述翻译成硬件逻辑图的自动逻辑综合系统。    

14.  基于一阶模态逻辑的模糊推理  
   张晓如  张再跃  眭跃飞  黄智生《软件学报》,2008年第19卷第12期
   研究基于可信度的模糊一阶模态逻辑,给出了基于常域的模糊一阶模态逻辑语义以及推理形式系统描述.为有效进行模糊断言间的推理,考虑了模糊约束的概念.模糊约束是一个表达式,其中既有语法成分又包含意义信息.模糊推理形式系统中的基本对象是模糊约束,针对模糊约束引进可满足性概念,研究模糊约束可满足性相关性质.利用模糊约束的概念,模糊断言间的推理可以直接在语义环境下加以考虑,因此,以模糊约束为基本元素的模糊推理形式系统随之建立.主要分析新产生断言有效性与模糊约束集可满足性之间的关系,并在此基础上给出了模糊推理形式系统的推理规则.进一步的工作可探讨模糊推理形式系统的可靠性与完全性,建立推理过程的能行机制.研究结果可在人工智能和计算机科学等领域得以应用.    

15.  一种基于图的DL-Li te本体最小不可满足保持子集的计算方法  
   付雪峰  漆桂林  张勇《电子学报》,2016年第9期
   演变中的本体常出现不一致性问题,这将导致标准推理失效。针对不一致性问题,最小不可满足保持子集能够提供本体中概念不可满足的解释。计算最小不可满足保持子集是本体工程中的一项重要的非标准推理任务,但多数计算方法须借助外部的推理机,导致计算的效率不高。为了减少对推理机的依赖,本文提出了一种基于图的最小不可满足保持子集的计算方法。新的方法面向DL-Lite描述逻辑家族,将DL-Lite本体转换成图,将本体中的最小不可满足保持子集转换成图上的最小不可满足保持路径对。对比实验表明,基于图的方法提高了计算的效率和稳定性。    

16.  基于Yices对时间自动机的有界模型检测  
   王晓亮《计算机工程与设计》,2010年第31卷第1期
   为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法.该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测.实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势.    

17.  基于Game理论的μ-演算公理化  
   刘万伟  王戟  陈火旺《计算机研究与发展》,2007年第44卷第11期
   随着软硬件系统复杂性的不断提高,各种验证技术被越来越广泛的使用.模型检验技术是一种保证软硬件设计、实现正确性的有效技术.在针对软硬件的模型验证技术中,一般采用时序逻辑作为规约语言.模态μ-演算是模态和时序逻辑中应用较为广泛的一种,它具有语法成分简洁、表达能力强等特点.扩展了Lange和Stirling基于Focus Game的LTL和CTL的公理化方法.提出了一种基于Game理论的μ-演算公式的可满足性的测试方法,该种方法能够将模态μ-演算公式的可满足性问题转化为Focus Game的求解问题.进一步,基于这套Game规则,给出了一个新的关于μ-演算可靠完备的推理系统.同已有的μ-演算公理系统相比,该推理系统相对直观、简洁.    

18.  一阶逻辑中约束求解的局部搜索法*  
     《软件学报》,1998年第9卷第8期
   以一阶谓词逻辑为基础,讨论约束满足问题.着重研究一阶逻辑公式可满足性的局部搜索法,并与命题逻辑中的可满足性过程加以比较.以皇后问题和哈密顿回路问题为例,说明基于一阶逻辑的方法能处理较大的问题实例.    

19.  基于动态时序描述逻辑的动作理论  
   孙永新  赵希顺《计算机科学》,2014年第41卷第9期
   动态时序描述逻辑(DLTLDL)是一类描述逻辑的动态时序扩展。提出一种基于DLTLALCIO的动态域建模方法,利用该方法可构造出刻画动态域知识的DLTLALCIO理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等,可归结为关于DLTLALCIO理论的推理问题,并最终归结为DLTLALCIO的公式可满足性问题。DLTLALCIO公式可表达动作和时间约束,相对于其他基于描述逻辑的动作形式,基于DLTLALCIO的动作形式在需要执行复杂查询,尤其是含时间或动作的查询的应用场合具有更好的适用性。    

20.  基于限界模型检查的Web服务行为失配检测  
   戎玫  陈圣标  张广泉《计算机科学》,2012年第39卷第6期
   在Web服务组合过程中,常因交互协议不一致等导致服务失配;Web服务失配检测可准确捕捉失配点,为实现服务的有效组合奠定基础。采用限界模型检查技术,提出一种基于可满足性模理论(SMT)的Web服务行为失配检测方法。该方法首先将服务失配检测问题转化为逻辑公式的可满足性判定问题,然后利用Yices工具实现Web服务行为失配检测,最后通过实例进一步阐述该方法的有效性。    

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号