基于约束求解的微处理器功能验证程序生成

针对伪随机方法生成微处理器功能验证程序缺乏完备性、灵活性的问题,构建一种用于生成验证程序的C++约束函数库。以微处理器指令系统为对象,以约束满足问题的数学模型为理论依据,结合用户验证需求,利用约束函数库生成功能验证程序。验证结果表明,该方法开发验证程序简单、高效,加快了验证收敛速度。     

Automatic Generation of Redundant Models for Permutation Constraint Satisfaction Problems

If we have two representations of a problem as constraint satisfaction problem (CSP) models, it has been shown that combining the models using channeling constraints can increase constraint propagation in tree search CSP solvers. Handcrafting two CSP models for a problem, however, is often time-consuming. In this paper, we propose model induction, a process which generates a second CSP model from an existing model using channeling constraints, and study its theoretical properties. The generated induced model is in a different viewpoint, i.e., set of variables. It is mutually redundant to and can be combined with the input model, so that the combined model contains more redundant information, which is useful to increase constraint propagation. We also propose two methods of combining CSP models, namely model intersection and model channeling. The two methods allow combining two mutually redundant models in the same and different viewpoints respectively. We exploit the applications of model induction, intersection, and channeling and identify three new classes of combined models, which contain different amounts of redundant information. We construct combined models of permutation CSPs and show in extensive benchmark results that the combined models are more robust and efficient to solve than the single models.     

Constraint Solving for Proof Planning

Proof planning is an application of AI planning to theorem proving that employs plan operators that encapsulate mathematical proof techniques. Many proofs require the instantiation of variables; that is, mathematical objects with certain properties have to be constructed. This is particularly difficult for automated theorem provers if the instantiations have to satisfy requirements specific for a mathematical theory, for example, for finite sets or for real numbers, because in this case unification is insufficient for finding a proper instantiation. Often, constraint solving can be employed for this task. We describe a framework for the integration of constraint solving into proof planning that combines proof planners and stand-alone constraint solvers. Proof planning has some peculiar requirements that are not met by any off-the-shelf constraint-solving system. Therefore, we extended an existing propagation-based constraint solver in a generic way. This approach generalizes previous work on tackling the problem. It provides a more principled way and employs existing AI technology.     

数值型数据的泛概念树的自动生成方法

概念层次在数据挖掘中有着重要的作用 .通过自动生成概念层次 ,可有效地提高数据挖掘的效率 ,在不同层次上发现知识 .文中介绍基于云模型的数值型概念表示方法 ,通过云模型的期望值、熵和超熵三个数字特征有效地表达定性概念 ,并实现定性和定量的不确定转换 .通过云变换实现了泛概念树中叶结点的自动生成 ,并自动构造数值型数据的泛概念树 .同时 ,进一步研究了泛概念树中的概念爬升和跳跃的方法 ,为通过数据挖掘发现各层次知识提供了基础 .     

Solving Non-Linear Models with Saddle-Path Instabilities

Economic models derived from optimizing behavior are typically characterized by the properties of non-linearity and saddle-path instability. The typical solution method involves deriving the stable arm of the saddle-path and calculating suitable “jumps” to bring the path of endogenous variables onto this stable arm. The solution for the stable arm can be determined using a range of different approaches. In this paper we examine the extent to which the success of these alternative approaches can be evaluated. Any method of evaluation will be dependent upon the amount of information that is known about a particular model solution. For some deterministic models the only information known with certainty about the path of the model solution are values taken by steady-state solutions; the rest of the path must be approximated in some way based on numerical solutions derived from non-linear ordinary differential equations. In some special cases it is possible to derive a closed-form solution of the entire path. As an example of a model with a closed-form solution, we consider a simple linear model with two stable complex-valued eigenvalues and one unstable real-valued eigenvalue. The model is then employed as a benchmark to compare the properties of model solutions derived using two well-known solution algorithms. Because the model has complex-valued eigenvalues it will have cyclic dynamics and thus problems encountered in solving these dynamics will likely coincide with some of the problems that solution algorithms have in solving non-linear models. Since the entire solution path of the model is known, it is possible to derive deeper insights into the factors that are likely to ensure the success or failure of different solution approaches than would be the case if less information about the solution path was available.An earlier version of this paper was presented to the Ninth International Conference on Computing in Economics and Finance organized by the Society of Computational Economics, University of Washington at Seattle, July 11–13, 2003. Earlier versions of this paper have also been presented at seminars and workshops at the University of Oxford, at the University of Canterbury at Christchurch, and at the University of Melbourne. JEL Classifications: C63, E17     

