Mapping Inferences: Constraint Propagation and Diamond Satisfaction

Abstract

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.