发表机构
Eindhoven University of Technology（埃因霍温理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对现有本原蕴含项计算方法因指数级数量导致可扩展性差的问题，提出基于决策图的端到端符号算法，实现受侧约束的本原蕴含项的隐式计算。
AI 中文摘要
本原蕴含项（Prime Implicants，PIs）在计算机科学中处于核心地位，应用于逻辑极小化、诊断、可解释形式化方法及人工智能等领域。计算PIs的算法最初主要针对完整输入空间设计，未考虑输入空间可能受上下文或结构依赖约束的情况。为剔除不满足约束的PIs，现有方法依赖于计算所有PIs后的显式后处理步骤，由于PIs的数量呈指数级增长，这导致了可扩展性问题。我们提出端到端的符号算法，该算法隐式表示受侧约束的PIs集合。为此，我们扩展了基于决策图的知名Coudert-Madre方法，并实现了模块化工具链，将决策图构建、PI计算和过滤分离。
英文摘要
Prime implicants (PIs) are central in computer science, with applications in logic minimization, diagnosis, explainable formal methods and AI. Algorithms for the computation of PIs were first-and-foremost considered on the full input space, not considering the case where the input space might be constrained by context or structural dependencies. To filter out those PIs that do not fulfill the constraints, existing methods rely on an explicit post-processing step after computing all PIs, which leads to scalability issues due to the number of PIs being exponential. We propose end-to-end symbolic algorithms that implicitly represent the set of PIs under side constraints. For this, we extend the prominent method based on decision diagrams by Coudert and Madre and implement a modular tool chain that separates decision-diagram construction, PI computation, and filtering.
