[ANN] Satisfiability.jl: a simple interface to theorem provers using the SMT-LIB standard

Package Announcements
,
1

Satisfiability.jl is a package for representing satisfiability modulo theories (SMT) problems in Julia.

SMT is used in formal verification and synthesis. You can use it to find satisfying assignments for logical statements (finding a set of values that make the statement true), or to prove that no satisfying assignment exists. More practically, you can verify software correctness (some good examples are in Chapter 5 of “SAT/SMT by Example”), find a set of inputs for which a system crashes, or prove your Amazon EC2 instance is secure (Amazon’s IAM access analyzer uses SMT).

Satisfiability.jl is not a theorem prover. It is a simple interface to existing provers (Z3, cvc5, etc) using the SMT-LIB language. Currently, the theories of propositional logic, Integers, Reals and fixed-size BitVectors are supported. We plan to add support for the remaining SMT-LIB standard theories: IEEE floating points, Arrays, and Strings.

If you’re familiar with PySMT, Satisfiability.jl seeks to fill the same niche in the Julia ecosystem. Our inspirations for the package interface are JuMP and Convex.jl

What Satisfiability.jl does

  • Provides a high-level interface to specify single-valued or vector-valued SMT expressions using Julia’s built-in capabilities.
  • Generates files in the SMT-LIB specification language.
  • Interacts with any solver that follows the SMT-LIB standard.

Examples

These are from the package documentation, linked in the respository!

Proving a bitwise version of de Morgan’s law.

Verify there is NO possible value of x and y such that de Morgan’s bitwise law doesn’t hold.

@satvariable(x, BitVector, 64)
@satvariable(y, BitVector, 64)

expr = not((~x & ~y) == ~(x | y))

status = sat!(expr, solver=Z3())
println(status) # if status is UNSAT we proved it.

Investigating rounding of real numbers

We want to find out if there exists a constant a and two real numbers xR and yR such that round(xR) + round(yR) > a while xR + yR < a.

@satvariable(xR, Real)
@satvariable(yR, Real)
@satvariable(x, Int) # x represents a rounded version of xR
@satvariable(y, Int) # y represents a rounded version of yR
@satvariable(a, Int)

exprs = [xR + yR < a,
         x + y > a,
         or(x == xR, ((x < xR) ∧ (xR < x+1)), ((x-1 < xR) ∧ (xR < x))),
         or(y == yR, ((y < yR) ∧ (yR < y+1)), ((y-1 < yR) ∧ (yR < y))),
        ]
status = sat!(exprs)
println("status = $status, xR=$(value(xR)), yR=$(value(yR)), a = $(value(a))")

There are! We get status = SAT, xR=0.666, yR=-0.834, a = 0.

Previous work in Julia SMT

  • Z3.jl provides bindings of the Z3 C++ API
  • PicoSAT.jl provides bindings to the PicoSAT solver (using CNF format).
  • SatisfiabilityInterface.jl was presented at JuliaCon 2021. It’s for “modelling discrete constraint satisfaction problems and encoding them to Boolean satisfiability (SAT) problems.”

Try it out!

I haven’t registered the package yet, so you can install it with using Pkg; Pkg.add(url="https://github.com/elsoroka/Satisfiability.jl/")
You’ll also need a back-end solver. Both Z3 and cvc5 are available for free; the package documentation has instructions to install them.
If you do try it I’d love to hear feedback, ideas, or any issues you encountered!

17 Likes
2

Since I’m a new developer, I would specifically like to solicit feedback on the name Satisfiability.jl. It meets the package name guidelines but I want to ask people’s opinions on it. Thank you!

7 Likes
3

Fantastic stuff! For all those folks who liked PropCheck.jl (which is just a fancy fuzzer), this is the mathematically correct theorem proving counterpart!

Do you have plans for depending (weakly) on Z3.jl or other solvers like cvc5, so that users don’t have to install the solver through their system package manager and instead can just use a JLL from Pkg?

As for the name - I think it’s fine, since this is more or less an interface package. Kind of like Tables.jl is an interface package.

4 Likes
4

Thank you! I haven’t seen PropCheck before so I will make a note to add it to a list of related packages.

Do you have plans for depending (weakly) on Z3.jl or other solvers like cvc5, so that users don’t have to install the solver through their system package manager and instead can just use a JLL from Pkg?

Other Languages’ SMT Packages (PySMT) do this! It’s a good thing to put on a roadmap. Z3.jl (there seem to be 2 but I’m familiar with this one) My main concern is it’s not well documented, so although I’ve used it I’m not confident in understanding it well enough to interface with it.

I use Base.process to talk with solvers but have had difficulty with pipes which I think is related to Julia issue #24717 and the state of two-way communication with long-lived external processes. So other ways to interface with solvers are a good idea, especially if they allow all the dependencies to be Pkg installed.

1 Like
5

As far as I can tell, Z3.jl is the only package providing a Julia interface - z3_jll is just the BinaryBuilder.jl provided binary, built in CI for all platforms Julia (and the binary dependency in question) supports.

According to its README, the package is mostly autogenerated bindings to the C++ library, with the same names & functions as the original library.

I’m not sure which issue in the linked discourse thread you’re referring to exactly, but readavailable doesn’t read in everything by default - the default IOStream does some internal (hidden…) buffering, which is what readavailable ultimately returns. I haven’t heard anything about long lived external processes being particularly problematic themselves though.

1 Like