An incremental algorithm for DLO quantifier elimination via constraint propagation

The first-order logical theory of dense linear order has long been known to admit quantifier elimination. This paper develops an explicit algorithm that yields an equivalent quantifier free form of its input formula. This algorithm performs existential quantifier elimination via constraint propagation. The result is computed incrementally using functional programming techniques. This approach may be of interest in implementing query languages for constraint databases.     

Out of order quantifier elimination for Standard Quantified Linear Programs

In this paper, we present an out of order quantifier elimination algorithm for a class of Quantified Linear Programs (QLPs) called Standard Quantified Linear Programs (SQLPs). QLPs in general and SQLPs in particular are extremely useful constraint logic programming structures that find wide applicability in the modeling of real-time schedulability specifications; see Subramani [Subramani, K., 2005a. A comprehensive framework for specifying clairvoyance, constraints and periodicity in real-time scheduling. The Computer Journal 48 (3), 259–272]. Consequently any algorithmic advance in their solution has a strong practical impact. Prior to this work, the only known approaches to the solution of QLPs involved sequential variable elimination; see Subramani [Subramani, K., 2003b. An analysis of quantified linear programs. In: Calude, C.S. et al. (Eds.), Proceedings of the 4th International Conference on Discrete Mathematics and Theoretical Computer Science. DMTCS. In: Lecture Notes in Computer Science, vol. 2731. Springer-Verlag, pp. 265–277]. In the sequential approach, the innermost quantified variable is eliminated first, followed by the variable which then becomes the innermost quantified variable and so on, until we are left with a single variable from which the satisfiability of the original formula is easily deduced. This approach is applicable in both discrete and continuous domains; however, it is to be noted that the logic demanding the sequential approach requires that the variables are discrete-valued. To the best of our knowledge, the necessity for sequential elimination over continuous-valued variables has not been investigated in the literature. The techniques used in the development of our elimination algorithm may find applications in domains such as classical logic and finite model theory. The final aspect of our research concerns the structure-preserving nature of the algorithm that we introduce here; in general, it is not known whether discrete domains admit such elimination procedures.     

Automatic computation of the complete root classification for a parametric polynomial

An improved algorithm, together with its implementation, is presented for the automatic computation of the complete root classification of a real parametric polynomial. The algorithm offers improved efficiency and a new test for non-realizable conditions. The improvement lies in the direct use of ‘sign lists’, obtained from the discriminant sequence, rather than ‘revised sign lists’. It is shown that the discriminant sequences, upon which the sign lists are based, are closely related both to Sturm–Habicht sequences and to subresultant sequences. Thus calculations based on any of these quantities are essentially equivalent.     

Cylindrical decomposition for systems transcendental in the first variable

We present a generalization of the Cylindrical Algebraic Decomposition (CAD) algorithm to systems of equations and inequalities in functions of the form p(x,f₁(x),…,f_m(x),y₁,…,y_n), where p∈Q[x,t₁,…,t_m,y₁,…,y_n] and f₁(x),…,f_m(x) are real univariate functions such that there exists a real root isolation algorithm for functions from the algebra Q[x,f₁(x),…,f_m(x)]. In particular, the algorithm applies when f₁(x),…,f_m(x) are real exp-log functions or tame elementary functions.     

Termination of linear programs with nonlinear constraints

Tiwari (2004) proved that the termination problem of a class of linear programs (loops with linear loop conditions and updates) over the reals is decidable through Jordan forms and eigenvector computation. Braverman (2006) proved that it is also decidable over the integers. Following their work, we consider the termination problems of three more general classes of programs which are loops with linear updates and three kinds of polynomial loop conditions, i.e., strict constraints, non-strict constraints and both strict and non-strict constraints, respectively. First, we prove that the termination problems of such loops over the integers are all undecidable. Then, for each class we provide an algorithm to decide the termination of such programs over the reals. The algorithms are complete for those programs satisfying a property, Non-Zero Minimum.     

碰撞问题中的量词消去算法的并行化研究

机器人技术中的碰撞问题可以被表示成量词消去问题，但由于有些碰撞问题的复杂性使得这些问题在单个微机上求解需要花费的时间很长或者根本就解不出来。本文提出了基于分布Maple系统下量词消去算法的并行化．并针对分布Maple系统的特点以及算法的特点，通过实例分析，给出了两种并行策略，以达到在Maple软件环境下提高处理器利用率，提高量词消去算法的效率的目的。     

