# Extending SMT Solving with Non-Ground Clause Learning

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 42 references that are in the map.
- First posted on arXiv 10 Sep 2026.

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

- [Conflict Resolution: a First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning](https://mlsanity.com/paper/1602.04568/) (2016)
- [SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning](https://mlsanity.com/paper/2305.12926/) (2023)
- [A Two-Watched Literal Scheme for First-Order Logic](https://mlsanity.com/paper/2605.21335/) (2026)

## Abstract (arXiv)

Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style reasoning. When a conflict is found, conflict analysis learns only a ground clause, even though the conflict comes from instances of non-ground clauses. Yet non-ground reasoning can give exponentially shorter proofs than purely ground reasoning. We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. The solver reasons on ground instances, but the resolution steps of conflict analysis are performed on their original non-ground clauses. This produces learned clauses that are typically more general than the ground conflict. With a suitable strategy, the learned clauses are even non-redundant. We also show how chronological backtracking can be included in SMT solving. Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning, and we prove that it simulates CDCL, SCL(FOL), SCL(T), and even Resolution.