A mechanical design "compiler" has been developed which, given an appropriate schematic, specifications, and utility function for a mechanical design, returns catalog numbers for an optimal implementation. The compiler has been successfully tested on a variety of mechanical and hydraulic power transmission designs and a few temperature sensing designs. Times required have been at worst proportional to the logarithm of the number of possible combinations of catalog numbers.

Déterminer si un problème de satisfaction de contraintes (CSP) a une solution ou non est NP-complet. Les CSP sont résolus par inférence (c’est-à-dire, en appliquant un algorithme de cohérence), par énumération (c’est-à-dire en effectuant une recherche avec retour sur trace ou backtracking), ou, plus souvent, en intercalant les deux mécanismes. La propriété de cohérence la plus courante appliquée en cours du backtracking est la GAC (Generalized Arc Consistency). Au cours des dernières années, de nouveaux algorithmes pour appliquer des cohérences plus fortes que le GAC ont été proposés et montrés comme étant nécessaires pour résoudre les problèmes difficiles.Nous nous attaquons à la question de balancer d’une part le coût et, d’autre part, le pouvoir d’élagage des algorithmes de cohérence et posons cette question comme étant celle de déterminer où, quand et combien une cohérence doit-elle être appliquée en cours de backtracking. Pour répondre à la question « où », nous exploitons la structure topologique d'une instance du problème et focalisons la cohérence forte là où des structures cycliques apparaissent. Pour répondre à la question « quand », nous proposons une stratégie simple, réactive et efficace qui surveille la performance du backtracking puis déclenche une cohérence forte lorsque l’effort du retour sur trace devient alarmant. Enfin, pour la question du « combien », nous surveillons les mises à jour provoquées par la propagation des contraintes et interrompons le processus dès qu’il devient inactif ou coûteux même avant qu’il n’atteigne un point fixe. Les évaluations empiriques sur des problèmes de référence établissent l’efficacité de nos stratégies. / Determining whether or not a Constraint Satisfaction Problem (CSP) has a solution is NP-complete. CSPs are solved by inference (i.e., enforcing consistency), conditioning (i.e., doing search), or, more commonly, by interleaving the two mechanisms. The most common consistency property enforced during search is Generalized Arc Consistency (GAC). In recent years, new algorithms that enforceconsistency properties stronger than GAC have been proposed and shown to be necessary to solve difficult problem instances.We frame the question of balancing the cost and the pruning effectiveness of consistency algorithms as the question of determining where, when, and how much of a higher-level consistency to enforce during search. To answer the ‘where’ question, we exploit the topological structure of a problem instance and target high-level consistency where cycle structures appear. To answer the ‘when’ question, we propose a simple, reactive, and effective strategy that monitors the performance of backtrack search and triggers a higher-level consistency as search thrashes. Lastly, for the question of ‘how much,’ we monitor the amount of updates caused by propagation and interrupt the process before it reaches a fixpoint. Empirical evaluations on benchmark problems demonstrate the effectiveness of our strategies.

Generics has recently been adopted to many mainstream object oriented languages, such as C# and Java. As a particular design choice, generics in C# and Java use a sub-typing relation to constraint type parameters. Failing to encapsulate type parameters within generic interfaces and inability to encapsulate type constraints as part of an interface definition have been identified as deficiencies in the way this design choice has been implemented in these languages. These deficiencies can lead to verbose and redundant code. In particular, they have been reported to affect the development of highly generic libraries. To address these issues, extending object oriented interfaces and sub-typing with associated types and constraint propagation has been proposed and studied in an idealized small-scale formal setting. This thesis builds on this previous work and provides a design and implementation of the extensions in full C#. We also present a proof of soundness of the Featherweight Generic Java (FGJ) formalism extended with interfaces. This property was assumed in a proof of type safety of associated types and constraint propagation, but no proof for the property was provided.

