Julia Tools for Large-Scale SMT/SAT problems?

Specific Domains Optimization (Mathematical)
1

Hi, Everyone,

I’m exploring options for working with SAT/SMT solvers in Julia. So far, I’ve come across Z3.jl and Satisfiability.jl, and I really appreciate the JuMP-like idiomatic interface of Satisfiability.jl, Are there other libraries, bindings, or tools in the Julia ecosystem designed for industrial-scale SMT/SAT problems?

I’m interested in understanding the practical limits of aforementioned tools, in terms of problem size, especially when applied to large-scale SAT/SMT problems. Are there benchmarks, examples, or specific use cases that demonstrate their capabilities or limitations?

I’d also love to hear about your experiences working on large-scale SAT/SMT problems in Julia. Which tools or approaches have worked well for you, and are there any challenges or best practices you’d recommend?

Any insights or recommendations would be greatly appreciated.

Happy New Year

Best Regards,

4 Likes
2

Hi @Fe-r-oz, welcome to the forum :smile:

I’m not aware of other libraries in Julia for SAT problems. It’s something that we have considered adding to JuMP, but we’re not there yet.

The field is rather broad. What problem are you trying to solve?

1 Like