How to leverage the fact that I'm solving 1000's of very similar SMT instances?

I have a core SMT solver problem consisting of 100,000 bit-vector array clauses, and one 10000-dimensional bit-vector array. Then, my program takes as input k << 100,000 new clauses, and adds them to the core SMT problem. My goal is, for any input of k clauses, to solve the entire problem.

Is there any static optimization or learning I could do on the core problem in order to find a better way to solve each of its siblings? For instance, is there some property of the graph of bit-vector variables being constrained in each clause that I could use as a heuristic for solving the specific instances?

Thanks!

Some SAT solvers and SMT solvers offer an interface that lets you push clauses, and then later pop/retract them and push some new ones. You could explore to see whether this offers a speedup in your situation. There are no guarantees, and the only way to tell is to try it.

StackExchange Computer Science Q#127991, answer score: 3