可满足性模理论综述

可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广泛应用在人工智能、硬件RTL验证、自动化推理和软件工程等领域。根据近些年SMT的发展,首先阐述SMT基本知识和常见的背景理论;然后分析总结Eager方法、Lazy方法和DPLL(T)方法的实现流程,并进一步介绍主流求解器Z3、CVC5和MathSAT5的实现过程;接着介绍SMT的扩展问题#SMT、SMT应用在深度神经网络的SMTlayer方法和量子SMT求解器;最后对SMT的发展进行展望,并讨论其面临的挑战。

《石油化工安全仪表系统设计规范》解读

主要介绍了GB/T 50770—2013《石油化工安全仪表系统设计规范》的编制过程、编制宗旨及适用范围,安全生命周期各阶段的活动及要求,各章节的内容及广大用户关注问题的探讨等。阐述了石油化工安全仪表系统在工程设计阶段,集成、调试与验收测试阶段,操作维护阶段的活动内容和设计规范,系统性地规范了安全仪表系统的测量仪表、最终元件、逻辑控制器、通信接口、人机接口、应用软件等设计原则。

基于硬解题的PLC设计及其在测发控系统中的应用

梯形图是目前应用最为广泛的PLC编程语言,根据解析方式不同分为硬解题和软解题两种。硬解题采用专用的梯形图硬件处理器,跟采用通用处理器软件解析方式相比,梯形图处理速率大大提升、功耗明显降低,能够满足恶劣环境下高可靠性应用需求,是高端PLC中的首选。本文通过研究梯形图构图原理,提出了一种梯形图编码方法,采用该方法完成了梯形图硬解题专用处理器HLS(Hardware Logic Solver)设计,并通过与通用处理器双核集成,在一个芯片实现了梯形图解析、通信控制、中断处理等全部内容,进一步提升了PLC的集成化、小型化水平。采用硬解题的PLC满足火箭测发控系统高可靠应用要求,已经在多个运载火箭中应用。

一种可扩展型CLP系统的统一建模方法

约束推理是人工智能中主要组成部分之一,可以解决实际优化调度和规划过程中的约束求解问题。这里在解释了约束逻辑程序设计的原理和过程基础上,打破封闭式约束逻辑程序设计系统,从软件工程上采用统一建模语言,提出一种新的开放的可扩展型约束逻辑程序设计结构系统。为实现可扩展的约束推理搜索系统,引进UML建模语言中用例图、类图和协作图。在建模基础上详细说明了可扩展约束逻辑程序设计中数学模型,搜索引擎和搜索驱动三者间的关系以及它们内部的工作内容。最后在描述系统结构后,提出了可扩展的内容。根据扩展因素,外界为满足更多的需要可扩展本系统的约束过滤器。

化工安全仪表系统设计探讨

介绍和分析了一般化工安全仪表系统各组成部分,明确了安全仪表系统在化工企业生产中的重要性,对在化工安全仪表系统中如何设计和设置传感器、最终执行元件、逻辑运算器、通讯接口、人机接口、过程接口、软件组态等进行了分析。

基于逻辑程序的调机路径规划研究

调机路径规划的核心是合理编排各台编组(解体)调机的移动路径以完成编组(解体)任务。但目前的编制工作仍以人工为主,存在编制作业的工作量大、计划编制不及时、计划调整困难等问题。为此,给出基于回答集程序(ASP)与有限域约束逻辑程序(CLP(FD))的设计方法。在轨道规模增大的情况下,讨论2种方法在求解不同问题规模时的时间效率以及对应求解器的运行规律。实验结果表明,ASP在解决调机路径规划问题时比CLP(FD)表现更优,能快速地得到路径编排结果,对应的DLV求解器能更有效地克服轨道数目增减带来的影响。

IMPLEMENTATION OF 3-VALUED PARACONSISTENT LOGIC PROGRAMMING TOWARDS DECISION MAKING SYSTEM OF AGENTS

Due to the rapid development of applications of artificial intelligence and robotics in recent years, the necessity of reasoning and decision making with uncertain and inaccurate information is increasing. Since robots in the real world are always exposed to behavioral inaccuracies and uncertainty arising from recognition methods, they may occasionally encounter contradictory facts during reasoning on action decision. Paraconsistent logic programming is promising to make appropriate action decisions even when an agent is exposed to such uncertain information or contradictory facts, but there has been no implementation of this programming to the best of our knowledge. We propose a resolution algorithm for the 3-valued paraconsistent logic programming system QMPT0 and its implementation on SWI-Prolog. We also describe an application of the 3-valued paraconsistent logic programming regarding agent decision making.

智能规划的逻辑编码求解性能分析

将SAT问题的编码和求解过程联合起来进行研究,提出了逻辑编码求解性能分析模型,利用该模型对国际标准规划域Logistic域和Blocks World域中的问题进行实验研究,并对实验结果中大量数据进行分析,进而分析逻辑编码的特性与求解效率的关系.实验结果表明逻辑编码的编码方式、编码规模以及规划图的扩展程度影响逻辑编码的求解效率.