constructing finite algebras with falcon

The generation of models and counterexamples is an important form of reasoning. In this paper, we give a formal account of a system, called FALCON, for constructing finite algebras from given equational axioms. The abstract algorithms, as well as some implementation details and sample applications, are presented. The generation of finite models is viewed as a constraint satisfaction problem, with ground instances of the axioms as constraints. One feature of the system is that it employs a very simple technique, called the least number heuristic, to eliminate isomorphic (partial) models, thus reducing the size of the search space. The correctness of the heuristic is proved. Some experimental data are given to show the performance and applications of the system.

SAT和DSOLS问题的研究

约束可满足性问题（Constraint Satisfaction Problem,CSP）是在人工智能领域被广泛研究的一类问题。对CSP问题的研究有两种重要的思路：一种思路是用统一的模型来表示CSP，然后用针对这个统一模型的通用工具进行求解；另外一种思路是针对不同的CSP问题开发专门工具，设计不同的算法和数据结构来求解。 本文研究了两个CSP问题：SAT(SATisfiability problem)和DSOLS(DoublySelf-Orthogonal Latin Squares)。CSP可以方便的转换为SAT来求解，因此对SAT的研究对很多问题具有重大意义。本文介绍了当前流行的SAT solver的一些技术，也提出一种新的搜索空间裁剪策略Local Lemma。DSOLS是一种具有特定性质的拉丁方，本文对它的研究不仅仅因为它的应用意义。更重要的是它作为一个特定的CSP问题，可以用来比较通用工具和专门工具的优劣。本文尝试了把DSOLS转化为SAT求解，也试过用一般CSP的思路来求解，最后提出了一种针对性的高效算法并开发了一个专门工具DSOLver，用这个工具证明了一个开放问题：DSOLS(10)不存在。

参数化系统安全性的启发式符号验证

参数化系统(paramterized system)是指包含特定有限状态进程多个实例的并发系统,其中的参数是指系统内进程实例的数目,即系统的规模.反向可达性分析(backward reachability analysis)已被广泛用于验证参数化系统是否满足以向上封闭(upward-closed)集合表示的安全性(safety property).与有限状态系统验证相类似,参数化系统的验证同样也面临着状态爆炸(state explosion)问题,并且模型检测算法的有效性依赖于如何采用有效的数据结构表示状态集合.针对表示无穷状态的向上封闭集合,研究人员提出了多种基于约束(constraint-based)的符号表示方法.但这些方法依然面临着符号状态爆炸(symbolic state explosion)问题或者其包含判定问题,即判断一个约束条件集合符号化表示的实际状态集合是否为另一约束条件集合所对应的状态集合的子集,是Co-NP完全问题.因此,虽然有限状态验证技术能够验证一些具有一定规模的问题,但现有针对参数化系统的验证方法所能解决的问题的规模较为有限,需要近一步提高模型检测算法的效率.针对参数化系统提出了加快反向可达性分析的多个启发式规则,实验结果表明,这些启发式规则可以使算法的效率提高几个数量级,从而有助于解决现有参数化系统验证方法所存在的问题.

网驰平台统一部署框架的设计与实现

随着软件技术的发展，越来越多的应用系统采用组件技术来提高系统开发效率。企业级应用通常通过集成多种组件形成复杂软件，完成业务功能。各种组件之间存在直接或者间接的依赖关系以及配置限制，使得当前以手工为主的组件部署效率低下且容易出错。 针对分布式组件系统部署面临的问题，论文建立了一种基于约束规则的统一部署框架，支持各种组件的统一一致的自动化部署。论文首先分析总结了组件部署现状，设计了一种统一部署描述模型，刻画不同组件的部署需求，包括部署单元、部署目标、以及约束规则，为部署计划正确性验证以及自动部署提供基础。针对组件部署中缺乏提前验证的问题，论文还设计了一套基于约束规则的验证机制。通过总结当前多种组件平台中领域相关的约束规则，对约束规则进行分类，并使用声明式对象约束语言（Object Constraint Language）刻画约束规则。为不同类型约束设计了验证算法，并且设计了包含约束规则验证活动的组件部署流程。最后论文给出了网驰平台统一部署系统OnceUD的设计与实现，将前述研究成果引入其中，并通过应用案例评估了系统的功能。

