Constraint technology offers advantages over traditional Operations Research methods to solve optimisation tasks. However, the CSP model presents some limitations because all constraints are mandatory. In real problems, constraints are often preferences, but if included in the CSP model an over-constrasined problem is produced. Then, the only option is to relax / remove some of the preference constraints by hand, but it is difficult to assure teh solution quality and this is not commercially satisfactory.

In the last years, several theoretical models as well as algorithms have been developed to represent and solve CSP with preferences. They have been produced in an academic context, but they are not fully available to industry. This project aims to bridge the gap between academic results and industrial needs. Specifically, the goal of ECSPLAIN is to develop methods, techniques and generic software, making it possible to address such problems in a systematic manner, thus insuring quality solutions to complex, constrained optimisation tasks. More specifically, the project focuses on the resolution of over-constrained problems and of problems involving multiple optimisation criteria and/or a wide variety of preference constraints.

The current project is focused on propositional logic as a foundation for computer science. We will study classical logic, as well as multivalued logic, looking at the foundation of multivalued logic based on t-norms, and the proof theory of both logics. Moreover, we will apply this knowledge to automated deduction, hardware verification and implementation of heuristics for computationally hard problems. The topics will be:

1. logic and algebraic foundation of multivalued logic;
2. applications to this logics to the study of approximate reasoning for further creation of intelligent systems;
3. study of classical deduction systems from the point of view of computational complexity;
4. extension to multivalued logic of the results obtained in classical proof theory;
5. theoretical foundation of automated deduction;
6. algorithms and implementations of classical SAT and signed SAT (multivalued), as well as implementations of proof systems.