Quantifier instantiation is the dominant approach for non‑ground SMT solving: solvers first generate ground instances and then apply CDCL(T)‑style reasoning to the resulting ground SMT problems. When a conflict is detected, traditional conflict analysis learns only a ground clause, even though the conflict originates from instances of non‑ground clauses. Non‑ground reasoning, however, can yield exponentially shorter proofs.
We introduce a calculus that combines ground instantiation, CDCL(T) rules, and non‑ground conflict analysis. The solver still reasons on ground instances, but the resolution steps of conflict analysis are performed on the original non‑ground clauses from which those instances were derived. Consequently, the learned clauses are typically more general than purely ground conflicts, and with an appropriate strategy they can be made non‑redundant.
We also show how chronological backtracking can be incorporated into SMT solving, further improving efficiency. This calculus provides a unified setting for CDCL(T)‑style SMT solving, a variety of instantiation‑based procedures, and non‑ground clause learning, and we prove that it simulates CDCL, SCL(FOL), SCL(T), and even classical Resolution.
Review: By preserving non‑ground information during conflict analysis, the approach achieves stronger learning capabilities, offering theoretically tighter proof lengths for SMT solvers and a clear framework for practical implementation.