命题编码中公理的组合与设计

近年来,基于可满足性的规划方法研究逐渐成为智能规划研究领域中的热点。提出3种基于Graphplan的编码方式中公理的改进:动作互斥的部分放松、动作互斥的完全放松方法、添加框架公理。基于SATPLAN2006规划系统分别实现上述3种改进的编码方式,并对国际规划竞赛中选用的标准后勤域与积木世界域的问题样例予以测试,分析不同编码方式的编码规模与求解效率,验证了基于Graphplan编码方式的改进在绝大多数情况下是有效的。最后,实现基于状态的编码方式,并对上述两个域进行测试,比较约简动作与约简状态这两种极端方式的求解效率和编码规模。实验结果表明,在后勤域的某些问题上基于状态的编码方式比基于动作的编码方式有效得多。上述的改进策略表明,可根据问题域的特性等来考虑该问题最适宜哪些公理组合的编码方式,而不固定使用某种特定的编码方式。     

量化关联规则的隐私保持挖掘方法

根据数据库中量化属性值和分类属性值数量的不同,分别提出了基于布尔关联规则的量化关联规则隐私保持挖掘方法和基于部分变换机制的量化关联规则隐私保持挖掘方法。对于每一种方法都进行了隐私度和正确度分析,并通过实验证明了其正确性和可行性。     

规划问题编码成SAT问题研究

智能规划问题是一个NP-hard的问题。近年来,由于在可满足问题（SAT）研究领域取得了较大进展,出现了一大批快速的能达到工业级应用的SAT solver求解器的出现,这使得运用可满足技术来求解规划问题的方法越来越得到智能规划研究者们的重视。用可满足技术求解规划问题的首要任务是必须将规划问题“翻译”成可满足问题。讨论了如何将规划问题编码成命题可满足问题的一般技术,并对“直接编码”和“基于规划图的编码”两种编码技术进行了比较,指出了两种编码技术各自的优缺点。在此基础上,深入地分析了各种不同的编码方案之间的异同点以及它们各自的优缺点。最后,指出了用SAT技术求解规划问题中存在的一些问题以及相关改进方法。     

智能规划的逻辑编码方式研究

逻辑编码方式的设计和实现是基于转换的规划方法有效处理的关键.对几种智能规划方法中的逻辑编码方式予以分析,分别介绍线性编码、基于Graphplan的编码、基于状态的编码、基于动作的编码、基于命题的编码、基于转移的编码、提升的因果编码、基于多值变元的编码、基于有向二元决策图的编码以及基于约束可满足的编码等,并结合国际规划竞赛和相关论文等的实验结论,说明上述编码方式的有效性和可行性,分析该类编码方式在其他领域的应用前景.最后,提出目前智能规划方法中逻辑编码方式研究所面临的挑战、可能的处理方法,以及与之相关的研究热点与趋势.     

量化关联规则的隐私保持挖掘算法

为了保证用户信息不被有意或无意地泄漏,根据数据库中量化属性值和分类属性值数量的不同,分别提出了基于布尔关联规则、基于部分变换机制和基于概率变换的量化关联规则隐私保持挖掘方法.对于每一种方法都进行了隐私度和正确度分析,并通过实验验证其正确性和可行性.     

面向深空探测任务的实数遗传编码多星任务规划算法

针对面向深空探测任务的多星任务规划问题,综合考虑卫星对目标时间窗口、卫星姿态机动以及工作能耗等约束条件,建立了面向深空探测任务的多星任务规划问题模型,针对常规01编码在进行大规模卫星任务规划时,存在的编码长度过长等问题,提出了一种基于实数编码方式的遗传算法,以求解面向深空探测的多星任务规划问题.该算法采用了一种以目标为染色体的实数编码方式,相比传统的以时间窗口为染色体的01编码方式,缩短了染色体长度,可有效提高算法的求解效率.通过仿真算例分析,验证了基于实数编码的遗传算法对求解多星任务规划问题的正确性、合理性和有效性,并将其与基于传统01编码方式的遗传算法进行对比分析,其结果表明基于实数编码方式的遗传算法在寻优能力和计算速度上具有明显优势,这为求解面向深空探测任务的多星任务规划问题提供了一种新的思路和方法.     

基于布尔型粒子群优化算法的网络编码优化

