Satisfiability.jl

Satisfiability.jl: Satisfiability Modulo Theories in Julia - Published in JOSS (2024)

https://github.com/elsoroka/satisfiability.jl

Science Score: 100.0%

This score indicates how likely this project is to be science-related based on various indicators:

✓
CITATION.cff file
Found CITATION.cff file
✓
codemeta.json file
Found codemeta.json file
✓
.zenodo.json file
Found .zenodo.json file
✓
DOI references
Found 4 DOI reference(s) in README and JOSS metadata
✓
Academic publication links
Links to: joss.theoj.org
✓
Committers with academic emails
3 of 10 committers (30.0%) from academic institutions
○
Institutional organization owner
✓
JOSS paper metadata
Published in Journal of Open Source Software

Keywords

satisfiability-modulo-theories smt-lib

Keywords from Contributors

investing pde standardization turing-machine genetic-algorithm energy-system plasma benchmarking hydrology distribution

Last synced: 6 months ago · JSON representation ·

Repository

Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.

Basic Info

Host: GitHub
Owner: elsoroka
License: mit
Language: Julia
Default Branch: main
Homepage: https://elsoroka.github.io/Satisfiability.jl/
Size: 2.87 MB

Statistics

Stars: 48
Watchers: 7
Forks: 7
Open Issues: 15
Releases: 4

Topics

satisfiability-modulo-theories smt-lib

Created almost 3 years ago · Last pushed 6 months ago

Metadata Files

Readme License Citation

Satisfiability.jl

Satisfiability.jl is a package for representing satisfiability modulo theories (SMT) problems in Julia. This package provides a simple front-end interface to common SMT solvers, including full support for vector-valued and matrix-valued expressions. Currently, the theories of propositional logic, uninterpreted functions, Integers, Reals and fixed-size BitVectors are supported. We will eventually add support for all SMT-LIB standard theories.

What you can do with this package: * Cleanly specify SMT expressions using Julia's built-in broadcasting and iteration capabilities to write concise expressions. * Generate files in the SMT-LIB specification language. * Interact with any solver that follows the SMT-LIB standard. We test with Z3, CVC5, and Yices.

You can read the documentation here.

Examples

Solving the vector-valued Boolean problem

(x1 ∧ y1) ∨ (¬x1 ∧ y1) ∧ ... ∧ (xn ∧ yn) ∨ (¬xn ∧ yn) julia n = 10 @satvariable(x[1:n], Bool) @satvariable(y[1:n], Bool) expr = (x .∧ y) .∨ (¬x .∧ y) status = sat!(expr, solver=Z3()) println("x = $(value(x)), y = $(value(y))")

Investigating rounding of real numbers

