Extending SMT Solving with Non-Ground Clause Learning
This research contributes to the theoretical foundations of SMT solving, which is a core component of many automated reasoning and verification tools.
A new SMT solving method is proposed that extends CDCL(T)-style reasoning by performing conflict analysis on non-ground clauses. This approach aims to produce more general learned clauses and potentially shorter proofs compared to traditional methods that only learn ground clauses. The method combines ground instantiations with non-ground conflict analysis.
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.