Algorithm transformations for the data broadcast elimination method

VLSI technology has had tremendous success in revolutionizing computer design with processor arrays. Local communication and interconnection is a constraint that dictates the design of processor arrays. The shared bus and global access to memory are now no longer used, since they lower the speed. Consequently, parallel algorithms must be designed according to these constraints.

One of the problems that must be resolved for the above mentioned constraints is data broadcast elimination. Algorithms must be transformed into a form that uses data propagation instead of data broadcast.

Here systems of affine recurrence equations are analyzed and data broadcast is denned in context of the definition of data dependence and affine recurrence equations. A method for data broadcast elimination is introduced in [1] and expands the system of affine recurrence equations into new recurrence equations, that define data propagation and eliminates the data dependences where data broadcast occurs.

Parallel algorithms are usually given as a set of similar tasks repetitively performed on different data. The iteration form of presenting the algorithms is most common. Several techniques are introduced to transform the algorithm to a single assignment form of recurrence equations.

Some improvements of these techniques are presented to make the application of the data broadcast elimination method easier and more straight forward. The presented techniques are classified as the transformation of iterative algorithms to a recurrence form, the transformation of recurrence form to a single assignment form, and fulfilling the index forms of the algorithms.

A system of affine recurrence equations with the data broadcast property is always obtained by applying these procedures. The method of data broadcast elimination successfully transforms this system of affine recurrence equations into a system of uniform recurrence equations which can be used for parallel implementation on VLSI processor arrays.     

Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction

Typical bottom-up, forward-chaining reasoning systems such as hyperresolution lack goaldirectedness, while typical top-down, backward-chaining reasoning systems like Prolog or model elimination repeatedly solve the same goals. Reasoning systems that are goal-directed and avoid repeatedly solving the same goals can be constructed by formulating the top-down methods meta-theoretically for execution by a bottom-up reasoning system (hence, we use the term upside-down meta-interpretation). This formulation also facilitates the use of flexible search strategies, such as merit-ordered search, that are common to bottom-up reasoning systems. The model elimination theorem-proving procedure, its extension by an assumption rule for abduction, and its restriction to Horn clauses are adapted here for such upside-down meta-interpretation. This work can be regarded as an extension of the magic-sets or Alexander method for query evaluation in deductive databases to both non-Horn clauses and abductive reasoning.This research was supported by the National Science Foundation under Grant CCT-8922330 and by the Defense Advanced Research Projects Agency under Office of Naval Research Contract N00014-90-C-0220. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies, either expressed or implied, of the National Science Foundation, the Defense Advanced Research Projects Agency, or the United States Government.     

一种安全策略的冲突检测与消解方法

安全策略是系统安全管理的基础。分布式环境的复杂性使策略配置中不可避免地存在冲突。如何有效地分析检测策略冲突并解决冲突是应用安全策略的关键。提出了一个极具一般性的安全策略形式化描述方法,并定义了安全策略描述要素间的逻辑关系;给出了安全策略间的冲突分类描述;针对不同的冲突类型给出了相应的冲突检测算法及消解方法。     

A weighted mean filter with spatial-bias elimination for impulse noise removal

In this paper, we propose Unbiased Weighted Mean Filter (UWMF) for removing high-density impulse noise. Asymmetric distribution of corrupted pixels in the filtering window creates a spatial-bias towards the center of uncorrupted pixels. UWMF eliminates this bias by recalibrating the contribution factor (weight) of each uncorrupted pixel in such a way that the center shifts back to the center of the filtering window. The restoration process involves three sequential operations while convolving a filtering window over a contaminated image. Noise is detected, weights are recalibrated and the new intensity value is replaced by weighted mean using the recalibrated weights. Compared to the state-of-the-art impulse noise removal methods, UWMF provides superior performance, without requiring a fine-tuning for its parameters, in terms of both objective measurements and subjective assessments.     

A systolic processor array for the quadrant interlocking elimination method

In this paper a systolic array is presented for the solution of linear equations occurring in scientific and engineering calculations. The new systolic array is based on the parallel Quadrant Interlocking Elimination method of Evans and Hadjidimos [1].     

Stereoelectronic explanations for the mechanistic details of transimination and HF elimination reactions

