Many AI-related reasoning problems are based on the problem of satisfiability of propositional formulas with some cardinality-minimality condition. While the complexity of the satisfiability problem (SAT) is well understood when considering systematically all fragments of propositional logic within Schaefer's framework (STOC 1978) this is not the case when such minimality condition is added. We consider the CardMinSat problem, which asks, given a formula F and an atom x, whether x is true in some cardinality-minimal model of F. We completely classify the computational complexity of the CardMinSat problem within Schaefer's framework, thus paving the way for a better understanding of the tractability frontier of many AI-related reasoning problems. To this end we use advanced algebraic tools developed by (Schnoor & Schnoor 2008) and (Lagerkvist 2014).

翻译：许多与人工智能相关的推理问题都基于带有某种基数极小化条件的命题公式可满足性问题。虽然在使用Schaefer框架（STOC 1978）系统考虑命题逻辑所有片段时，可满足性问题（SAT）的复杂性已得到充分理解，但当添加这种极小化条件时，情况并非如此。我们考虑CardMinSat问题，即给定公式F和原子x，判断x是否存在于F的某个基数极小模型中的真值。我们在Schaefer框架内完全分类了CardMinSat问题的计算复杂性，从而为更好地理解许多与AI相关推理问题的易解性边界铺平了道路。为此，我们使用了(Schnoor & Schnoor 2008)和(Lagerkvist 2014)开发的先进代数工具。