<p>This thesis explores three new techniques for increasing the efficiency of constraint propagation: support for incremental propagation, improved representation of constraints, and abstractions to simplify propagation.  Support for incremental propagation is added to a propagator centered propagation system by adding a new intermediate layer of abstraction, advisors, that capture the essential aspects of a variable centered system. Advisors are used to give propagators a detailed view of the dynamic changes between propagator runs. Advisors enable the implementation of optimal algorithms for important constraints such as extensional constraints and Boolean linear in-equations, which is not possible in a propagator centered system lacking advisors.  Using Multivalued Decision Diagrams (MDD) as the representation for extensional constraints is shown to be useful for several reasons. Classical operations on MDDs can be used to optimize the representation, and thus speeding up the propagation. In particular, the reduction operation is stronger than the use of DFA minimization for the regular constraint. The use of MDDs is contrasted and compared to a recent proposal where tables are compressed.  Abstractions for constraint programs try to capture small and essential features of a model. These features may be much cheaper to propagate than the unabstracted program. The potential for abstraction is explored using several examples. These three techniques work on different levels. Support for incremental propagation is essential for the efficient implementation of some constraints, so that the algorithms have the right complexity. On a higher level, the question of representation looks at what a propagator should use for propagation. Finally, the question of abstraction can potentially look at several propagators, to find cases where abstractions might be fruitful. An essential feature of this thesis is a novel model for general placement constraints that uses regular expressions. The model is very versatile and can be used for several different kinds of placement problems. The model applied to the classic pentominoes puzzle will be used through-out the thesis as an example and for experiments.</p><p> </p> / <p>Den här avhandlingen utforskar tre nya tekniker för att öka effektiviteten av villkorspropagering: stöd för inkrementell propagering, val av representation för villkor, samt abstraktion för att förenkla propagering. Ett propageringssystem organiserat efter propagerare utökas med stöd för inkrementell propagering genom att lägga till ett nytt abstraktionslager: rådgivare. Detta lager fångar de essentiella aspekterna hos system organiserade efter variabler. Rådgivare används för att ge propagerare detaljerad information om de dynamiska ändringarna i variabler mellan körningar av propageraren. Utökningen innebär att det går att implementera optimala algoritmer för vissa viktiga villkor såsom tabellvillkor och Boolska linjära olikheter, något som inte är möjligt i ett rent propagator-organiserat system. Användandet av så kallade <em>Multivalued Decision Diagram</em> (MDD) som representation för tabellvillkor visas vara användbart i flera avseenden. Klassiska MDD-operationer kan användas för att optimera representationen, vilket leder till snabbare propagering. Specifikt så är reduktionsoperationen kraftfullare än användandet av DFA-minimering för reguljära villkor. MDD-representationen jämförs också med ett nyligen framlagt förslag för komprimerade tabeller. Abstraktioner för villkorsprogram försöker fånga små men viktiga egenskaper i modeller. Sådana egenskaper kan vara mycket enklare att propagera än den konkreta modellen. Potentialen för abstraktioner undersöks för några exempel. Dessa tre tekniker fungerar på olika nivåer. Stöd för inkrementell propagering är nödvändigt för att kunna implementera vissa villkor effektivt med rätt komplexitet. Valet av representation för villkor är på en högre nivå, då det gäller att se vilka algoritmer som skall användas för ett villkor. Slutligen så måste flera villkor i en modell studeras för att finna rätt typ av abstraktioner. Ett utmärkande drag för den här avhandlingen är en ny modell för generella placeringsvillkor som använder reguljära uttryck. Modellen är mångsidig och kan användas för flera olika typer av placeringsproblem. Modellen specialiserad för pentominopussel används genomgående som exempel för experiment.</p><p> </p> / Coordinating Constraint Propagation

