We consider the problem EnumIP of enumerating prime implicants of Boolean functions represented by decision decomposable negation normal form (dec-DNNF) circuits. We study EnumIP from dec-DNNF within the framework of enumeration complexity and prove that it is in OutputP, the class of output polynomial enumeration problems, and more precisely in IncP, the class of polynomial incremental time enumeration problems. We then focus on two closely related, but seemingly harder, enumeration problems where further restrictions are put on the prime implicants to be generated. In the first problem, one is only interested in prime implicants representing subset-minimal abductive explanations, a notion much investigated in AI for more than three decades. In the second problem, the target is prime implicants representing sufficient reasons, a recent yet important notion in the emerging field of eXplainable AI, since they aim to explain predictions achieved by machine learning classifiers. We provide evidence showing that enumerating specific prime implicants corresponding to subset-minimal abductive explanations or to sufficient reasons is not in OutputP.
翻译:我们研究了由决策可分解否定范式(dec-DNNF)电路表示的布尔函数的素隐含项枚举问题EnumIP。在枚举复杂性框架下,我们从dec-DNNF角度研究了EnumIP问题,并证明它属于输出多项式枚举问题类OutputP,更确切地说属于多项式增量时间枚举问题类IncP。接着,我们关注两个密切相关但表面上更困难的枚举问题,这两个问题对要生成的素隐含项施加了进一步限制。第一个问题仅关注表示子集极小溯因解释的素隐含项,这一概念在人工智能领域已被深入研究三十余年。第二个问题的目标是表示充分理由的素隐含项,这是可解释人工智能新兴领域中一个近期但重要的概念,因为它们旨在解释机器学习分类器做出的预测。我们提供了证据表明,枚举对应于子集极小溯因解释或充分理由的特定素隐含项不属于OutputP类。