In this paper, we propose a new approach for solving the SAT problem. This approach consists in representing SAT instances thanks to an undirected graph issued from a polynomial transformation from SAT to the CLIQUE problem. Considering this graph, we exploit well known properties of chordal graphs to manipulate the SAT instance. Firstly, these properties allow us to define a new class of SAT polynomial instances. Moreover, they allow us to rewrite SAT instances in disjunctions of smaller instances which could be significantly easier to solve.

Complete row and column symmetry breaking in constraint satisfaction problems using the lex leader method is generally prohibitively costly. Double lex, which is derived from lex leader, is commonly used in practice as an incomplete symmetry-breaking method for row and column symmetries. This technique uses a row-wise ordering to construct the lex leader. For this reason, it is generally counterproductive to choose a search ordering that is not also row-wise. It seems logical that the search order should be used to pick the symmetry breaking technique, rather than the other way around. This paper surveys other possible orderings and investigates one particular ordering, snake ordering. From this we derive a corresponding incomplete set of symmetry breaking constraints, snake lex. We present experimental data comparing double lex and the snake lex, showing that snake lex is substantially faster than double lex in many cases.

The lex leader method for breaking symmetry in CSPs typically produces a large set of lexicographic ordering constraints. Several rules have been proposed to reduce such sets whilst preserving logical equivalence. These reduction rules are not generally confuent: they may reach more than one xpoint, depending on the order of application. These fixpoints vary in size. Smaller sets of lex constraints are desirable so ensuring reduction to a global minimum is essential. We characterise the systems of constraints for which the reduction rules are confluent in terms of a simple feature of the input, and define an algorithm to determine whether a set of lex constraints reduce confuently.

Given a system design (SD), a key task is to optimize this design to reduce the probability of catastrophic failures. We consider the task of redesigning an SD to minimize the probability of particular faults by introducing components selected from a component library. We have implemented a General Redesign Engine (GRE), which uses model-based reasoning techniques and Boolean functional synthesis from component libraries, to automate redesign for combinational circuits. For a significant subset of observations leading to catastrophic (forbidden) modes we demonstrate that GRE trades off redesign cost for increased fault tolerance, and shows a significant advantage compared to the Triple-Modular Redundancy (TMR) method. Our algorithm has a wide application in AI, including automated software and hardware design, error detection, reconfiguration and recovery, and modular robotics.

In a constraint satisfaction problem, the tightness of an individual constraint only describes the influence that the variables within its scope have on one another. Clusters provide a broader view; they are dense, tight subproblems within a problem. A set of clusters for a problem and the links between them provide an abstraction of it. That abstraction can be used to guide search, to curtail inference, and to provide explanations to the user. This work is a hybrid of global and local search, where local search creates an abstraction and then global search exploits it. Heuristics reference clusters to order variables and to propagate more thoughtfully with respect to them. Results are provided on a variety of challenging benchmark problems.

Despite a big progress in solving planning problems, more complex problems still remain hard and challenging for existing planners. One of the most promising research directions is exploiting knowledge engineering techniques such as (re)formulating the planning problem to be easier to solve for existing planners. In particular, it is possible to automatically gather knowledge from toy planning problems and exploit this knowledge when solving more complex planning problems. In this paper we propose a method for eliminating some actions from the problem specification that are often useless or may mislead the planners. The method detects if actions are somehow connected with the initial or goal predicates and by using this information we suggest that some actions are not necessary when solving the planning problem. To eliminate these actions we modify the planning domain and hence the method remains independent of used planning system.

An important challenge in constraint programming is to rewrite constraint models into executable programs calculating the solutions. This phase of constraint processing may require translations between constraint programming languages, transformations of constraint representations, model optimizations, and tuning of solving strategies. In this paper, we introduce a pivot metamodel describing the common features of constraint models including different kinds of constraints, statements like conditionals and loops, and other first-class elements like object classes and predicates. This metamodel is general enough to cope with the constructions of many languages, from object-oriented modeling languages to logic languages, but it is independent from them. The rewriting operations manipulate metamodel instances apart from languages. As a consequence, the rewriting operations apply whatever languages are selected and they are able to manage model semantic information. A bridge is created between the metamodel space and languages using parsing techniques. Tools from the software engineering world can be useful to implement this framework.

Classical planning deals with finding a (shortest) sequence of actions transferring the world from its initial state to a state satisfying the goal condition. Traditional planning systems explore either paths in the state space (state-space planning) or partial plans (plan-space planning). In this paper we show how the ideas from plan-space (partial order) planning can be integrated into state-space (sequential) planning by combining constraint models describing both types of planning. In particular, we extend our existing constraint model for sequential planning by constraints describing satisfaction of open goals. We demonstrate experimentally that this extension pays-off especially when the planning problems become harder.

Generating minimal hitting sets of a collection of sets is known to be NP-hard, necessitating heuristic approaches to handle large problems. In this paper a low-cost, approximate minimal hitting set (MHS) algorithm, coined Staccato, is presented. Staccato uses a heuristic function, borrowed from a lightweight, statistics-based software fault localization approach, to guide the MHS search. Given the nature of the heuristic function, Staccato is specially tailored to model-based diagnosis problems (where each MHS solution is a diagnosis to the problem), although well-suited for other application domains as well. We apply Staccato in the context of model-based diagnosis and show that even for small problems our approach is orders of magnitude faster than the brute-force approach, while still capturing all important solutions. Furthermore, due to its low cost complexity, we also show that Staccato is amenable to large problems including millions of variables.

Current research on qualitative spatial representation and reasoning mainly focuses on one single aspect of space. In real world applications, however, multiple spatial aspects are often involved simultaneously. This paper investigates problems arising in reasoning with combined topological and directional information. We use the RCC8 algebra and the Rectangle Algebra (RA) for expressing topological and directional information respectively. We give examples to show that the bipath-consistency algorithm BIPATH is incomplete for solving even basic RCC8 and RA constraints. If topological constraints are taken from some maximal tractable subclasses of RCC8, and directional constraints are taken from a subalgebra, termed DIR49, of RA, then we show that BIPATH is able to separate topological constraints from directional ones. This means, given a set of hybrid topological and directional constraints from the above subclasses of RCC8 and RA, we can transfer the joint satisfaction problem in polynomial time to two independent satisfaction problems in RCC8 and RA. For general RA constraints, we give a method to compute solutions that satisfy all topological constraints and approximately satisfy each RA constraint to any prescribed precision.