Satisfiability Modulo Theory Meets Inductive Logic Programming

TL;DR

This paper introduces a modular approach combining Inductive Logic Programming with Satisfiability Modulo Theories, enabling the induction of rules that include both relational predicates and numerical constraints, thus enhancing expressivity.

Contribution

It presents a novel modular framework coupling PyGol with Z3, allowing ILP to incorporate numerical constraints via SMT solving, which was limited in prior ILP systems.

Findings

Supports induction of hybrid symbolic and numerical rules

Extends ILP expressivity with linear and nonlinear arithmetic

Demonstrates effectiveness on synthetic datasets for complex reasoning

Abstract

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.