用SAT求解器实现ALC逻辑公式的有界拟合，兼具理论保证与高效计算。
SAT-Based Bounded Fitting for the Description Logic ALC
- 将有界拟合问题转化为SAT实例，利用求解器高效求解
- 证明所有语法片段的拟合问题是NP完全，即使仅一对正负例也难
- 相比其他算法，本方法在概率可学习框架下有理论保障
有界拟合是一种从正负数据样本中学习逻辑公式的通用范式，近年来受到广泛关注。本文研究描述逻辑ALC及其语法片段的有界拟合问题。我们证明，所有研究片段的受限大小拟合问题是NP完全的，甚至在仅有一对正负例的情况下也是如此。有界拟合天然具备瓦利安特（Valiant）PAC学习框架下的概率保证，而其他ALC概念学习算法则不具备此类保证。最后，我们基于SAT求解器实现了ALC及其片段的有界拟合方法，讨论了优化策略，并与其它概念学习工具进行了对比。
原文摘要 · Abstract (English)
Bounded fitting is a general paradigm for learning logical formulas from positive and negative data examples, that has received considerable interest recently. We investigate bounded fitting for the description logic ALC and its syntactic fragments. We show that the underlying size-restricted fitting problem is NP-complete for all studied fragments, even in the special case of a single positive and a single negative example. By design, bounded fitting comes with probabilistic guarantees in Valiant's PAC learning framework. In contrast, we show that other classes of algorithms for learning ALC concepts do not provide such guarantees. Finally, we present an implementation of bounded fitting in ALC and its fragments based on a SAT solver. We discuss optimizations and compare our implementation to other concept learning tools.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。