The study of reasoning problems is a very active area in Artificial Intelligence. The majority of such problems are computationally involved as they are often situated at the second level of the polynomial hierarchy when considered in full propositional logic. Identifying fragments of propositional
logic in which these problems are easier to solve has become one of the recent challenges in the knowledge representation research area. Many of these problems bring into play minimality conditions, therefore it turns out that understanding the complexity of the following satis ability problem is crucial:
CardMinSat: Given a propositional formula Phi and an atom x, is x true in a cardinality-minimal model of Phi ?
We aim at classifying the complexity of this problem in fragments of propositional logic. Universal algebra establishing a Galois connection between the lattice of Boolean relations (co-clones) and the lattice of Boolean functions (clones) is nowadays recognized as a very powerful tool in order to get complexity classifcations of satisfiability related problems. Nevertheless the minimality condition arising here makes this classical connection inappropriate. We have to investigate a finer lattice, namely the one of frozen partial co-clones. In doing so we hope to be able to better understand the complexity of CardMinSat in fragments of propositional logic. This would be a cornerstone in order to embark on a systematic study of the complexity of many reasoning problems within fragments of propositional logic.