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

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

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

Zero-One Designs Produce Small Hard SAT Instances

Some basics of combinatorial block design are combined with certain constraint satisfaction problems of interest to the satisfiability community. The paper shows how such combinations lead to satisfiability problems, and shows empirically that these are some of the smallest very hard satisfiability problems ever constructed. Partially balanced (0,1) designs (PB01Ds) are introduced as an extension of balanced incomplete block designs (BIBDs) and (0,1) designs. Also, (0,1) difference sets are introduced as an extension of certain cyclical difference sets. Constructions based on (0,1) difference sets enable generation of PB01Ds over a much wider range of parameters than is possible for BIBDs. Building upon previous work of Spence, it is shown how PB01Ds lead to small, very hard, unsatisfiable formulas. A new three-dimensional form of combinatorial block design is introduced, and leads to small, very hard, satisfiable formulas. The methods are validated on solvers that performed well in the SAT 2009 and earlier competitions.

Complexité des homomorphismes de graphes avec listes

Les problèmes de satisfaction de contraintes, qui consistent à attribuer des valeurs à des variables en respectant un ensemble de contraintes, constituent une large classe de problèmes naturels. Pour étudier la complexité de ces problèmes, il est commode de les voir comme des problèmes d'homomorphismes vers des structures relationnelles. Un axe de recherche actuel est la caractérisation des classes de complexité auxquelles appartient le problème d'homomorphisme, ceci dans la perspective de confirmer des conjectures reliant les propriétés algébriques des structures relationelles à la complexité du problème d'homomorphisme. Cette thèse propose dans un premier temps la caractérisation des digraphes pour lesquels le problème d'homomorphisme avec listes appartient à FO. On montre également que dans le cas du problèmes d'homomorphisme avec listes sur les digraphes télescopiques, les conjectures reliant algèbre et complexité sont confirmées. Dans un deuxième temps, on caractérise les graphes pour lesquels le problème d'homomorphisme avec listes est résoluble par cohérence d'arc. On introduit la notion de polymorphisme monochromatique et on propose un algorithme simple qui résoud le problème d'homomorphisme avec listes si le graphe cible admet un polymorphisme monochromatique TSI d'arité k pour tout k ≥ 2.

Safe Distributed Coordination of Heterogeneous Robots through Dynamic Simple Temporal Networks

Research on autonomous intelligent systems has focused on how robots can robustly carry out missions in uncertain and harsh environments with very little or no human intervention. Robotic execution languages such as RAPs, ESL, and TDL improve robustness by managing functionally redundant procedures for achieving goals. The model-based programming approach extends this by guaranteeing correctness of execution through pre-planning of non-deterministic timed threads of activities. Executing model-based programs effectively on distributed autonomous platforms requires distributing this pre-planning process. This thesis presents a distributed planner for modelbased programs whose planning and execution is distributed among agents with widely varying levels of processor power and memory resources. We make two key contributions. First, we reformulate a model-based program, which describes cooperative activities, into a hierarchical dynamic simple temporal network. This enables efficient distributed coordination of robots and supports deployment on heterogeneous robots. Second, we introduce a distributed temporal planner, called DTP, which solves hierarchical dynamic simple temporal networks with the assistance of the distributed Bellman-Ford shortest path algorithm. The implementation of DTP has been demonstrated successfully on a wide range of randomly generated examples and on a pursuer-evader challenge problem in simulation.

Robust fault detection using consistency techniques for uncertainty handling

Often practical performance of analytical redundancy for fault detection and diagnosis is decreased by uncertainties prevailing not only in the system model, but also in the measurements. In this paper, the problem of fault detection is stated as a constraint satisfaction problem over continuous domains with a big number of variables and constraints. This problem can be solved using modal interval analysis and consistency techniques. Consistency techniques are then shown to be particularly efficient to check the consistency of the analytical redundancy relations (ARRs), dealing with uncertain measurements and parameters. Through the work presented in this paper, it can be observed that consistency techniques can be used to increase the performance of a robust fault detection tool, which is based on interval arithmetic. The proposed method is illustrated using a nonlinear dynamic model of a hydraulic system

Fault diagnosis by refining the parameter uncertainty space of nonlinear dynamic systems

This paper deals with fault detection and isolation problems for nonlinear dynamic systems. Both problems are stated as constraint satisfaction problems (CSP) and solved using consistency techniques. The main contribution is the isolation method based on consistency techniques and uncertainty space refining of interval parameters. The major advantage of this method is that the isolation speed is fast even taking into account uncertainty in parameters, measurements, and model errors. Interval calculations bring independence from the assumption of monotony considered by several approaches for fault isolation which are based on observers. An application to a well known alcoholic fermentation process model is presented

A proposal for the diagnosis of uncertain dynamic systems based on interval models

The performance of a model-based diagnosis system could be affected by several uncertainty sources, such as,model errors,uncertainty in measurements, and disturbances. This uncertainty can be handled by mean of interval models.The aim of this thesis is to propose a methodology for fault detection, isolation and identification based on interval models. The methodology includes some algorithms to obtain in an automatic way the symbolic expression of the residual generators enhancing the structural isolability of the faults, in order to design the fault detection tests. These algorithms are based on the structural model of the system. The stages of fault detection, isolation, and identification are stated as constraint satisfaction problems in continuous domains and solved by means of interval based consistency techniques. The qualitative fault isolation is enhanced by a reasoning in which the signs of the symptoms are derived from analytical redundancy relations or bond graph models of the system. An initial and empirical analysis regarding the differences between interval-based and statistical-based techniques is presented in this thesis. The performance and efficiency of the contributions are illustrated through several application examples, covering different levels of complexity.

