Candidate: Nham Van Le
Title: Novel clause sharing strategies for distributed SMT solvers
Date: August 7, 2024
Time: 10:00 AM
Place: REMOTE ATTENDANCE
Supervisor(s): Gurfinkel, Arie
All are welcome!
Abstract:
We introduce cvc5-d, a tool for portfolio-based distributed SMT solving. We propose a general architecture consisting of two main components: (i) solvers extended with the capability of sharing and importing information on the fly while solving; and (ii) a central manager that orchestrates and monitors solvers while also deciding which information to share with which solvers.
We introduce new information sharing strategies based on the idea of maximizing the amount of “good” diversity in the system. We extend the cvc5 SMT solver to implement the interface required for cvc5-d. We show that on hard benchmarks from recent related work, cvc5-d instantiated with cvc5 outperforms a state-of-the-art partitioning-based approach, is competitive with existing portfolio approaches, and enables portfolio solving for new benchmarks.