This thesis explores three new techniques for increasing the efficiency of constraint propagation: support for incremental propagation, improved representation of constraints, and abstractions to simplify propagation.  Support for incremental propagation is added to a propagator centered propagation system by adding a new intermediate layer of abstraction, advisors, that capture the essential aspects of a variable centered system. Advisors are used to give propagators a detailed view of the dynamic changes between propagator runs. Advisors enable the implementation of optimal algorithms for important constraints such as extensional constraints and Boolean linear in-equations, which is not possible in a propagator centered system lacking advisors.  Using Multivalued Decision Diagrams (MDD) as the representation for extensional constraints is shown to be useful for several reasons. Classical operations on MDDs can be used to optimize the representation, and thus speeding up the propagation. In particular, the reduction operation is stronger than the use of DFA minimization for the regular constraint. The use of MDDs is contrasted and compared to a recent proposal where tables are compressed.  Abstractions for constraint programs try to capture small and essential features of a model. These features may be much cheaper to propagate than the unabstracted program. The potential for abstraction is explored using several examples. These three techniques work on different levels. Support for incremental propagation is essential for the efficient implementation of some constraints, so that the algorithms have the right complexity. On a higher level, the question of representation looks at what a propagator should use for propagation. Finally, the question of abstraction can potentially look at several propagators, to find cases where abstractions might be fruitful. An essential feature of this thesis is a novel model for general placement constraints that uses regular expressions. The model is very versatile and can be used for several different kinds of placement problems. The model applied to the classic pentominoes puzzle will be used through-out the thesis as an example and for experiments. / Den här avhandlingen utforskar tre nya tekniker för att öka effektiviteten av villkorspropagering: stöd för inkrementell propagering, val av representation för villkor, samt abstraktion för att förenkla propagering. Ett propageringssystem organiserat efter propagerare utökas med stöd för inkrementell propagering genom att lägga till ett nytt abstraktionslager: rådgivare. Detta lager fångar de essentiella aspekterna hos system organiserade efter variabler. Rådgivare används för att ge propagerare detaljerad information om de dynamiska ändringarna i variabler mellan körningar av propageraren. Utökningen innebär att det går att implementera optimala algoritmer för vissa viktiga villkor såsom tabellvillkor och Boolska linjära olikheter, något som inte är möjligt i ett rent propagator-organiserat system. Användandet av så kallade Multivalued Decision Diagram (MDD) som representation för tabellvillkor visas vara användbart i flera avseenden. Klassiska MDD-operationer kan användas för att optimera representationen, vilket leder till snabbare propagering. Specifikt så är reduktionsoperationen kraftfullare än användandet av DFA-minimering för reguljära villkor. MDD-representationen jämförs också med ett nyligen framlagt förslag för komprimerade tabeller. Abstraktioner för villkorsprogram försöker fånga små men viktiga egenskaper i modeller. Sådana egenskaper kan vara mycket enklare att propagera än den konkreta modellen. Potentialen för abstraktioner undersöks för några exempel. Dessa tre tekniker fungerar på olika nivåer. Stöd för inkrementell propagering är nödvändigt för att kunna implementera vissa villkor effektivt med rätt komplexitet. Valet av representation för villkor är på en högre nivå, då det gäller att se vilka algoritmer som skall användas för ett villkor. Slutligen så måste flera villkor i en modell studeras för att finna rätt typ av abstraktioner. Ett utmärkande drag för den här avhandlingen är en ny modell för generella placeringsvillkor som använder reguljära uttryck. Modellen är mångsidig och kan användas för flera olika typer av placeringsproblem. Modellen specialiserad för pentominopussel används genomgående som exempel för experiment. / QC 20101117 / Coordinating Constraint Propagation