This problem (from Microsoft's Z3 tutorials) uses mixed integer and real variables to figure out whether there exists a constant a and two real numbers xR and yR such that round(xR) + round(yR) > a while xR + yR < a. ```julia @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))") ```

Uninterpreted functions

An uninterpreted function is a function where the input-to-output mapping isn't known. The task of the SMT solver is to find this mapping such that some logical statements hole true. Let's find out if there exists a function f(x) such that f(f(x)) == x, f(x) == y and x != y.

```julia @satvariable(x, Bool) @satvariable(y, Bool) @uninterpreted(f, Bool, Bool)

status = sat!(distinct(x,y), f(x) == y, f(f(x)) == x, solver=Z3()) println("status = $status") ```

The problem is :SAT, so there is such a function! Since the satisfying assignment for an uninterpreted function is itself a function, Satisfiability.jl sets the value of f to this function. Now calling f(value) returns the value of this satisfying assignment.

Using a different solver

Now let's suppose we want to use Yices, another SMT solver. Unlike Z3, Yices requires setting the logic manually. Here we set it to "QF_UFLIA" - "Quantifier free uninterpreted functions, linear integer arithmetic".

```julia @satvariable(x, Bool) @satvariable(y, Bool) @uninterpreted(f, Bool, Bool)

status = sat!(distinct(x,y), f(x) == y, f(f(x)) == x, solver=Yices(), logic="QF_UFLIA") println("status = $status")

println(f(x.value)) # prints 0 println(f(x.value) == y.value) # true println(f(f(x.value)) == x.value) # true ``` We see this yields the same result.

Proving a bitwise version of de Morgan's law.

In this example we want to show there is NO possible value of x and y such that de Morgan's bitwise law doesn't hold. ```julia @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. ```

Development status

Release 0.1.2 is out! You can install it with the command using Pkg; Pkg.add("Satisfiability"). Please help make the Julia ecosystem better for everyone by opening a GitHub issue if you have feedback or find a bug.

Contributing

Contribution guidelines are here. If you're not sure how to get started, take a look at the Roadmap and anything tagged help wanted.

Owner

Name: Emiko Soroka
Login: elsoroka
Kind: user
Location: Palo Alto, CA. USA
Company: Stanford University

Repositories: 3
Profile: https://github.com/elsoroka

JOSS Publication

Satisfiability.jl: Satisfiability Modulo Theories in Julia

Published

August 20, 2024

DOI

10.21105/joss.06757

Volume 9, Issue 100, Page 6757

Authors

Emiko Soroka

Stanford University Department of Aeronautics and Astronautics, Stanford CA 94305, USA

Mykel J. Kochenderfer

Stanford University Department of Aeronautics and Astronautics, Stanford CA 94305, USA

Sanjay Lall

Stanford University Department of Electrical Engineering, Stanford CA 94305, USA

Editor

Patrick Diehl

Citation (CITATION.cff)

cff-version: "1.2.0"
authors:
- family-names: Soroka
  given-names: Emiko
  orcid: "https://orcid.org/0009-0001-2710-469X"
- family-names: Kochenderfer
  given-names: Mykel J.
  orcid: "https://orcid.org/0000-0002-7238-9663"
- family-names: Lall
  given-names: Sanjay
  orcid: "https://orcid.org/0000-0002-1783-5309"
contact:
- family-names: Soroka
  given-names: Emiko
  orcid: "https://orcid.org/0009-0001-2710-469X"
- family-names: Kochenderfer
  given-names: Mykel J.
  orcid: "https://orcid.org/0000-0002-7238-9663"
- family-names: Lall
  given-names: Sanjay
  orcid: "https://orcid.org/0000-0002-1783-5309"
doi: 10.6084/m9.figshare.26768461
message: If you use this software, please cite our article in the
  Journal of Open Source Software.
preferred-citation:
  authors:
  - family-names: Soroka
    given-names: Emiko
    orcid: "https://orcid.org/0009-0001-2710-469X"
  - family-names: Kochenderfer
    given-names: Mykel J.
    orcid: "https://orcid.org/0000-0002-7238-9663"
  - family-names: Lall
    given-names: Sanjay
    orcid: "https://orcid.org/0000-0002-1783-5309"
  date-published: 2024-08-20
  doi: 10.21105/joss.06757
  issn: 2475-9066
  issue: 100
  journal: Journal of Open Source Software
  publisher:
    name: Open Journals
  start: 6757
  title: "Satisfiability.jl: Satisfiability Modulo Theories in Julia"
  type: article
  url: "https://joss.theoj.org/papers/10.21105/joss.06757"
  volume: 9
title: "Satisfiability.jl: Satisfiability Modulo Theories in Julia"

GitHub Events

Total

Create event: 2
Release event: 1
Issues event: 11
Watch event: 15
Delete event: 2
Issue comment event: 58
Push event: 16
Pull request review event: 11
Pull request event: 32
Fork event: 4

Last Year

Create event: 2
Release event: 1
Issues event: 11
Watch event: 15
Delete event: 2
Issue comment event: 58
Push event: 16
Pull request review event: 11
Pull request event: 32
Fork event: 4

Committers

Last synced: 7 months ago

All Time

Total Commits: 309
Total Committers: 10
Avg Commits per committer: 30.9
Development Distribution Score (DDS): 0.113

Past Year

Commits: 27
Committers: 7
Avg Commits per committer: 3.857
Development Distribution Score (DDS): 0.519

Top Committers

Name	Email	Commits
Emiko Soroka	e**o@m**m	274
Fe-r-oz	f**l@g**m	13
dependabot[bot]	4****]	5
Martin Kunz	m**z@e**z	5
Mykel Kochenderfer	m**l@s**u	4
ℝafael Bailo	D**o@g**m	3
jchanke	j**2@a**u	2
Thomas Schmelzer	t**r@g**m	1
Nikos Pitsianis	p**s@y**m	1
Daniel S. Katz	d**z@i**g	1