Neural Logic Constraint Solving

Constraint Satisfaction Problems (CSPs) play a crucial role in Artificial Intelligence and in the real world. CSPs are in general NP-hard, and a general deterministic polynomial time algorithm is not known. CSPs can be reduced in polynomial time to the Satisfaction of a Conjunctive Normal Form (CNF-SAT). We present here techniques for solving CNF-SAT by means of several different simulated neural networks. The results of significant tests are described.     

数值流形方法物理覆盖的自动生成

数值流形方法物理覆盖的自动生成在工程应用中具有重要意义同时也是一项困难的工程.它主要包括两个难点,一是几何模型的建立相当耗时耗力;二是数学网格和物理网格的自动生成,从而生成物理覆盖.通过设计AutoCAD软件与数值流形方法程序的集成接口解决了建立高效准确的工程模型的难点问题;通过生成规则等边三角形数学网格系统,并利用由裂隙或块体边界彤成的物理网格对数学网格系统进行再剖分形成物理覆盖.将以上工作一体化就实现了物理覆盖的自动生成.仿真结果表明:可以有效提高数值流形方法程序的效率和准确性.     

两种空间约束求解算法

进行了3个方面的研究：(1)对由3点3面组成的空间约束系统进行了几何分析和推导，并且利用数值解验证了几何分析和推导的正确性，从而进一步完善了Hoffmann提出的基于图构造方法的约束求解方法；(2)将遗传模拟退火算法结合于空间约束求解中，有效地克服了基于图构造方法的可扩展性差的缺陷，并可以解决过约束和欠约束的情况；(3)应用遗传模拟退火算法对3点3面约束系统进行求解，分析比较了基于图构造方法和基于遗传模拟退火算法两种约束求解算法．     

用连杆机构几何约束求解

在这篇文章里,我们引入连杆机构作为新的工具,且证明这是完备的,也就是说,所有能构造性描述的图形能被连杆机构作出,这一类包括了所有只含距离约束的约束问题.作为一个应用,我们说明了超出Owen和Hoffmann的三角分解方法之外的最简单的约束图能被转化为纯几何构造形式.为了求解起源于连杆构造的方程,我们提出了一种基于动态轨迹生成的几何方法.     

用圆锥曲线求解几何约束问题

几何约束求解广泛应用于机械设计,化学分子形成,几何定理证明和勘探等诸多领域,用于求解几何约束问题主要有3种方法：数值方法,符号方法和构造法,构造法用于具有简单易行的特点,因此被大多数的参数化机械设计系统作为求解几何约束问题的基本方法,针对构造法中只采用直线和圆,即直尺和圆规,来作为基本的作图工具,引进了一种新的作图工具,圆锥曲线,并且证明了在引进圆锥曲线以后,作图的范围明显大于只用直尺和圆规作图的范围;证明了一个图形能用圆锥曲线作出的充分必要条件是这个图形可以用一个三角化的次数小于等于4的方程组来描述;由于三次和四次方程的解可以显式地表示出来,所以引进圆锥曲线作为一个新的作图工具仍然可以保持原来尺规作图的简洁性和完整性。     

非二元约束满足问题求解

在约束满足问题(CSP)的研究中，大部分工作集中在二元约束，但处理实际问题时，常常会遇到非二元约束的情况．该文在概要地讨论了两类求解非二元约束问题方法的基础上，研究了一种将约束传播技术和一般弧相容回溯算法相结合的非二元约束求解方法，并在设计开发的约束求解工具“明月SOLVER1.0”中实现了该方法，以典型例子给出了实现系统的运行结果．     

求解约束可满足问题的eSTR算法优化

