Improving SMT solvers by learning from non-ground conflicts
Extending SMT Solving with Non-Ground Clause Learning
Artificial IntelligenceLogic in Computer Science
Summary
Solvers that check logical formulas often work by turning general rules into specific examples. When a contradiction happens, current methods only learn from these specific examples, missing the chance to learn more general lessons. The authors develop a new way to analyze contradictions that reasons directly with the original general rules, allowing the solver to learn broader facts and avoid repeating mistakes. This approach also integrates a technique called chronological backtracking to make the solving process more efficient.
What this means in practice
- •For software verification engineers: Enable verification tools to detect bugs faster by learning more general failure patterns from logical constraints involving variables.
- •For automated reasoning developers: Implement solvers that produce more compact proofs and reduce redundant search when checking satisfiability of formulas with quantifiers.
A theory result. No direct application yet.
Authors
Yasmine Briefs, Christoph Weidenbach
Abstract
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.