首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   87篇
  国内免费   3篇
  完全免费   66篇
  自动化技术   156篇
  2018年   1篇
  2017年   2篇
  2016年   6篇
  2015年   9篇
  2014年   8篇
  2013年   11篇
  2012年   8篇
  2011年   6篇
  2010年   22篇
  2009年   16篇
  2008年   12篇
  2007年   8篇
  2006年   8篇
  2005年   9篇
  2004年   7篇
  2003年   5篇
  2002年   4篇
  2000年   1篇
  1999年   3篇
  1998年   5篇
  1997年   3篇
  1996年   1篇
  1991年   1篇
排序方式: 共有156条查询结果,搜索用时 93 毫秒
1.
求解SAT问题的拟人退火算法   总被引:21,自引:3,他引:18  
该文利用一个简单的变换,将可满足性(SAT)问题转换为一个求相应目标函数最小值的优化问题,提出了一种用于跳出局部陷阱的拟人策略,基于模拟退火算法和拟人策略,为SAT问题的高效近注解得出了拟人退火算法(PA),该方法不仅具有模拟退火算法的全局收敛性质,而且具有一定的并行性,继承性。数值实验表明,对于本文随机产生的测试问题例,采用拟人策略的模拟退火算法的结果优于局部搜索算法,模拟退火算法以及近来国际上流行的WALKSAT算法,因此拟人退火算法是可行的和有效的。  相似文献
2.
基于自动推理技术的智能规划方法   总被引:9,自引:0,他引:9       下载免费PDF全文
吕帅  刘磊  石莲  李莹 《软件学报》2009,20(5):1226-1240
对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规划方法,并结合国际规划竞赛和相关论文等的实验结论说明上述方法的有效性和可行性.最后,提出目前基于自动推理技术的智能规划方法所面临的挑战、可能的处理方法以及与之相关的研究热点与趋势.  相似文献
3.
中介谓词逻辑系统的λ-归结   总被引:8,自引:0,他引:8       下载免费PDF全文
潘正华 《软件学报》2003,14(3):345-349
给出中介逻辑谓词演算系统MF的一种无穷值语义解释,即无穷值的(解释,将λ-归结方法引入到MF中,讨论了MF的λ-归结原理,并证明了它的完备性.  相似文献
4.
This paper exploits Boolean satisfiability problem in equivalence checking and model checking respectively. A combinational equivalence checking method based on incremental satisfiability is presented. This method chooses the candidate equivalent pairs with some new techniques, and uses incremental satisfiability algorithm to improve its performance.By substituting the internal equivalent pairs and converting the equivalence relations into conjunctive normal form (CNF)formulas, this approach can avoid the false negatives, and reduce the search space of SAT procedure. Experimental results on ISCAS‘85 benchmark circuits show that, the presented approach is faster and more robust than those existed in literature.This paper also presents an algorithm for extracting of unsatisfiable core, which has an important application in abstraction and refinement for model checking to alleviate the state space explosion bottleneck. The error of approximate extraction is analyzed by means of simulation. An analysis reveals that an interesting phenomenon occurs, with the increasing density of the formula, the average error of the extraction is decreasing. An exact extraction approach for MU subformula, referred to as pre-assignment algorithm, is proposed. Both theoretical analysis and experimental results show that it is more efficient.  相似文献
5.
一个求解结构SAT问题的高效局部搜索算法   总被引:7,自引:1,他引:6  
逻辑表达式可满足性(SAT)问题是第一个被证明的NP完全问题.它也是解决人工智能和计算理论中许多实际问题的基础.人们发现,对于某些类型的SAT问题,局部搜索算法要比一些传统的算法(例如Davis-Putnam过程)更为有效.在本文中,我们主要讨论如何用局部搜索算法求解结构SAT问题.我们对一个典型的局部搜索算法GSAT+walk做了改进与扩展.首先,我们除去了GSAT+walk中GSAT部分的"平移";其次,我们给每一个子句赋权,并在GSAT+walk的搜索过程中动态地调整子句的权.文中给出的实验结果表明改进后的新算法对于求解结构SAT问题非常有效.  相似文献
6.
命题逻辑可满足性问题的算法分析   总被引:7,自引:0,他引:7       下载免费PDF全文
1 引言可满足性问题(以下简称SAT)是问:对于一个命题逻辑公式,是否存在对其变元的一个真值赋值使之成立?这个问题在许多领域都有非常重要的意义,其快速求解算法的研究成为计算机科学的中心课题之一。例如在机器定理证明领域,某命题是否是一个和谐的公理集合的推论,这个问题归结为该命题的反面与该公理集合一起是否是不可满足的。通过量词消去技术和Herbrand定理的作用,谓词逻辑公式的不可满足性可以归结为命题逻辑公式的不可满足性。在知识库维护中,当知识以逻辑公式的形式表达时,知识库的一致性检查可以归结为命题逻辑公式的可满足性。在开放逻辑中,新事实是否与已有的知识矛盾,当遇到事实反驳时如何求得最大和谐的知识集,这些问题最后都要归结为命题逻辑公式的可满足性。1971年Cook首次证明了SAT是NP-完全的,从而大量的计算问题都可以归约到SAT。正是由于SAT的重要地位,各国学者对它进行了广泛而深入的研究。  相似文献
7.
粘贴DNA模型的多级分离技术及其应用   总被引:6,自引:0,他引:6  
利用粘贴DNA模型现有的4种基本操作来解决问题效率低下,为解决这一问题,提出多级分离的概念,设计一个多级分离装置的模型,引入了多级分离技术.以可满足性问题(satisfiabilty problem,SAT)为例说明了该技术与装置的应用;通过实例的分析对比,展示了该技术的优越性.最后,证实了多级分离装置的有效性,并对多级分离技术的前景给予了展望.  相似文献
8.
求解SAT问题的改进粒子群优化算法   总被引:6,自引:5,他引:1  
贺毅朝  刘坤起 《计算机工程与设计》2006,27(15):2731-2733,2758
利用限制哆公式的相关理论将可满足性问题(SAT)等价转换为定义在{0,1}^n上的多项式函数优化问题,并将二进制粒子群优化算法(BPSO)与局部爬山搜索策略相结合,给出了一种求解SAT问题的新算法:基于局部爬山搜索的改进二进制粒子群优化算法(简称IBPSO).数值实验表明,对于随机产生的3-SAT问题测试实例,该算法的计算结果均优于著名的WalkSAT算法和SATI.3算法.  相似文献
9.
动态描述逻辑的Tableau判定算法   总被引:6,自引:1,他引:5  
动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动态逻辑的Tableau算法以及对可能模型途径的处理有机地结合起来,给出了D-ALCO的Tableau判定算法,证明了算法的可终止性、可靠性和完备性.应用该算法,可以在采用开世界假设的情况下对D-ALCO中公式的可满足性进行判定.对于D-ALCQO、D-ALCQIO等具有更强描述能力的动态描述逻辑,可以对该算法扩展后得到相应的Tableau判定算法.  相似文献
10.
一个适于形式验证的ATPG引擎   总被引:4,自引:0,他引:4  
自动测试产生(ATPG)不仅应用于芯片测试向量生成,也是芯片设计验证的重要引擎之一.提出了一种组合电路测试产生的代数方法,既可作为组合验证的ATPG引擎,又可用于通常的测试产生.该算法充分发挥了二叉判决图(BDD)及布尔可满足性(SAT)的优势,通过启发式策略实现SAT算法与BDD算法的交替,防止因构造BDD可能导致的内存爆炸,而且使用增量的可满足性算法,进一步提高了算法的效率.实验结果表明了该算法的可行性和有效性.  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

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