Several explanation and interpretation tasks, such as diagnosis, plan recognition and image interpretation, can be formalized as abductive and consistency reasoning. The interpretation task is usually executed for the purpose of performing actions, e.g., in diagnosis, repair actions or therapy. In some cases actions are the only or the main way for discriminating among alternative explanations. Some proposals address the problem based on a task-independent representation of a domain which includes an ontology or taxonomy of hypotheses and actions. In this paper we rely on the same type of representation, and we point out the role of abstractions in an iterative process where, like in model-based diagnosis and troubleshooting, further observations or actions are proposed to achieve the overall goal of discriminating among candidate hypotheses and, more importantly, performing the appropriate actions for the case at hand. Discrimination is performed up to an appropriate level which depends on the cost of actions (e.g. repair actions or therapy) to be taken based on the results of abduction, and on the cost of additional observations, which should be balanced with the benefits, in terms of more suitable actions, of better discrimination. Abstractions have a significant impact on this trade-off, given that the cost of observing the same phenomenon at different levels of abstraction may be quite different, and choosing a generic action, without information on which specific instance is most appropriate, is, in general, suboptimal.

State abstraction has been widely used for state aggregation in approaches to AI search and planning. In this paper we use a powerful abstraction technique from software model checking for representing collections of states with different object quantities and properties. We exploit this method to develop precise abstractions and action operators for use in AI. This enables us to find scalable, algorithm-like plans with branches and loops which can solve problems of unbounded sizes. We describe how this method of abstraction can be effectively used in AI, with compelling results from implementations of two planning algorithms.

We present algorithms for testing the satisfiability and finding the tightened transitive closure of conjunctions of addition constraints of the form ± x ± y ≤ d and bound constraints of the form ± x ≤ d where x and y are integer variables and d is an integer constrant. The running time of these algorithms is a cubic polynomial in the number of input constraints. We also describe an efficient matrix representation of addition and bound constraints. The matrix representation provides a easy, algebraic implementation of the satisfiability and tightened transitive closure algorithms. We also outline the use of these algorithms for the improved implementation of abstract interpretation methods based on the octagonal abstract domain.

Constraint Programming is an attractive approach for solving AI planning problems by modelling them as Constraint Satisfaction Problems (CSPs). However, formulating effective constraint models of complex planning problems is challenging,  and CSPs resulting from standard approaches often require further enhancement to perform well. Common subexpression elimination is a computationally cheap and  general technique for improving CSPs, which can lead to a great reduction in instance size, solving time and search space. In this work we identify general causes of common subexpressions from three modelling techniques often used to encode planning problems into   constraints. We present four case studies of constraint  models of AI planning problems. In each, we describe the constraint model, highlight the sources of common subexpressions, and present an empirical analysis of the effects of eliminating common subexpressions.

Tailoring solver-independent constraint instances to target solvers is an important component of automated constraint modelling. We augment the tailoring process by a set of enhancement techniques of which many are successfully established in related fields, such as common subexpression elimination. Our aim is to apply these techniques in an efficient fashion,  since we tailor instance-wise, and not whole problem classes. We integrate automated enhancement into the tailoring procedure, which creates a novel setup with great potential, as our empirical analysis confirms: impressive speedups, additional propagation and instance  reduction, all for investing little computational effort.

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.

Real-world automated reasoning systems must contend with inconsistencies and the vast amount of information stored in relational databases.  In this paper, we introduce compilation techniques for inconsistency-tolerant reasoning over the combination of classical logic and a relational database.  Our resolution-based algorithms address a quantifier-free, function-free fragment of first-order logic while leveraging off-the-shelf database technology for all data-intensive computation.

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.

Equidistant Frequency Permutation Arrays are combinatorial objects of interest in coding theory. A frequency permutation array is a type of constant composition code in which each symbol occurs the same number of times in each codeword. The problem is to find a set of codewords such that any pair of codewords are a given uniform Hamming distance apart. The equidistant case is of special interest given the result that any optimal constant composition code is equidistant. This paper presents, compares and combines a number of different constraint formulations of this problem class, including a new method of representing permutations with constraints. Using these constraint models, we are able to establish several new results, which are contributing directly to mathematical research in this area.