Constraint programming (CP) is a technology in which a combinatorial problem is modeled declaratively as a conjunction of constraints, each of which captures some of the combinatorial substructure of the problem. Constraints are more than a modeling convenience: every constraint is partially implemented by an inference algorithm, called a propagator, that rules out some but not necessarily all infeasible candidate values of one or more unknowns in the scope of the constraint. Interleaving propagation with systematic search leads to a powerful and complete solution method, combining a high degree of re-usability with natural, high-level modeling. A propagator can be characterized as a sound approximation of a constraint on an abstraction of sets of candidate values; propagators that share an abstraction are similar in the strength of the inference they perform when identifying infeasible candidate values. In this thesis, we consider abstractions of sets of candidate values that may be described by an elegant mathematical formalism, the Galois connection. We develop a theoretical framework from the correspondence between Galois connections and propagators, unifying two disparate views of the abstraction-propagation connection, namely the oft-overlooked distinction between representational and computational over-approximations. Our framework yields compact definitions of propagator strength, even in complicated cases (i.e., involving several types, or unknowns with internal structure); it also yields a method for the principled derivation of propagators from constraint definitions. We apply this framework to the extension of an existing CP solver to constraints over strings, that is, words of finite length. We define, via a Galois connection, an over-approximation for bounded-length strings, and demonstrate two different methods for implementing this overapproximation in a CP solver. First we use the Galois connection to derive a bounded-length string representation as an aggregation of existing scalar types; propagators for this representation are obtained by manual derivation, or automated synthesis, or a combination. Then we implement a string variable type, motivating design choices with knowledge gained from the construction of the over-approximation. The resulting CP solver extension not only substantially eases modeling for combinatorial string problems, but also leads to substantial efficiency improvements over prior CP methods.

Relations among various nodes in the circuit, as captured by static and inductive invariants, have shown to have a positive impact on a wide range of EDA applications. Techniques such as boolean constraint propagation for static learning and assume-then-verify approach to reason about inductive invariants have been possible due to efficient SAT solvers. Although a significant amount of research effort has been dedicated to the development of effective invariant learning techniques over the years, the computation time for deriving powerful multi-node invariants is still a bottleneck for large circuits. Fast computation of static and inductive invariants is the primary focus of this thesis. We present a novel technique to reduce the cost of static learning by intelligently identifying redundant computations that may not yield new invariants, thereby achieving significant speedup. The process of inductive invariant reasoning relies on the assume-then-verify framework, which requires multiple iterations to complete, making it infeasible for cases with a large set of multi-node invariants. We present filtering techniques that can be applied to a diverse set of multi-node invariants to achieve a significant boost in performance of the invariant checker. Mining and reasoning about all possible potential multi-node invariants is simply infeasible. To alleviate this problem, strategies that narrow down the focus on specific types of powerful multi-node invariants are also presented. Experimental results reflect the promise of these techniques. As a measure of quality, the invariants are utilized for untestable fault identification and to constrain ATPG for path delay fault testing, with positive results. / Master of Science

