# SAT-Based Bounded Fitting for the Description Logic ALC

arXiv: https://arxiv.org/abs/2507.21752 · HTML: https://mlsanity.com/paper/2507.21752/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 41 references that are in the map.
- First posted on arXiv 29 Jul 2025.

## Builds on (most cited first, 8 of 8)

- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [YAGO 4.5: A Large and Clean Knowledge Base with a Rich Taxonomy](https://mlsanity.com/paper/2308.11884/) (2023)
- [EvoLearner: Learning Description Logics with Evolutionary Algorithms](https://mlsanity.com/paper/2111.04879/) (2021)
- [Neural Class Expression Synthesis](https://mlsanity.com/paper/2111.08486/) (2021)
- [SAT-Based PAC Learning of Description Logic Concepts](https://mlsanity.com/paper/2305.08511/) (2023)
- [Learning temporal formulas from examples is hard](https://mlsanity.com/paper/2312.16336/) (2023)
- [SAT-based Learning of Computation Tree Logic](https://mlsanity.com/paper/2402.06366/) (2024)
- [On the non-efficient PAC learnability of conjunctive queries](https://mlsanity.com/paper/2208.10255/) (2022)

## Built on by (most cited first, 1 of 1)

- [Bounded Fitting for Expressive Description Logics](https://mlsanity.com/paper/2605.07452/) (2026)

## Abstract (arXiv)

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.