针对布尔型粒子群优化算法存在容易陷入局部极值和收敛速度慢的缺点,提出一种带扰动因子的自适应调整惯性权重和学习因子取1概率的布尔型粒子群优化算法,并把这种改进的布尔型粒子群优化算法用于网络编码的优化以得到具有最小编码边的编码方案.对两个人工拓扑进行优化得到的结果表明,基于布尔型粒子群优化算法最小化编码边方案的收敛速度和精度都优于基于遗传算法最小化编码边的方案的速度和精度,能有效用于网络编码的优化.     

基于混沌遗传的巡航导弹实时规划技术

研究针对突发威胁的实时规划技术能够提高巡航导弹在未知威胁环境中的生存能力,具有重大的研究价值。实时规划的规划思想和规划算法的设计问题是巡航导弹实时规划技术必须要解决的两大难题。基于解决问题的考虑,设计了实时航迹规划的规划思路和一种混沌遗传规划算法。基于传统遗传算法的思想,利用威胁和约束条件构建适应度函数对航迹进行评价,设计了一种特殊的实数结构体编码,提出了合适的选择、交叉、变异三种算子使种群进化,并引入了混沌搜索算子,加速种群的收敛。最后进行了实时航迹规划的仿真分析。仿真结果表明:实时规划的航迹能够避开地形和新出现的威胁,算法收敛速度较快。这说明,设计的算法能够满足当前未知威胁环境下巡航导弹实时规划的需要。     

量化关联规则在高校就业信息数据中的应用

针对就业信息数据中存在着大量的量化属性和分类属性等现象,提出了一种基于k-means的量化关联规则挖掘方法。该方法利用聚类算法k-means对量化属性进行合理分区,将量化属性转化为布尔型;利用改进的布尔关联规则方法对此进行关联规则挖掘,找出学生的受教育属性和就业属性之间的关联性;对挖掘出的规则进行分析和运用。就业信息数据实验证明,文中所提方法对就业信息进行挖掘是有效的、可行的。     

高效的MPEG先进音频编码方案

为提高MPEG先进音频编码系统的编码效率,分别在三个关键模块上进行了算法优化,提出一种高效的编码实现方案.在心理声学模型中,使用新的时域分块峰值变换率准则代替感知熵来判断MDCT变换块的类型,降低误判、漏判概率,提高编码质量和速度;在分析滤波器中,基于双路并行计算技术,采用N/8点FFT算法实现N点MDCT变换,提高运算速度;在量化编码模块中,利用量化噪声能量公式,减少量化迭代次数,提高编码效率.该编码方案在保证音频质量的前提下,减少了50%的编码时间,满足实时性系统设计的要求.     

谓词模态逻辑到对应物理论的翻译

对应物理论(counterpart theory)是一阶逻辑的一种理论.Lewis利用谓词模态逻辑到对应物理论的翻译来研究谓词模态逻辑的性质,但是Lewis的翻译存在把不可满足的公式翻译为可满足公式的情况针对这个问题,提出了一种扩展语义的谓词模态逻辑,建立了扩展语义后谓词模态逻辑模型与对应物理论模型的一一对应关系,并在此基础上建立了谓词模态逻辑到对应物理论的语义忠实语义满翻译(faithful and full translation),其可确保将谓词模态逻辑的可满足公式和不可满足公式分别翻译为对应物理论的可满足公式和不可满足公式.由对应物理论是可靠的、完备的一阶逻辑的理论且语义忠实语义满翻译保持可靠性和完备性,进一步证明了扩展语义的谓词模态逻辑也是可靠和完备的.     

On the Hybrid Propositional Encodings of Planning

Recently, casting planning as propositional satisfiability (SAT) has been shown to be an efficient technique of plan synthesis. This article is a response to the recently proposed challenge of developing novel propositional encodings that are based on a combination of different types of plan refinements and characterizing the tradeoffs. We refer to these encodings as hybrid encodings. An investigation of these encodings is important, because this can give insights into what kinds of planning problems can be solved faster with hybrid encodings.
Encodings based on partial–order planning and state–space planning have been reported in previous research. We propose a new type of encoding called a unifying encoding that subsumes these two encodings. We also report on several other hybrid encodings. Next, we show how the satisfiability framework can be extended to incremental planning. State–space encoding is attractive because of its lower size and causal encoding is attractive because of its highest flexibility in reordering steps. We show that hybrid encodings have a higher size and a lower flexibility in step reordering and, thus, do not combine the best of these encodings. We discuss in detail several specific planning scenarios where hybrid encodings are likely to be superior to nonhybrid encodings.     

智能规划中的动作互斥编码方式研究