The main theme shared by the two main parts of this thesis is EFFICIENT AUTOMATED REASONING.Part I is focussed on a general theory underpinning a number of efficient approximate algorithms for Constraint Satisfaction Problems (CSPs),the constraint propagation algorithms.In Chapter 3, we propose a Structured Generic Algorithm schema (SGI) for these algorithms. This iterates functions according to a certain strategy, i.e. by searching for a common fixpoint of the functions. A simple theory for SGI is developed by studying properties of functions and of the ways these influence the basic strategy. One of the primary objectives of our theorisation is thus the following: using SGI or some of its variations for DESCRIBINING and ANALISYING HOW the "pruning" and "propagation" process is carried through by constraint propagation algorithms.Hence, in Chapter 4, different domains of functions (e.g., domain orderings) are related to different classes of constraint propagation algorithms (e.g., arc consistency algorithms); thus each class of constraint propagation algorithms is associated with a "type" of function domains, and so separated from the others. Then we analys each such class: we distinguished functions on the same domains for their different ways of performing pruning (point or set based), and consequently differentiated between algorithms of the same class (e.g., AC-1 and AC-3 versus AC-4 or AC-5). Besides, we also show how properties of functions (e.g., commutativity or stationarity) are related to different strategies of propagation in constraint algorithms of the same class (see, for instance, AC-1 versus AC-3). In Chapter 5 we apply the SGI schema to the case of soft CSPs (a generalisation of CSPs with sort-of preferences), thereby clarifying some of the similarities and differences between the "classical" and soft constraint-propagation algorithms. Finally, in Chapter 6, we summarise and characterise all the functions used for constraint propagation; in fact, the other goal of our theorisation is abstracting WHICH functions, iterated as in SGI or its variations, perform the task of "pruning" or "propagation" of inconsistencies in constraint propagation algorithms.We focus on relations and relational structures in Part II of the thesis. More specifically, modal languages allow us to talk about various relational structures and their properties. Once the latter are formulated in a modal language, they can be passed to automated theorem provers and tested for satisfiability, with respect to certain modal logics. Our task, in this part, can be described as follows: determining the satisfiability of modal formulas in an efficient manner. In Chapter 8, we focus on one way of doing this: we refine the standard translation as the layered translation, and use existing theorem provers for first-order logic on the output of this refined translation. We provide ample experimental evidence on the improvements in performances that were obtained by means of the refinement.The refinement of the standard translation is based on the tree model property. This property is also used in the basic algorithm schema in Chapter 9 ---the original schema is due to~\cite{seb97}. The proposed algorithm proceeds layer by layer in the modal formula and in its candidate models, applying constraint propagation and satisfaction algorithms for finite CSPs at each layer. With Chapter 9, we wish to draw the attention of constraint programmers to modal logics, and of modal logicians to CSPs.Modal logics themselves express interesting problems in terms of relations and unary predicates, like temporal reasoning tasks. On the other hand, constraint algorithms manipulate relations in the form of constraints, and unary predicates in the form of domains or unary constraints, see Chapter 6. Thus the question of how efficiently those algorithms can be applied to modal reasoning problems seems quite natural and challenging.

