Improving Linear Constraint Propagation by Changing Constraint Representation

Propagation based finite domain solvers provide a general mechanism for solving combinatorial problems. Different propagation methods can be used in conjunction by communicating through the domains of shared variables. The flexibility that this entails has been an important factor in the success of propagation based solving for solving hard combinatorial problems. In this paper we investigate how linear integer constraints should be represented in order that propagation can determine strong domain information. We identify two kinds of substitution which can improve propagation solvers, and can never weaken the domain information. This leads us to an alternate approach to propagation based solving where the form of constraints is modified by substitution as computation progresses. We compare and contrast a solver using substitution against an indexical based solver, the current method of choice for implementing propagation based constraint solvers, identifying the relative advantages and disadvantages of the two approaches. In doing so, we investigate a number of choices in propagation solvers and their effects on a suite of benchmarks.     

A Repeated-Update Problem in the DeltaBlue Algorithm

We observe a repeated-update problem in the process of updating walkabout strengths of the DeltaBlue algorithm, which is known as a fast constraint solving method based on local propagation. According to the basic references on the DeltaBlue algorithm, the time complexity of the planning phase is described as O(MN) for a constraint problem such that the number of constraints is N and the maximum number of methods a constraint has is M . We, however, point out that the time complexity is not O(MN) using a very simple example. In this example, the time complexity is exponential order for N . Then we present a corrected DeltaBlue algorithm whose time complexity is O(EN ²) for a constraint problem such that the number of constraints is N and the maximum number of variables a constraint has is E . Finally we measure the performance of the corrected DeltaBlue algorithm using two benchmarks.     

Geometric constraint solving with geometric transformation

This paper proposes two algorithms for solving geometric constraint systems. The first algorithm is for constrained systems without loops and has linear complexity. The second algorithm can solve constraint systems with loops. The latter algorithm is of quadratic complexity and is complete for constraint problems about simple polygons. The key to it is to combine the idea of graph based methods for geometric constraint solving and geometric transformations coming from rule-based methods.     

Dealing with redundancy and inconsistency in constructive geometric constraint solving

General constructive geometric constraint solvers are pre-processed by a degree-of-freedom analysis, which enables efficient graph decomposition and recombination. However, all these methods are based on the assumption that structural rigidity automatically assures solvability. In this paper, we show that this assumption fails in numerous, even the most basic, configurations. We introduce several simple but efficient rules aimed to additionally analyse solvability in such cases. Another novelty addresses conditional constraints between three or more geometric parts, rules for their simplification and a redundancy check. All these functionalities are built into our original 2D geometric constraint solver, based on concepts of rigid clusters and constrained-angle (CA) sets.     

Revisiting decomposition analysis of geometric constraint graphs

Geometric problems defined by constraints can be represented by geometric constraint graphs whose nodes are geometric elements and whose arcs represent geometric constraints. Reduction and decomposition are techniques commonly used to analyze geometric constraint graphs in geometric constraint solving.In this paper we first introduce the concept of deficit of a constraint graph. Then we give a new formalization of the decomposition algorithm due to Owen. This new formalization is based on preserving the deficit rather than on computing triconnected components of the graph and is simpler. Finally we apply tree decompositions to prove that the class of problems solved by the formalizations studied here and other formalizations reported in the literature is the same.     

基于约束的主动规则终止性分析

终止性是主动规则所需的最重要的一个性质,但规则的终止性检查通常是不可判定的.已有的静态分析方法非常保守,SQL3标准也没有提供保证终止的机制,所以商业数据库限制规则级联触发的最大次数确保终止.由于规则可看成数据库状态转换器,而约束能够表示所有可能的数据库状态,基于约束表示的数据库状态及约束求解,模拟规则处理,可得到更精确的终止性结论.     

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

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

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

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

GC-MCR:有向图约束指导的并发缺陷检测方法

约束求解应用到程序分析的多个领域,在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用,然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响,因此,针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题,给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织,以降低在并发程序状态空间内的探索开销.比如,最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而,其在约束构建过程中会产生大量冗余和冲突的约束,大幅度增加了约束求解的时间以及约束求解器的调用次数,降低了并发程序状态空间的探索效率.针对上述问题,提出了一种有向图约束指导的并发缺陷检测方法 GC-MCR (directed graph constraint-guided maximal causalityreduction).该方法旨在通过使用有向图对约束进行过滤和约减,从而提高约束求解速度,并进一步提高并发程序状态空间的探索效率.实验结果表明:GC-MCR方法构建的有向图可以有效优化约束的表达式,从而提高约束求解器的求解速度并减少求解器的调用次...     

