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)不存在。

面向多目标追踪的无线传感器网络协同任务分配研究

在基于动态联盟机制的无线传感器网络协同任务分配研究中,为了解决多目标追踪带来的联盟间的资源竞争问题,本文采用分布式约束满足算法解决多动态联盟间的协同问题.根据无线传感器网络多目标追踪的应用需求,建立了基于动态联盟机制的协同任务分配的分布式约束满足模型,并采用分布式随机算法求解满足约束条件的动态联盟集合,实现多动态联盟间的协同.仿真结果表明,分布式约束满足算法有效地解决了多目标追踪中多个动态联盟间的资源竞争问题,能够有效降低系统的能量消耗。

Genetic evidence of a strong functional constraint of neurotrypsin during primate evolution

Neurotrypsin is one of the extra-cellular serine proteases that are predominantly expressed in the brain and involved in neuronal development and function. Mutations in humans are associated with autosomal recessive non-syndromic mental retardation (MR). We studied the molecular evolution of neurotrypsin by sequencing the coding region of neurotrypsin in 11 representative non-human primate species covering great apes, lesser apes, Old World monkeys and New World monkeys. Our results demonstrated a strong functional constraint of neurotrypsin that was caused by strong purifying selection during primate evolution, an implication of an essential functional role of neurotrypsin in primate cognition. Further analysis indicated that the purifying selection was in fact acting on the SRCR domains of neurotrypsin, which mediate the binding activity of neurotrypsin to cell surface or extracellular proteins. In addition, by comparing primates with three other mammalian orders, we demonstrated that the absence of the first copy of the SRCR domain (exon 2 and 3) in mouse and rat was due to the deletion of this segment in the murine lineage. Copyright (C) 2005 S. Karger AG, Basel.

a constraint solver and its application to path feasibility analysis

Many testing methods are based on program paths. A well-known problem with them is that some paths are infeasible. To decide the feasibility of paths, we may solve a set of constraints. In this paper, we describe constraint-based tools that can be used for this purpose. They accept constraints expressed in a natural form, which may involve variables of different types such as integers, Booleans, reals and fixed-size arrays. The constraint solver is an extension of a Boolean satisfiability checker and it makes use of a linear programming package. The solving algorithm is described, and examples are given to illustrate the use of the tools. For many paths in the testing literature, their feasibility can be decided in a reasonable amount of time.

etl workflow analysis and verification using backwards constraint propagation

University of Twente; Centre for Telematics and Information Technology; Netherlands Organisation for Scientific Research; Jacquard; Capgemini

Quantified MS analysis applied to combinatorial heterogeneous catalyst libraries

A high-throughput screening system for secondary catalyst libraries has been developed by incorporation of an 80-pass reactor and a quantified multistream mass spectrometer screening (MSMSS) technique. With a low-melting alloy as the heating medium, a uniform reaction temperature could be obtained in the multistream reactor (maximum temperature differences are less than 1 K at 673 K). Quantification of the results was realized by combination of a gas chromatogram with the MSMSS, which could provide the product selectivities of each catalyst in a heterogeneous catalyst library. Because the catalyst loading of each reaction tube is comparable to that of the conventional microreaction system and because the parallel reactions could be operated under identical conditions (homogeneous temperature, same pressure and WHSV), the reaction results of a promising catalyst selected from the library could be reasonably applied to the further scale-up of the system. The aldol condensation of acetone, with obvious differences in the product distribution over different kind of catalysts, was selected as a model reaction to validate the screening system.