以规划领域中的动作为对象,研究规划方法中的动作互斥编码方式。介绍基于规划图的动作互斥编码、利用提取领域相关信息生成动作效果的直接阻碍与间接阻碍编码,以及依赖于域转移图动作间的长距离互斥编码,说明每类动作互斥编码的构造方法及其削减搜索空间、提高求解效率的作用。     

A solver for QBFs in negation normal form

Various problems in artificial intelligence can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula’s structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and describe a solver, $\ensuremath{\sf qpro}Various problems in artificial intelligence can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula’s structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and describe a solver, , which is able to handle arbitrary formulas. To this end, we extend algorithms for QBFs to the non-normal form case and compare with the leading normal form provers on several problems from the area of artificial intelligence. We prove properties of the algorithms generalized to non-clausal form by using a novel approach based on a sequent-style formulation of the calculus. This paper is based on an extended abstract presented at ECAI 2006 (see [16]). This work was supported by the Austrian Science Fund (FWF) under grant P18019, the Austrian Academic Exchange Service (?AD) under grant Amadée 2/2006, and by the Austrian Federal Ministry of Transport, Innovation and Technology BMVIT and the Austrian Research Promotion Agency FFG under grant FIT-IT-810806.     

Randomization of classical inference patterns and its application

By means of randomization, the concept of D-randomized truth degree of formulas in two-valued propositional logic is introduced, and it is proved that the set of values of D-randomized truth degree of formulas has no isolated point in [0,1]. The concepts of D-logic pseudo-metric and D-logic metric space are also introduced and it is proved that there is no isolated point in the space. The new built D-randomized concepts are extensions of the corresponding concepts in quantified logic. Moreover, it is proved that the basic logic connectives are continuous operators in D-logic metric space. Lastly, three different types of approximate reasoning patterns are proposed.     

A Dichotomy Theorem for Learning Quantified Boolean Formulas

We consider the following classes of quantified boolean formulas. Fix a finite set of basic boolean functions. Take conjunctions of these basic functions applied to variables and constants in arbitrary ways. Finally quantify existentially or universally some of the variables. We prove the following dichotomy theorem: For any set of basic boolean functions, the resulting set of formulas is either polynomially learnable from equivalence queries alone or else it is not PAC-predictable even with membership queries under cryptographic assumptions. Furthermore, we identify precisely which sets of basic functions are in which of the two cases.     

On linear logic planning and concurrency

We present an approach to linear logic planning where an explicit correspondence between partial order plans and multiplicative exponential linear logic proofs is established. This is performed by extracting partial order plans from sound and complete encodings of planning problems in multiplicative exponential linear logic. These partial order plans exhibit a non-interleaving behavioural concurrency semantics, i.e., labelled event structures. Relying on this fact, we argue that this work is a crucial step for establishing a common language for concurrency and planning that will allow to carry techniques and methods between these two fields.     

基于自动推理技术的智能规划方法

对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规划方法,并结合国际规划竞赛和相关论文等的实验结论说明上述方法的有效性和可行性.最后,提出目前基于自动推理技术的智能规划方法所面临的挑战、可能的处理方法以及与之相关的研究热点与趋势.     

Planning as Propositional CSP: From Walksat to Local Search Techniques for Action Graphs

Graphplan-style of planning can be formulated as an incremental propositional CSP where the (boolean) variables correspond to operator instantiations (actions) that are or are not scheduled at certain time steps. In this paper we present a framework for solving this class of propositional CSPs using local search in planning graphs. The search space consists of particular subgraphs of a planning graph corresponding to (complete) variable assignments, and representing partial plans. The operators for moving from one search state to the next one are graph modifications corresponding to revisions of the current variable assignment (partial plan), or to an extension of the represented CSP.Our techniques are implemented in a planner called LPG using various types of heuristics based on a parametrized objective function, where the parameters weight different constraint violations, and are dynamically evaluated using Lagrange multipliers. LPG's basic heuristic was inspired by Walksat, which in Kautz and Selman's Blackbox can be used to solve the SAT-encoding of a planning graph. An advantage of LPG is that its heuristics exploit the structure of the planning graph, while Blackbox relies on general heuristics for SAT-problems, and requires the translation of the planning graph into propositional clauses. Another major difference is that LPG can handle action execution costs to produce good quality plans. This is achieved by an anytime process minimizing an objective function based on the number of constraint violations in a plan and on its overall cost. Experimental results illustrate the efficiency of our approach, showing, in particular, that LPG is significantly faster than Blackbox and other planners based on planning graphs.