SAT-Based Bounded Fitting for the Description Logic ALC

TL;DR

This paper explores the computational complexity and implementation of SAT-based bounded fitting algorithms for the description logic ALC, providing probabilistic guarantees and empirical evaluation.

Contribution

It demonstrates NP-completeness of bounded fitting for ALC, introduces a SAT-based implementation, and compares it with existing tools, highlighting its guarantees and practical performance.

Findings

Bounded fitting NP-complete for all studied fragments of ALC.

SAT-based implementation effectively solves bounded fitting problems.

Compared with other tools, our approach offers probabilistic guarantees.

Abstract

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.