Committer Domains (Top 20 + Academic)

ieee.org: 1 andrew.cmu.edu: 1 stanford.edu: 1 email.cz: 1 me.com: 1

Issues and Pull Requests

Last synced: 6 months ago

All Time

Total issues: 31
Total pull requests: 89
Average time to close issues: 14 days
Average time to close pull requests: 3 days
Total issue authors: 13
Total pull request authors: 10
Average comments per issue: 2.45
Average comments per pull request: 0.92
Merged pull requests: 83
Bot issues: 0
Bot pull requests: 11

Past Year

Issues: 7
Pull requests: 29
Average time to close issues: about 17 hours
Average time to close pull requests: 7 days
Issue authors: 5
Pull request authors: 5
Average comments per issue: 0.71
Average comments per pull request: 1.52
Merged pull requests: 24
Bot issues: 0
Bot pull requests: 3

View more stats

Top Authors

Issue Authors

elsoroka (11)
mykelk (5)
Fe-r-oz (3)
rafaelbailo (2)
JuliaTagBot (2)
EveWCheng (1)
zygi (1)
pitsianis (1)
remysucre (1)
kunzaatko (1)
jchanke (1)
computablee (1)
vyudu (1)

Pull Request Authors

elsoroka (39)
Fe-r-oz (20)
dependabot[bot] (11)
kunzaatko (9)
mykelk (5)
rafaelbailo (4)
jchanke (4)
pitsianis (2)
tschm (2)
danielskatz (2)

Top Labels

Issue Labels

enhancement (7) bug (5) help wanted (1) question (1) documentation (1)

Pull Request Labels

dependencies (11) bug (2) github_actions (1)

Packages

Total packages: 1
Total downloads:
- julia 3 total

Total dependent packages: 0
Total dependent repositories: 0
Total versions: 3

juliahub.com: Satisfiability

Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.

Homepage: https://elsoroka.github.io/Satisfiability.jl/
Documentation: https://docs.juliahub.com/General/Satisfiability/stable/
License: MIT
Latest release: 0.2.0
published over 1 year ago

Versions: 3
Dependent Packages: 0
Dependent Repositories: 0
Downloads: 3 Total

Rankings

Dependent repos count: 10.2%

Average: 23.9%

Dependent packages count: 37.6%

Last synced: 6 months ago

Dependencies

.github/workflows/ci.yml actions

actions/checkout master composite
codecov/codecov-action v3 composite
julia-actions/julia-buildpkg v1 composite
julia-actions/julia-processcoverage v1 composite
julia-actions/julia-runtest v1 composite
julia-actions/setup-julia v1 composite

.github/workflows/docs.yml actions

actions/checkout v3 composite
julia-actions/julia-buildpkg v1 composite
julia-actions/julia-docdeploy v1 composite

.github/workflows/TagBot.yml actions

JuliaRegistries/TagBot v1 composite

examples/paper_examples/Dockerfile docker

julia 1.9 build

Satisfiability.jl

Science Score: 100.0%

Keywords

Keywords from Contributors

Basic Info

Statistics

Topics

Metadata Files

Examples

Solving the vector-valued Boolean problem

Investigating rounding of real numbers

Uninterpreted functions

Using a different solver

Proving a bitwise version of de Morgan's law.

Development status

Contributing

JOSS Publication

Satisfiability.jl: Satisfiability Modulo Theories in Julia

Authors

Editor

Tags

Citation (CITATION.cff)

GitHub Events

Total

Last Year

All Time

Past Year

Top Committers

Committer Domains (Top 20 + Academic)

All Time

Past Year

Top Authors

Issue Authors

Pull Request Authors

Top Labels

Issue Labels

Pull Request Labels

Packages

juliahub.com: Satisfiability

Rankings

Dependencies