A Foundation of Solution Methods for Constraint Hierarchies

Constraint hierarchies provide a framework for soft constraints, and have been applied to areas such as artificial intelligence, logic programming, and user interfaces. In this framework, constraints are associated with hierarchical preferences or priorities called strengths, and may be relaxed if they conflict with stronger constraints. To utilize constraint hierarchies, researchers have designed and implemented various practical constraint satisfaction algorithms. Although existing algorithms can be categorized into several approaches, what kinds of algorithms are possible has been unclear from a more general viewpoint. In this paper, we propose a novel theory called generalized local propagation as a foundation of algorithms for solving constraint hierarchies. This theory formalizes a way to express algorithms as constraint scheduling, and presents theorems that support possible approaches. A benefit of this theory is that it covers algorithms using constraint hierarchy solution criteria known as global comparators, for which only a small number of algorithms have been implemented. With this theory, we provide a new classification of solution criteria based on their difficulties in constraint satisfaction. We also discuss how existing algorithms are related to our theory, which will be helpful in designing new algorithms.     

GC-MCR: Directed Graph Constraint-guided Concurrent Bug Detection Method

Constraint solving has been applied to many domains of program analysis and is further used in concurrent program analysis. Concurrent programs have been widely used with the rapid development of multi-core processors. However, concurrent bugs threaten the security and reliability of concurrent programs, and thus it is of great importance to detect concurrent bugs. The explosion of thread interleaving caused by the uncertainty of the execution of concurrent program threads brings some challenges to the detection of concurrent bugs. Existing concurrent defect detection algorithms reduce the exploration cost in the state space of concurrent programs by reducing invalid thread interleaving. For example, the maximal causal model algorithm transforms the state space exploration problem of concurrent programs into a constraint solving problem. However, it will produce a large number of redundant and conflicting constraints during constraint construction, which greatly prolongs the time of constraint solving, increases the number of constraint solver calls, and reduces the exploration efficiency of concurrent program state space. Thus, this study proposes a directed graph constraint-guided maximal causality reduction method, called GC-MCR. This method aims to improve the speed of constraint solving and the efficiency of the state space exploration of concurrent programs by filtering and reducing constraints using directed graphs. The experimental results show that the GC-MCR method can effectively optimize the expression of constraints, so as to improve the solving speed of the constraint solver and reduce the number of solver calls. Compared with the existing J-MCR method, GC-MCR can significantly improve the detection efficiency of concurrent program bugs without reducing the detection ability of concurrent bugs, and the test time on 38 groups of concurrent test programs widely used by existing research methods can be reduced by 34.01% on average.     

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

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

The CCUBE Constraint Object-Oriented Database System

Constraints provide a flexible and uniform way to represent diverse data capturing spatio-temporal behavior, complex modeling requirements, partial and incomplete information etc, and have been used in a wide variety of application domains. Constraint databases have recently emerged to deeply integrate data captured by constraints in databases. This paper reports on the development of the first constraint object-oriented database system, CCUBE, and describes its specification, design and implementation. The CCUBE system is designed to be used for the implementation and optimization of high-level constraint object-oriented query languages as well as for directly building software systems requiring extensible use of constraint database features. The CCUBE data manipulation language, Constraint Comprehension Calculus, is an integration of a constraint calculus for extensible constraint domains within monoid comprehensions, which serve as an optimization-level language for object-oriented queries. The data model for the constraint calculus is based on constraint spatio-temporal (CST) objects that may hold spatial, temporal or constraint data, conceptually represented by constraints. New CST objects are constructed, manipulated and queried by means of the constraint calculus. The model for the monoid comprehensions, in turn, is based on the notion of monoids, which is a generalization of collection and aggregation types. The focal point of our work is achieving the right balance between the expressiveness, complexity and representation usefulness, without which the practical use of the system would not be possible. To that end, CCUBE constraint calculus guarantees polynomial time data complexity, and, furthermore, is tightly integrated with the monoid comprehensions to allow deeply interleaved global optimization.     