Dans cette thèse nous montrons que le raisonnement symbolique associé à la vérification de la consistance d'arc avec propagation de contraintes est un outil efficace pour interpréter les images. Nous montrons dans un premier temps que ce cadre théorique permet de vérifier l'organisation spatiale de différentes composantes d'un objet complexe dans une image. Nous proposons ensuite d'étendre l'utilisation de celui-ci à la reconnaissance sélective des formes décrites par des équations mathématiques, grâce à la notion de consistance d'hyper-arc à deux niveaux de contraintes. La pertinence et la faisabilité de cette approche ont été validées par de multiples tests. En outre, les résultats obtenus sur des images sur-segmentées montrent que la méthode proposée est résistante au bruit, même dans des conditions où les humains (dans certains cas d'agnosie visuelle) peuvent échouer. Ces résultats soutiennent l'intérêt du raisonnement symbolique dans la compréhension de l'image. / In this thesis we show that symbolic reasoning associated with arc consistency checking is an efficient tool for images interpretation. We first show that this theoretical framework makes it possible to verify the spatial organization of different components of a complex object in an image. We then propose to extend the use of this framework to the selective recognition of shapes described by mathematical equations, thanks to the notion of hyper-arc consistency with bi-levels constraint. The relevance and feasibility of this approach have been validated by multiple tests. In addition, the results obtained on over-segmented images show that the proposed method is noise-resistant, even under conditions where humans (in some cases visual agnosia) may fail. These results support the interest of symbolic reasoning in image understanding.

Avec le développement rapide et les applications étendues de la technologie de robot, la recherche sur le robot mobile intelligent a été programmée dans le plan de développement de haute technologie dans beaucoup de pays. La navigation autonome joue un rôle de plus en plus important dans le domaine de recherche du robot mobile intelligent. La localisation et la construction de cartes sont les principaux problèmes à résoudre par le robot pour réaliser une navigation autonome. Les techniques probabilistes (telles que le filtre étendu de Kalman et le filtre de particules) ont longtemps été utilisées pour résoudre le problème de localisation et de cartographie robotisées. Malgré leurs bonnes performances dans les applications pratiques, ils pourraient souffrir du problème d'incohérence dans les scénarios non linéaires, non gaussiens. Cette thèse se concentre sur l'étude des méthodes basées sur l'analyse par intervalles appliquées pour résoudre le problème de localisation et de cartographie robotisées. Au lieu de faire des hypothèses sur la distribution de probabilité, tous les bruits de capteurs sont supposés être bornés dans des limites connues. Sur la base d'une telle base, cette thèse formule le problème de localisation et de cartographie dans le cadre du problème de satisfaction de contraintes d'intervalle et applique des techniques d'intervalles cohérentes pour les résoudre de manière garantie. Pour traiter le problème du "lacet non corrigé" rencontré par les approches de localisation par ICP (Interval Constraint Propagation), cette thèse propose un nouvel algorithme ICP traitant de la localisation en temps réel du véhicule. L'algorithme proposé utilise un algorithme de cohérence de bas niveau et est capable de diriger la correction d'incertitude. Par la suite, la thèse présente un algorithme SLAM basé sur l'analyse d'intervalle (IA-SLAM) dédié à la caméra monoculaire. Une paramétrisation d'erreur liée et une initialisation non retardée pour un point de repère naturel sont proposées. Le problème SLAM est formé comme ICSP et résolu par des techniques de propagation par contrainte d'intervalle. Une méthode de rasage pour la contraction de l'incertitude historique et une méthode d'optimisation basée sur un graphique ICSP sont proposées pour améliorer le résultat obtenu. L'analyse théorique de la cohérence de la cartographie est également fournie pour illustrer la force de IA-SLAM. De plus, sur la base de l'algorithme IA-SLAM proposé, la thèse présente une approche cohérente et peu coûteuse pour la localisation de véhicules en extérieur. Il fonctionne dans un cadre en deux étapes (enseignement visuel et répétition) et est validé avec un véhicule de type voiture équipé de capteurs de navigation à l'estime et d'une caméra monoculaire. / With the rapid development and extensive applications of robot technology, the research on intelligent mobile robot has been scheduled in high technology development plan in many countries. Autonomous navigation plays a more and more important role in the research field of intelligent mobile robot. Localization and map building are the core problems to be solved by the robot to realize autonomous navigation. Probabilistic techniques (such as Extented Kalman Filter and Particle Filter) have long been used to solve the robotic localization and mapping problem. Despite their good performance in practical applications, they could suffer the inconsistency problem in the non linear, non Gaussian scenarios. This thesis focus on study the interval analysis based methods applied to solve the robotic localization and mapping problem. Instead of making hypothesis on the probability distribution, all the sensor noises are assumed to be bounded within known limits. Based on such foundation, this thesis formulates the localization and mapping problem in the framework of Interval Constraint Satisfaction Problem and applied consistent interval techniques to solve them in a guaranteed way. To deal with the “uncorrected yaw” problem encountered by Interval Constraint Propagation (ICP) based localization approaches, this thesis proposes a new ICP algorithm dealing with the real-time vehicle localization. The proposed algorithm employs a low-level consistency algorithm and is capable of heading uncertainty correction. Afterwards, the thesis presents an interval analysis based SLAM algorithm (IA-SLAM) dedicates for monocular camera. Bound-error parameterization and undelayed initialization for nature landmark are proposed. The SLAM problem is formed as ICSP and solved via interval constraint propagation techniques. A shaving method for landmark uncertainty contraction and an ICSP graph based optimization method are put forward to improve the obtaining result. Theoretical analysis of mapping consistency is also provided to illustrated the strength of IA-SLAM. Moreover, based on the proposed IA-SLAM algorithm, the thesis presents a low cost and consistent approach for outdoor vehicle localization. It works in a two-stage framework (visual teach and repeat) and is validated with a car-like vehicle equipped with dead reckoning sensors and monocular camera.