# Julia Tools for Large-Scale SMT/SAT problems?

**URL:** https://discourse.julialang.org/t/julia-tools-for-large-scale-smt-sat-problems/123744
**Category:** Optimization (Mathematical)
**Tags:** question
**Created:** [December 12, 2024, 9:01am UTC](https://discourse.julialang.org/t/julia-tools-for-large-scale-smt-sat-problems/123744 "2024-12-12T09:01:47Z")
**Posts on this page:** 2
**Page:** 1

<div class="post-metadata">

### Author: ![Fe-r-oz](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/fe-r-oz/32/216415_2.png) [@Fe-r-oz](https://discourse.julialang.org/u/Fe-r-oz)
#### Post date: [December 12, 2024, 9:01am UTC](https://discourse.julialang.org/t/julia-tools-for-large-scale-smt-sat-problems/123744/1 "2024-12-12T09:01:47Z")

</div>

Hi, Everyone,

I’m exploring options for working with SAT/SMT solvers in Julia. So far, I’ve come across [Z3.jl](https://github.com/ahumenberger/Z3.jl) and [Satisfiability.jl](https://github.com/elsoroka/Satisfiability.jl), and I really appreciate the [JuMP](https://github.com/jump-dev/JuMP.jl)-like idiomatic interface of [Satisfiability.jl](https://github.com/elsoroka/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,

---

<div class="post-metadata">

### Author: ![odow](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/odow/32/28685_2.png) [@odow](https://discourse.julialang.org/u/odow)
#### Post date: [December 16, 2024, 9:17pm UTC](https://discourse.julialang.org/t/julia-tools-for-large-scale-smt-sat-problems/123744/2 "2024-12-16T21:17:21Z")

</div>

Hi @Fe-r-oz, welcome to the forum 😄

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?