- Quant a IIIA
This project aims at advancing the state-of-the-art in several aspects of fuzzy logic, argumentation with uncertainty and preferences, new techniques for SAT/MaxSAT and distributed solving, and in their application to solve two real problems: the analysis of discussions in social networks to determine which are the most relevant opinions, and the control of energy resources in energy grids with decision strategies optimizing the selection and use of the most appropriate available energy resource at every time, trying to balance the economical and environmental impacts. These two problems, although different, are examples of complex problems that our society has to face today that require advanced techniques of reasoning, preference modelling, and optimization tasks to be successfully solved. To this end, in this project we aim at addressing the following objectives.
First, to develop an uniform, fuzzy logic-based logical framework integrating reasoning, argumentation and decision making models able to cope with vague and uncertain knowledge, as well as mechanisms to handle inconsistent information. To this end, we will study extensions of t-norm based logics with multiple modalities, each one accounting for an intensional notion like uncertainty, preference, trust or approximation. Argumentation
mechanisms accommodating uncertain and trust information will be also studied, in particular a probabilistic extension of the DeLP framework will be investigated.
Second, to extend current SAT, MaxSAT or SMT-based techniques for solving different reasoning and optimization tasks over that framework, and needed for our application problems. In particular, in the classical setting, we will pay attention to improving techniques to solve SAT/MaxSAT problems in a distributed way. Indeed, we want to study how graph layout algorithms could be used to model the intrinsic structure or topology of industrial (or real problem) SAT instances, and then to explicitly exploit it, specially the modularity property, in specialized SAT solvers. As for MaxSAT and MinSAT, our objective is to investigate and implement inference-based solvers and empirically compare them with state- of-the-art solvers. In the finitely-valued setting, the goal is to extend successful MaxSAT and MinSAT solving techniques to the framework of signed CNF formulas, whereas in the infinitely-valued setting we plan to make use of SMT solvers.
Third, to use the above real problems as testbeds to check the applicability of our models and solving tools, and to study their strengths and weaknesses. For the analysis of discussions in social networks, we want to develop argumentation models, on top of our fuzzy logic-based framework, such that opinions and relations between them can be modelled with a rich set of features and then analized with our reasoning algorithms. For dynamic and big size discussions, we want to check the suitability of distributed versions of our algorithms. For solving problems about control of energy resources, we want to develop models that use the characteristics of our logic framework that allow to model uncertainty, for the behaviour of energy resources, and user preferences, for considering the integration of multiple competing objectives. We plan to integrate this novel modelling approach within the general framework of reinforcement learning algorithms.