Extending SMT Solving with Non-Ground Clause Learning
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…
We haven't written up this one. arXiv cs.AI has the full story — the link below goes straight to it.