半在线调度中约束求解算法研究

很多实际调度问题是半在线的. 尝试运用人工智能方法来求解半在线调度问题, 首先简要介绍了半在线调度问题并对其约束模型进行了分类, 通过引入单调性约束扩展的相关概念, 从约束建模角度形式化描述 了一类动态约束扩展, 并在此基础上设计了一个完备动态约束求解算法, 最后给出该算法在半在线离散资源约束调度求解的应用算例. 测试结果表明, 该算法是可行有效的.     

通用几何约束系统统一建模研究

在几何约束和几何实体的基本约束和欧拉参数表达的基础上,研究了通用几何约束系统的统一建模问题。通过对三维几何实体姿态约束和位置约束解耦性的分析,抽象出球实体、盒体和球盒体三种基本几何实体表达空间几何实体,并以基本约束的组合表达几何约束,形成几何约束模型特有的层次结构;并以有向图管理几何约束系统,可以清晰地反映姿态约束和位置约束的解耦性,实现约束系统的细粒度分解,得到规模更小的求解序列,实现高效求解。方法实现于原型系统WhutVAS中。     

多元约束混合搜索算法研究

解空间搜索是约束求解的关键环节. 目前较为常用的搜索算法一般是基于二元约束或单一搜索策略设计的. 本文设计了六个基于多元约束的混合搜索算法(BM_GASBJ, BM_GBJ, BM_CBJ, FC_GASBJ, FC_GBJ, FC_CBJ), 它们分别混合同一类搜索策略中不同算法或不同类搜索策略; 分析并给出了不同混合算法的性能差异. 系统测试结果表明混合搜索算法明显提高了解搜索效率和约束求解系统的性能.     

一种欠约束草图求解方法的研究

基于约束的参数化描述及求解是计算机辅助设计研究的一个热点，欠约束图的求解是参数化设计的基本问题，为了提高欠约束草图求解的参数化设计效率，提出了一种基于隐式约束优先级的欠约束草图求解方法，并首先给出了欠约束图求解的一般方法以及欠约束图的基本特征，提出了利用隐式约束去匹配缺少的显式约束；然后将隐式约束按照一定的规则分成不同的优先级，再利用优先级高的隐式约束去匹配变动约束图中的欠约束，直到完成约束图的有向化；最后，探讨了无尺寸约束图有向化过程中的基本特点，并给出了无尺寸约束图的求解算法和应用实例。实例应用结果表明，效果较好。     

Nicolog: A simple yet powerful cc(FD) language

In this paper, we describe Nicolog, a language with capabilities similar to recently developed constraint logic programming (CLP) languages such as CLP(BNR), clp(FD), and cc(FD). Central to Nicolog are projection constraints (PCs), a sublanguage for compiling and optimizing constraint propagation in numeric and Boolean domains. PCs are an interesting generalization of the indexical constraints introduced in cc(FD) and also found in clp(FD). Nicolog compiles a very general class of built-in constraints into equivalent sets of PCs, allowing an arbitrary mixture of integer (easily extensible to real) and Boolean operations. Nicolog also lets the user program PCs directly, making it possible to implement new sophisticated propagation procedures. We show that PCs are a simple, efficient, and flexible way to implement most of the propagation procedures possible in other FD CLP systems. These include procedures for cardinality, constructive disjunction, implication, and mixed Boolean/numeric constraints. Empirical results with a simple prototype Nicolog implementation based on the WAM architecture show it can solve hard problems with speed comparable to the fastest existing CLP systems.     

面向HDL描述基于路径覆盖的模拟矢量自动生成方法研究

提出和实现了一种面向HDL描述基于路径覆盖的模拟矢量自动生成方法,该方法在约束生成时只考虑控制语句的条件表达式，可有效避免生成冗余约束；利用扩展的决策图模型解决了中间信号到初始输入的传播问题和信号依赖关系问题，以及处理各种HDL描述风格的问题；采用约束逻辑编程方法解决了由位、位向量和整型变量组成的约束系统的统一处理问题,实验结果表明该方法能加快模拟矢量生成速度，提高路径覆盖率．生成的模拟矢量也能用于低层次设计验证和故障模拟，加快了设计进度,将该方法的原型系统用于一个32位微处理器核RTL级验证，发现了RTL级设计描述中的错误．