协同环境下基于角色的细粒度委托限制框架

提出了基于角色的细粒度委托限制框架，将角色分为对象角色和委托角色，实现细粒度的控制。分析了三类委托限制：时间限制、禁止限制和义务限制。针对不同类型定义相应限制规则，并用于描述条件委托和受控使用，条件委托要求满足条件后执行委托操作，防止非法扩散；受控使用约束委托权限，防止权限滥用。多个委托限制规则之间可能冲突，给出了时间复杂度为O（n^2）的基于图论的一致性检测算法。

基于收益机制发布/订阅系统时间约束保障技术

发布／订阅系统技术具有异步、松散耦合和多对多通信的特点，有着广阔的应用前景．但是，已有的发布／订阅系统技术不能满足动态环境下有延迟需求的应用要求．针对时间约束问题，扩展了发布／订阅系统的语法，建立了延迟模型，提出了一种基于收益机制的分布式发布／订阅系统时间约束保障技术和使系统获益最大化的调度算法MTEP（maximumto tal earning priority），其特点是能够满足订阅者和发布者指定延迟约束的需求，通过与订阅者商定的价格和违约成本信息来有效地利用网络带宽，适应网络环境的动态变化．实验结果表明，该调度策略和FCFS（first come first service）、最短时间优先和固定优先级等传统策略相比，可使订阅者接收到的有效事件明显增多，并使系统收益显著改善．

基于逻辑"或"约束优化的实时系统设计

标准约束优化问题的等式或不等式约束之间是逻辑“与”关系，目前已经有很多高效、收敛的优化算法．但是，在实际应用中有很多更一般的约束优化问题，其等式或不等式约束之间不仅包含逻辑“与”关系，而且还包含逻辑“或”关系，现有的针对标准约束优化问题的各种算法不再适用，给出一种新的数学变换方法，把具有逻辑“或”关系的不等式约束转换为一组具有逻辑“与”关系的不等式，并应用到实时单调速率调度算法的可调度性判定充要条件中，把实时系统设计表示成混合布尔型整数规划问题，利用经典的分支定界法求解．实验部分指出了各种方法的优缺点．

基于空间约束模型的目标识别

目标识别技术在现实生活中的很多领域都有广泛的应用，但是由于遮挡，视角变换等因素的影响，目标识别技术仍面临着巨大的挑战。局部特征由于其本身固有的局部性，引起了人们的重视。结合空间分布约束，局部特征可以包含高层的语义信息，能够提高目标识别算法抗遮挡和视角变化的能力。本文分析对比了当前流行的局部特征检测方法，描述方法以及空间分布约束方法，并提出了一种“中心-特征”结构模型以及相应的目标识别方法。 首先介绍局部特征检测方法，深入研究局部特征描述方法，并从原理，不变性，匹配速度，适用情形等方面进行了比较分析。 综合显式模型和隐式模型的优缺点，提出了一种“中心-特征”结构的模型。该模型以目标中心作为衡量所有局部特征之间位置关系的参考点，既保留了星形模型等的准确性，同时又去掉了特殊结点，避免了特殊结点缺失带来的不利影响，提高了算法的稳定性。 基于上述空间分布约束模型提出了相应的目标识别算法。该算法同时考虑表面特征和空间位置之间的匹配程度。基于模板中目标的表面特征和形状因素构造空间分布约束模型，利用待检测目标的表面特征信息形成相关假设，通过假设检验定量衡量目标出现的位置及可能性，并提出了一种搜索目标中心位置的加速算法。实验验证了算法在相似变换及仿射变换下的有效性，且具有一定的抗缺失能力。

概念设计中基于笔式手势的交互计算研究

