# Satisfiability Modulo Theory Meets Inductive Logic Programming

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 43 references that are in the map.
- First posted on arXiv 15 Dec 2025.

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

- [Learning Explanatory Rules from Noisy Data](https://mlsanity.com/paper/1711.04574/) (2017)
- [Learning programs by learning from failures](https://mlsanity.com/paper/2005.02259/) (2020)
- [Inductive logic programming at 30](https://mlsanity.com/paper/2102.10556/) (2021)
- [Differentiable Inductive Logic Programming for Structured Examples](https://mlsanity.com/paper/2103.01719/) (2021)
- [Learning Higher-Order Programs without Meta-Interpretive Learning](https://mlsanity.com/paper/2112.14603/) (2021)
- [Approximate Counting in SMT and Value Estimation for Probabilistic Programs](https://mlsanity.com/paper/1411.0659/) (2014)
- [QCBA: Improving Rule Classifiers Learned from Quantitative Data by Recovering Information Lost by Discretisation](https://mlsanity.com/paper/1711.10166/) (2017)
- [Learning programs with magic values](https://mlsanity.com/paper/2208.03238/) (2022)
- [Relational program synthesis with numerical reasoning](https://mlsanity.com/paper/2210.00764/) (2022)
- [SMT + ILP](https://mlsanity.com/paper/2001.05208/) (2020)

## Abstract (arXiv)

Inductive Logic Programming (ILP) provides interpretable rule learning in relational domains, yet remains limited in its ability to induce and reason with numerical constraints. Classical ILP systems operate over discrete predicates and typically rely on discretisation or hand-crafted numerical predicates, making it difficult to infer thresholds or arithmetic relations that must hold jointly across examples. Recent work has begun to address these limitations through tighter integrations of ILP with Satisfiability Modulo Theories (SMT) or specialised numerical inference mechanisms. In this paper we investigate a modular alternative that couples the ILP system PyGol with the SMT solver Z3. Candidate clauses proposed by PyGol are interpreted as quantifier-free formulas over background theories such as linear or nonlinear real arithmetic, allowing numerical parameters to be instantiated and verified by the SMT solver while preserving ILP's declarative relational bias. This supports the induction of hybrid rules that combine symbolic predicates with learned numerical constraints, including thresholds, intervals, and multi-literal arithmetic relations. We formalise this SMT-ILP setting and evaluate it on a suite of synthetic datasets designed to probe linear, relational, nonlinear, and multi-hop reasoning. The results illustrate how a modular SMT-ILP architecture can extend the expressivity of symbolic rule learning, complementing prior numerical ILP approaches while providing a flexible basis for future extensions toward richer theory-aware induction.