The β-fluoroamines are commonly used as substrate analogs to determine the mechanistic details of enzymatic reactions. Presence of fluorine atom gives rise to the alterations in the electronic profile and the pK_a of molecules which results in mechanistic deviations. The fluorine-substituted mechanism-based substrate analogs are widely used in the inactivation of pyridoxal 5′-phosphate (PLP)-dependent enzymes. The presence of fluorine atom also alters the sequence of reactions taking place in PLP-dependent enzymes where the HF elimination reaction appears in between the transimination and inactivation reactions. Despite the amount of the works on β-fluoroamines, the effect of stereoelectronic differences on the transimination and HF elimination reactions taking place in PLP-dependent enzymes has not been investigated yet. A density functional theory study is conducted to elucidate mechanistic details of the reactions occurring in PLP-dependent enzymes. In order to understand the mechanistic insights of different isomers and the effect of the fluorine atom, 4-amino-3-fluorobutanoic acid (3-F-GABA) enantiomers are chosen to be investigated besides 4-aminobutanoic acid (GABA), which is the natural substrate for γ-aminobutyric acid aminotransferase (GABA-AT). The investigated β-fluoroamines are the experimentally proposed potential inhibitors of PLP-dependent enzyme GABA-AT.     

The method of elimination of unknowns for systems of linear inequalities with graph structure

The method of elimination of unknowns in a system of linear inequalities is considered. This method is used to solve systems of linear inequalities whose structure is defined by some graph. The concepts of terminal and intermediate graphs are introduced. A new system of inequalities derived by eliminating a group of unknowns that correspond to these subgraphs is described. Translated from Kibernetika i Sistemnyi Analiz, No. 5, pp. 66–74, September–October, 1999.     

Parallel Gauss-Jordan elimination for the solution of dense linear systems

Any factorization/back substitution scheme for the solution of linear systems consists of two phases which are different in nature, and hence may be inefficient for parallel implementation on a single computational network. The Gauss-Jordan elimination scheme unifies the nature of the two phases of the solution process and thus seems to be more suitable for parallel architectures, especially if reconfiguration of the communication pattern is not permitted. In this communication, a computational network for the Gauss-Jordan algorithm is presented. This network compares favorably with optimal implementations of the Gauss elimination/back substitution algorithm.     

Modular inference of subprogram contracts for safety checking

Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently.     

PTN网状网拓扑设计动态删枝算法

针对分组传送网(PTN)网状网拓扑的特点,为提高PTN网状网拓扑设计中的计算效率,提出了一种改进的PTN网状网拓扑设计动态删枝算法(SR-DE)。该算法先分析PTN网络资源和业务信息,在对优化网络成本循环中动态改变每次循环中删除冗余链路数量,并对业务进行稳定路由,因此可以减少了网络权值的改变次数,避免对业务重复路由,提高了计算效率。模拟仿真结果表明,该算法有效地提高了设计满足业务需求PTN网状网拓扑的计算效率。     

State elimination and identifiability of the delay parameter for nonlinear time-delay systems

The identifiability of the delay parameter for nonlinear systems with a single constant time delay is analyzed. We show the existence of input–output equations and relate the identifiability of the delay parameter to their form. Explicit criteria based on rank calculations are formulated. The identifiability of the delay parameter is shown not to be directly related to the well-characterized identifiability/observability of the other system parameters/states.     

An application of PSO technique for harmonic elimination in a PWM inverter

Harmonic elimination problem in PWM inverter is treated as an optimization problem and solved using particle swarm optimization (PSO) technique. The derived equation for computation of total harmonic distortion (THD) of the output voltage of PWM inverter is used as the objective function in the PSO algorithm. The objective function is minimized to contribute the minimum THD in the voltage waveform and the corresponding switching angles are computed. The method is applied to investigate the switching patterns of both unipolar and bipolar case. While minimizing the objective function, the individual selected harmonics like 5th, 7th, 11th and 13th can be controlled within the allowable limits by incorporating the constraints in the PSO algorithm. The results of the unipolar case using five switching angles are compared with that of a recently reported work and it is observed that the proposed method is effective in reducing the voltage THD in a wide range of modulation index. The simulated results are also validated through suitable experiments.     

一种自适应的运动目标阴影消除新算法

精确地消除活动阴影对运动目标的影响是智能视频监控的核心任务之一,对此提出了一种基于局部纹理分析的自适应阴影消除新算法。进行了基于高斯混合模型的背景重建,并根据阴影的光学特性进行了阴影区域的预检测,得到疑似阴影区域;提出了一种新的自适应动态纹理分析方法并在此基础上实现了活动阴影的检测与消除。实验结果验证了算法的有效性和实用性。