基于笔式手势的自然交互是支持概念设计创新的有效方式.提出了一种笔式手势的层次概念模型,结合基于约束的自由勾画和上下文感知技术描述了手势设计方式,进一步讨论了手势内部的约束建立和求解算法;基于手势应用的范式,给出了概念设计中特征手势建模的应用实例,通过与传统建模和交互方式的对比,验证了特征手势建模的方便性.给出一个自然、高效的方法,以基于手势的方式来完成概念设计构思过程,采用笔式交互快速自然地记录下设计思路,所实现的系统方便了用户的创新设计,改善了人机交互模式.

基于几何约束求解的完备方法

针对参数化CAD在约束求解中的应用,提出了基于智能连杆的算法,该算法在扩充几何作图范围、改善算法复杂度方面都有明显的优势.将其同LIM0算法、几何变换方法、C-Tree算法、数值求解方法等方法相互融合,能够组成一套非常完备的几何约束求解框架,来完成对平面和空间几何约束问题的自动求解与图像生成.将该算法应用于智能动态几何软件的设计中,实验显示可以取得令人满意的结果.

目标检测中的空间位置约束模型

针对目前常见的星形模型等易受部件缺失影响的问题,提出一种空间位置约束模型.该模型以目标中心作为参考点,衡量所有局部特征之间的位置关系,避免了特殊结点缺失带来的不利影响.基于模板中目标的表面特征和形状因素构造空间位置约束模型,利用待检测目标的表面特征信息形成相关假设,通过假设检验定量地衡量目标出现的位置及可能性,并提出了一种搜索目标中心位置的加速算法.实验结果表明,该空间位置约束模型不受部件缺失的影响,性能稳定.

construction of feature-matching perception in virtual assembly

An important characteristic of virtual assembly is interaction. Traditional di-rect manipulation in virtual assembly relies on dynamic collision detection, which is very time-consuming and even impossible in desktop virtual assembly environment. Feature-matching isa critical process in harmonious virtual assembly, and is the premise of assembly constraint sens-ing. This paper puts forward an active object-based feature-matching perception mechanism and afeature-matching interactive computing process, both of which make the direct manipulation in vir-tual assembly break away from collision detection. They also help to enhance virtual environmentunderstandability of user intention and promote interaction performance. Experimental resultsshow that this perception mechanism can ensure that users achieve real-time direct manipulationin desktop virtual environment.

东北3省人类活动与水土流失关系的演进

受人类对土地过度垦殖及不合理耕作利用的影响,水土流失正在成为制约我国东北地区耕地可持续利用和粮食生产的主要因素。在对历史资料甄别与整理的基础上,分析近代以来东北3省区人口、土地利用变化及其与水土流失关系的演变。结果表明:到20世纪中期,东北地区人口压力达到60~70人/km2,伴随着生活方式的转变,机械化技术的应用,林草湿地被垦殖,森林覆盖率降到30%,垦殖率达30%,使区域性水土流失问题日益严重。

The Incident Angle Dependence of Quantum Efficiency of GaAs Based RCE Photodetectors

The theoretical analysis and experimental measurement on the incident angle dependence of quantum efficiency of GaAs based resonant cavity enhanced (RCE) photodetector is presented. By changing the angle of incoming light, about 40 nm wavelength variation of peak quantum efficiency is obtained. The peak quantum efficiency and optical bandwidth at different mode corresponding to different angle incidence is characterized with different absorption dependence on wavelength. The convenient angle tuning of resonant mode will be helpful to relax the strict constraint of RCE photodetector to light source with narrow emission spectrum such applications in space optical detections and communications.

Analysis for the angle dependence of GaAs based RCE photodetectors

The theoretical analysis and experimental measurement on the angle dependence of quantum efficiency of GaAs based resonant cavity enhanced (RCE) photodetector is presented. By changing the angle of incoming light, about 40mn wavelength variation of peak quantum efficiency has been experimentally obtained. The peak quantum efficiency and optical bandwidth at different mode corresponding to different angle incidence have been characterized with different absorption dependence on wavelength. The convenient angle tuning of resonant mode will be helpful to relax the strict constraint of RCE photodetector to light source with narrow emission spectrum while especially applied in space optical detections and communications.