表约束方法是1种外延式知识表示方法,每个约束通过元组集直接枚举出其在1个变量集上允许或禁止的所有元组,直观易于理解,在约束程序中得到了深入的研究,这是因为表约束出现在如设计、数据库、配置以及偏好建模等许多现实世界的应用中.但随着约束的增多及其元组集增大,占有的空间与相容性检测效率成了关键问题.eSTR是1个将STR扩展到高阶相容的算法,通过深入分析eSTR算法后发现有2种优化方式:PW\\+{sup}数据结构和极小约束范围,同时证明了在极小约束范围上,约束网络仍然能够维持PWC+GAC,其中极小约束范围可以通过删除约束元组集中相应的列来降低eSTR2算法的空间消耗,而PW\\+{sup}数据结构能够通过避免不必要的PW支持检测来减少eSTR2的CPU运行时间,实验结果表明：2种优化方式和eSTR2相结合后能够同时减少算法的空间消耗和CPU运行时间,在许多类实例上明显优于eSTR2和eSTR2w.     

几何约束求解研究综述

综述了几何约束求解的历史发展、研究现状和应用．对常见的4类求解方法：数值计算的方法、符号计算的方法、基于规则的方法、基于图论的方法做了详细的介绍．同时还列举了几何约束求解在计算机视觉、连杆设计、机器人、分子结构设计和计算机辅助教学等方面的应用实例．     

面向与历史无关造型的三维约束求解方法研究

以基于历史的造型系统中应用较为成熟的两项技术——特征编码和二维约束求解为基础,基于特征进行三维约束建模,从而打破传统的基于历史造型系统中特征之间的单向依赖关系;然后将三维约束关系映射到二维草图进行处理,简化了问题．该方法在InteSolid 2．0上实现．     

基因表达式中含有等式约束的处理方法

基因表达式编程（Gene Expression Programming,GEP）算法是遗传家族的新成员,被广泛用于函数发现。在微分方程中,要寻找的函数需要满足初始值,即有时希望GEP找到的函数能够满足一些等式约束条件。提出了一种带拉格朗日插值函数的GEP,对生成的种群加入插值函数使其满足等式约束,为提高GEP算法的进化效率和精度对目标目标值加入尺度变化,对其放大或者缩小。这样缩短了GEP算法的进化距离,从而提高了种群的进化效率。通过仿真实例,结果表明该方法可行有效。     

A Methodological View of Constraint Solving

Constraints are an effective tool to define sets of data by means of logical formulae. Our goal here is to survey the notion of constraint system and to give examples of constraint systems operating on various domains, such as natural, rational or real numbers, finite domains, and term domains. We classify the different methods used for solving constraints, syntactic methods based on transformations, semantic methods based on adequate representations of constraints, hybrid methods combining transformations and enumerations. The concepts and methods are illustrated via examples. We also discuss applications of constraints to various fields, such as programming, operations research, and theorem proving.     

面向集成变量化设计的三维几何约束求解方法

针对集成变量化设计中三维几何约束和装配几何约束的混合建模与求解问题,提出改进的有向图方法.该方法采用几何约束的基本约束表达和几何实体的抽象对偶实体表达,引入定向弧表达实体之间的内在依赖关系建立混合几何约束有向图模型;结合约束有向图的优化处理,实现了几何约束系统的细粒度分解和高效并行求解.最后用实例验证了文中方法的正确性和有效性.     

基于细胞元模型拓扑约束求解

在模型制造领域,对于拓扑约束的求解是一个比较新的课题,以往的研究一直局限在拓扑优化方面。而且对其应用也仅限于模型的定义方面,在模型的声明与约束求解方面却没有得到应用。文章提出一种基于细胞元模型拓扑约束求解方法,通过该方法可以确定模型拓扑声明的关系,文章假设一个模型是由一个或多个细胞元组成的,并且能够用这些细胞元的组合来表示,对模型进行拓扑约束求解就是用来确定细胞模型中的每个细胞元是否是全约束的。要做到这点,文章将每个细胞元用一个布尔变量表示,把拓扑约束问题映射成为布尔可满足性问题。再对新的问题进行求解,从而解决了模型的拓扑约束求解问题。     

基于子图的草图设计和约束求解

提出了一种基于子图的拟序列化草图设计方法。基于标识的约束模型统一了二维、三维约束,使得每个几何元素对应唯一的标识,几何元素之间的约束关系表示为标识之间的约束,这些约束被分为结构约束和尺寸约束。提出了基于序列化设计过程的约束求解方法。实验表明,该技术可快速有效地进行参数化草图设计和特征编辑。