Ever decreasing circles: speech production in semantic dementia

We explored the impact of a degraded semantic system on lexical, morphological and syntactic complexity in language production. We analysed transcripts from connected speech samples from eight patients with semantic dementia (SD) and eight age-matched healthy speakers. The frequency distributions of nouns and verbs were compared for hand-scored data and data extracted using text-analysis software. Lexical measures showed the predicted pattern for nouns and verbs in hand-scored data, and for nouns in software-extracted data, with fewer low frequency items in the speech of the patients relative to controls. The distribution of complex morpho-syntactic forms for the SD group showed a reduced range, with fewer constructions that required multiple auxiliaries and inflections. Finally, the distribution of syntactic constructions also differed between groups, with a pattern that reflects the patients’ characteristic anomia and constraints on morpho-syntactic complexity. The data are in line with previous findings of an absence of gross syntactic errors or violations in SD speech. Alterations in the distributions of morphology and syntax, however, support constraint satisfaction models of speech production in which there is no hard boundary between lexical retrieval and grammatical encoding.

Automating the creation of 3D animation from annotated fiction text

This paper describes a strategy for automatically converting fiction text into 3D animations. It assumes the existence of fiction text annotated with avatar, object, setting, transition and relation annotations, and presents a transformation process that converts annotated text into quantified constraint systems, the solutions to which are used in the population of 3D environments. Constraint solutions are valid over temporal intervals, ensuring that consistent dynamic behaviour is produced. A substantial level of automation is achieved, while providing opportunities for creative manual intervention in animation process. The process is demonstrated using annotated examples drawn from popular fiction text that are converted into animation sequences, confirming that the desired results can be achieved with only high-level human direction.

A method for automatically creating 3D animated scenes from annotated fiction text

This paper describes a strategy for automatically converting fiction text into 3D animations. It assumes the existence of fiction text annotated with avatar, object, setting, transition and relation annotations, and presents a transformation process that converts annotated text into quantified constraint systems, the solutions to which are used in the population of 3D environments. Constraint solutions are valid over temporal intervals, ensuring that consistent dynamic behaviour is produced. A substantial level of automation is achieved, while providing opportunities for creative manual intervention in animation process. The process is demonstrated using annotated examples drawn from popular fiction text that are converted into animation sequences, confirming that the desired results can be achieved with only highlevel human direction.

A novel semi-supervised approach for network traffic clustering

Network traffic classification is an essential component for network management and security systems. To address the limitations of traditional port-based and payload-based methods, recent studies have been focusing on alternative approaches. One promising direction is applying machine learning techniques to classify traffic flows based on packet and flow level statistics. In particular, previous papers have illustrated that clustering can achieve high accuracy and discover unknown application classes. In this work, we present a novel semi-supervised learning method using constrained clustering algorithms. The motivation is that in network domain a lot of background information is available in addition to the data instances themselves. For example, we might know that flow ƒ1 and ƒ2 are using the same application protocol because they are visiting the same host address at the same port simultaneously. In this case, ƒ1 and ƒ2 shall be grouped into the same cluster ideally. Therefore, we describe these correlations in the form of pair-wise must-link constraints and incorporate them in the process of clustering. We have applied three constrained variants of the K-Means algorithm, which perform hard or soft constraint satisfaction and metric learning from constraints. A number of real-world traffic traces have been used to show the availability of constraints and to test the proposed approach. The experimental results indicate that by incorporating constraints in the course of clustering, the overall accuracy and cluster purity can be significantly improved.

Uma investigação de algoritmos exatos e metaheurísticos aplicados ao nonograma

Nonogram is a logical puzzle whose associated decision problem is NP-complete. It has applications in pattern recognition problems and data compression, among others. The puzzle consists in determining an assignment of colors to pixels distributed in a N  M matrix that satisfies line and column constraints. A Nonogram is encoded by a vector whose elements specify the number of pixels in each row and column of a figure without specifying their coordinates. This work presents exact and heuristic approaches to solve Nonograms. The depth first search was one of the chosen exact approaches because it is a typical example of brute search algorithm that is easy to implement. Another implemented exact approach was based on the Las Vegas algorithm, so that we intend to investigate whether the randomness introduce by the Las Vegas-based algorithm would be an advantage over the depth first search. The Nonogram is also transformed into a Constraint Satisfaction Problem. Three heuristics approaches are proposed: a Tabu Search and two memetic algorithms. A new function to calculate the objective function is proposed. The approaches are applied on 234 instances, the size of the instances ranging from 5 x 5 to 100 x 100 size, and including logical and random Nonograms

Markov Constraints for Generating Texts with Style

This thesis addresses the issue of generating texts in the style of an existing author, that also satisfy structural constraints imposed by the genre of the text. Although Markov processes are known to be suitable for representing style, they are difficult to control in order to satisfy non-local properties, such as structural constraints, that require long distance modeling. The framework of Constrained Markov Processes allows to precisely generate texts that are consistent with a corpus, while being controllable in terms of rhymes and meter. Controlled Markov processes consist in reformulating Markov processes in the context of constraint satisfaction. The thesis describes how to represent stylistic and structural properties in terms of constraints in this framework and how this approach can be used for the generation of lyrics in the style of 60 differents authors An evaluation of the desctibed method is provided by comparing it to both pure Markov and pure constraint-based approaches. Finally the thesis describes the implementation of an augmented text editor, called Perec. Perec is intended to improve creativity, by helping the user to write lyrics and poetry, exploiting the techniques presented so far.