This project pivots around the satisfiability problem for logical languages including propositional logic (SAT), constraint satisfaction problems (CSP), and the fuzzy extension of description logics (FDL). Our purpose is to advance in each of the three areas using the synergy between the four groups that was initiated by previous joint projects. The concrete goals of the proposal are the following.

In SAT we want to study the structure of instances arising in industry, and apply this knowledge to develop more efficient solvers, both for SAT and for MaxSAT. In CSP we want to contribute to the problem of classification of tractable constraint languages. We will also study algorithms for geometric instances of MaxCSP and random instances for SAT of interest in computational complexity theory. In FDL we will study the expressive power and the complexity of the fragments of first-order fuzzy logic that correspond to description logics, and algorithms for satisfiability with special attention to the case of finitely valued FDLs.