From 565025e20c7c4653202997e62ce7edf9be41f5b2 Mon Sep 17 00:00:00 2001 From: Emiko Soroka Date: Sat, 1 Jul 2023 14:04:16 -0700 Subject: [PATCH] Updated documentation with Real and Int, job shop example md and general wording updates. Added an FAQ page. --- README.md | 8 ++-- docs/make.jl | 8 +++- docs/src/example_job_shop.md | 52 +++++++++++++++++++++++++ docs/src/example_scheduling.md | 3 +- docs/src/faq.md | 54 ++++++++++++++++++++++++++ docs/src/functions.md | 37 ++++++++++++++++-- docs/src/index.md | 11 +++++- docs/src/tutorial.md | 19 +++++++++- examples/job_shop_scheduling.jl | 6 ++- src/BoolExpr.jl | 2 +- src/IntExpr.jl | 67 ++++++++++++++++++++------------- 11 files changed, 225 insertions(+), 42 deletions(-) create mode 100644 docs/src/example_job_shop.md create mode 100644 docs/src/faq.md diff --git a/README.md b/README.md index 40859db..50306c9 100644 --- a/README.md +++ b/README.md @@ -3,11 +3,11 @@ [![Build Status](https://github.com/elsoroka/BooleanSatisfiability.jl/actions/workflows/CI.yml/badge.svg?branch=main)](https://github.com/elsoroka/BooleanSatisfiability.jl/actions/workflows/CI.yml?query=branch%3Amain) -A package for solving Boolean satisfiability problems in Julia. +BooleanSatisfiability.jl is a package for representing Boolean satisfiability (SAT) and selected other 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. -* Easily specify single-valued or vector-valued Boolean SAT problems using Julia's built-in broadcasting capabilities. -* Generate files in SMTLIB2 format. -* Uses [Z3](https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/) as the back-end solver. +* Easily specify single-valued or vector-valued Boolean SAT, integer or real-valued SMT problems using Julia's built-in broadcasting capabilities. +* Generate files in [SMT2](http://www.smtlib.org/) format. +* BooleanSatisfiability.jl calls [Z3](https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/) as the back-end solver and interprets the result. ## Example diff --git a/docs/make.jl b/docs/make.jl index db4a30e..ed47aab 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -6,14 +6,20 @@ using BooleanSatisfiability makedocs(sitename="BooleanSatisfiability.jl", repo = "https://github.com/elsoroka/BooleanSatisfiability.jl", clean=true, +draft=true, root=".", source = "src", +modules = [BooleanSatisfiability], pages = [ "index.md", "tutorial.md", + "faq.md", "Examples" => [ - "example_scheduling.md" + "example_scheduling.md", + "example_job_shop.md" ], + "Library" => [ "functions.md" + ], ] ) \ No newline at end of file diff --git a/docs/src/example_job_shop.md b/docs/src/example_job_shop.md new file mode 100644 index 0000000..efedaf3 --- /dev/null +++ b/docs/src/example_job_shop.md @@ -0,0 +1,52 @@ + +# Job shop scheduling + +The job shop scheduling problem is a linear integer problem arising in operations research. + +Suppose you are managing a machine shop with several different jobs in progress. +Each job consists of a series of tasks. Some of the tasks have ordering constraints: e.g. parts must be manufactured before they can be installed in a larger assembly. +Due to equipment constraints, we cannot schedule two tasks requiring the same machine at the same time. Additionally, all tasks must have a worker assigned to complete them. + +In this problem ([from Microsoft's Z3 tutorial](https://microsoft.github.io/z3guide/docs/theories/Arithmetic/)) we have three jobs, each consisting of one task to be completed first by worker A and one to be completed second by worker B. Each task has an integer-valued duration. Workers cannot work on two tasks at once or take each others' tasks. + +We'd like to find a solution such that all three jobs can be completed in an 8-hour workday. + +* Define two vector-valued variables t1 and t2 such that tj[i] is the start time of job i for worker j. + +* Define two vector-valued variables d1 and d2 such that dj[i] is the duration of job i for worker j. + +```@example +using BooleanSatisfiability +n = 3 # number of jobs +m = 2 # number of tasks per job +t1 = Int(n,"t1") +t2 = Int(n, "t2") +d1 = [2; 3; 2] +d2 = [1; 1; 3] +``` +A start time of 0 corresponds to the first hour of the workday, and an end time of 8 corresponds to the last hour of the workday. +```@example +working_hours = all(and.(t1 .>= 0, t2 .+ d2 .<= 8)) +``` + +Sequencing constraint: For each job, A must complete the first task before B can start the second task +```@example +sequencing = and(t2 .>= t1 .+ d1) +``` + +Overlap constraint between all permutations +```@example +overlaps = [(1,2), (1,3), (2,3)] +overlap_1 = all([or( t1[i] >= t1[j] + d1[j], t1[j] >= t1[i] + d1[i]) for (i,j) in overlaps]) +overlap_2 = all([or( t2[i] >= t2[j] + d2[j], t2[j] >= t2[i] + d2[i]) for (i,j) in overlaps]) +``` + +Solve the problem +```@example +status = sat!(working_hours, sequencing, overlap_1, overlap_2) +println("status = $status") +if status == :SAT + println("t1 = $(value(t1))") + println("t2 = $(value(t2))") +end +``` \ No newline at end of file diff --git a/docs/src/example_scheduling.md b/docs/src/example_scheduling.md index 5014d72..309452f 100644 --- a/docs/src/example_scheduling.md +++ b/docs/src/example_scheduling.md @@ -1,4 +1,4 @@ -# Scheduling example +# Finding a meeting time We have n people's availabilities for the meeting times 9a, 10a, 11a, 12, 1p, 2p, 3p, 4p. Each person's availability is reprsented as a Boolean vector ``a^\top\in \{0,1\}^8``. We would like to schedule ``J`` meetings between different groups of people, represented by ``J`` index sets ``\mathcal{I_j}\subseteq\{1,\dots,n\}``. @@ -13,6 +13,7 @@ Rules: We concatenate the availability row vectors into a 5 x 8 Boolean matrix ``\bar A``. ```@example using BooleanSatisfiability + n = 5 # number of people T = 8 # number of times diff --git a/docs/src/faq.md b/docs/src/faq.md new file mode 100644 index 0000000..04259d8 --- /dev/null +++ b/docs/src/faq.md @@ -0,0 +1,54 @@ +# FAQ +```@contents +Pages = ["faq.md"] +Depth = 3 +``` + +## Where can I get help? +Please open a Github issue! This is a new package and we would love to hear your suggestions, bug reports, feature requests, and other commentary. + +## Isn't this functionality included in JuMP? +[JuMP](https://jump.dev/) provides support for [integer and Boolean-valued variables](https://jump.dev/JuMP.jl/stable/manual/variables/#Binary-variables), however it is developed primarily to support mathematical optimization over real-valued or integer-valued variables and continuous functions. As such, JuMP interfaces with solvers such as ECOS, MOSEK, and Gurobi that are intended for continuous optimization problems. When you use JuMP to solve a problem with discrete variables, your solver will likely use a branch-and-bound style method. + +### Should I use JuMP or BooleanSatisfiability? +If you have a problem with mixed real and discrete variables, you should probably use JuMP to call a branch-and-bound solver. + +If you have a problem with only discrete variables, especially a large one, you should consider using a SAT solver. + +## How do I solve SAT problems in other langugages? +Z3 has [APIs](https://z3prover.github.io/api/html/index.html) for C, C++, .NET, Java, Python and ML/OCaml. Additionally, Microsoft Research provides [tutorials](https://microsoft.github.io/z3guide/programming/Z3%20JavaScript%20Examples) for using Z3 in Python and JavaScript. + +## What about other theories in the SMT standard? +In the future support may be added for additional theories supported in the SMTLIB2 standard, such as bitvectors and arrays. + +## How can I extract an unsatisfiability proof? +Instead of calling `sat!`, use `save` to write the SMT representation of your problem to a file. Then invoke the solver from your command line, feed it the file and issue `(get-proof)` in `unsat` mode. + +Yes, that was a long way of saying "we don't support this feature". (Unsatisfiability proofs are difficult to support because the SMT2 standard doesn't specify their format - it's solver-dependent.) However you can still specify your problem in BooleanSatisfiability.jl and use the generated SMT file any way you like. + +## What does BooleanSatisfiability.jl actually do? +We provide a high-level interface to SAT solvers. SAT solvers can accept input in the [SMT2](http://www.smtlib.org/) format, which is very powerful but not easy to read. When you specify a SAT problem in BooleanSatisfiability.jl and call `sat!`, we generate an SMT2-formatted **representation** of the problem, feed it to a solver, then interpret the result. + +You can feed the solver yourself. Call `save` instead of SAT to write the SMT2 representation of your problem to a file, where you can inspect it or add additional commands. + +# LFAQ +(Less frequently-asked questions.) + +## Where do all the long, ugly names in the SMT file come from? +To prevent names from being duplicated, BooleanSatisfiability.jl names new expressions using the Julia `hash` of their child expressions. + +For example, suppose you have +```@example +a = Int("a") +b = Int("b") +expr = a <= b +print(smt(expr)) +``` +The (long, ugly) name of the combined expression `a <= b` is generated by hashing the names `a` and `b`. + +**Q:** Why don't you just concatenate `a` and `b` and call it `LEQ_a_b`? + +**A:** Because what if we have `a = Int(10,"a"); expr = sum(a)`? Are we going to say `expr.name = ADD_a_1_a_2_a_3_a_4_a_5_a_6_a_7_a_8_a_9_a_10`? If not, where do we draw the line? What if we called it `ADD_a_1__a_10`, but then we defined `expr2 = a[1] + a[3:8] + a[10]`? Then both `expr` and `expr1` would share the name `ADD_a_1__a_10` and all heck would break loose. + +If you think of a nicer way to name expressions, please open an issue! + diff --git a/docs/src/functions.md b/docs/src/functions.md index 8f61386..0c9e9a3 100644 --- a/docs/src/functions.md +++ b/docs/src/functions.md @@ -5,12 +5,15 @@ Depth = 3 ``` Test link [link](#Logical-Operations) -## Defining Boolean Variables +## Defining variables ```@docs Bool(name::String) +Int(name::String) +Real(name::String) ``` -## Logical Operations +## Logical operations +These are operations in the theory of propositional logic. For a formal definition of this theory, see Figure 3.2 in *The SMT-LIB Standard, Version 2.6*. ```@docs not(z::BoolExpr) and(z1::BoolExpr, z2::BoolExpr) @@ -25,8 +28,31 @@ all(zs::Array{T}) where T <: BoolExpr any(zs::Array{T}) where T <: BoolExpr ``` +## Arithmetic operations +These are operations in the theory of integer and real-valued arithmetic. + +Note that `+`, `-`, and `*` follow type promotion rules: if both `a` and `b` are `IntExpr`s, `a+b` will have type `IntExpr`. If either `a` or `b` is a `RealExpr`, the result will have type `RealExpr`. Division `\` is defined only in the theory of real-valued arithmetic, thus it always has return type `RealExpr`. +For a formal definition of the theory of integer arithmetic, see Figure 3.3 in *The SMT-LIB Standard, Version 2.6*. + +```@docs +Base.:-(a::IntExpr) +Base.:+(a::IntExpr, b::IntExpr) +Base.:-(a::IntExpr, b::IntExpr) +Base.:*(a::RealExpr, b::RealExpr) +Base.:/(a::RealExpr, b::RealExpr) +``` + +### Comparison operators +```@docs +Base.:(==)(a::AbstractExpr, b::AbstractExpr) +Base.:<(a::AbstractExpr, b::AbstractExpr) +Base.:<=(a::AbstractExpr, b::AbstractExpr) +Base.:>(a::AbstractExpr, b::AbstractExpr) +Base.:>=(a::AbstractExpr, b::AbstractExpr) +``` + ## Generating the SMT representation of a problem -{#smt-representation} + ```@docs smt(zs::Array{T}) where T <: BoolExpr save(prob::BoolExpr; filename="out") @@ -37,3 +63,8 @@ save(prob::BoolExpr; filename="out") sat!(prob::BoolExpr) value(zs::Array{T}) where T <: AbstractExpr ``` + +## Miscellaneous functions +```@docs +Base.isequal(a::AbstractExpr, b::AbstractExpr) +``` \ No newline at end of file diff --git a/docs/src/index.md b/docs/src/index.md index 06c78b7..d047e67 100644 --- a/docs/src/index.md +++ b/docs/src/index.md @@ -1,5 +1,5 @@ -# Solving Boolean SAT Problems in Julia -BooleanSatisfiability.jl is a package for representing Boolean satisfiability (SAT) problems in Julia. This package provides a simple front-end interface to common SAT solvers with full support for vector-valued and matrix-valued Boolean expressions. +# Solving SMT Problems in Julia +BooleanSatisfiability.jl is a package for representing Boolean satisfiability (SAT) and selected other 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. ```@contents Pages = ["index.md"] @@ -31,6 +31,13 @@ Given a Boolean expression, the associated SAT problem can be posed as: * If the assignment does not exist, we say the formula is **unsatisfiable**. +### SMT problems +Satisfiability modulo theories is a superset of Boolean satisfiability. SMT encompasses many other theories besides Boolean logic, two of which are supported here. + +In the **theory of integers**, we can define integer-valued variables and operations such as `+`, `-`, `*` and the comparisons `<`, `<=`, `==`, `=>`, `>`. For example, we could determine whether there exists a satisfying assignment for integers `a` and `b` such that `a <= b, b <= 1 and a + b >= 2`. (There is - set `a = 1` and ` b = 1`.) + +In the **theory of reals**, we can define real-valued variables and operations. Reals use the same operations as integers, plus division (`\`). However, algorithms to solve SMT problems over real variables are often slow and not guaranteed to find a solution. If you have a problem over only real-valued variables, you should use [JuMP](jump.dev/) and a solver like Gurobi instead. + ## How does BooleanSatisfiability.jl work? BooleanSatisfiability.jl provides an **interface** to SAT solvers that accept input in the [SMTLIB2](http://www.smtlib.org/) format. It works by generating the SMT representation of your problem, then invoking a solver to read said file. diff --git a/docs/src/tutorial.md b/docs/src/tutorial.md index c7070b4..c77b0fb 100644 --- a/docs/src/tutorial.md +++ b/docs/src/tutorial.md @@ -1,5 +1,5 @@ # Tutorial -Here we present several mini-examples of SAT problems. +Here we present several mini-examples of SMT problems. ## Proving the validity of De Morgan's law This example is borrowed from Microsoft's [introduction](https://microsoft.github.io/z3guide/docs/logic/propositional-logic/) to Z3 for propositional logic. @@ -32,3 +32,20 @@ println("p = $(value(p))") println("q = $(value(q))") println("r = $(value(r))") ``` + +## Optimizing over integers +The knapsack problem is a famous NP-complete problem in which you are packing a bag that cannot exceed some maximum weight. Given a set of items with known value and weight, you want to pack a subset that maximizes the value. + +A simpler version, illustrated in this [classic XKCD strip](https://xkcd.com/287/), is to pack the bag to exactly its maximum weight (or spend a specific amount of money). +In fact, the problem in the XKCD strip can be expressed as a linear equation over integers. + +```@example +a = Int(6, "a") +c = [215; 275; 335; 355; 420; 580] +expr = and([all(a .>= 0), sum(a .* c) == 1505]) +sat!(expr) +println("Result: $(value(a))") +println("Check: $(sum(value(a) .* c))") +``` + + diff --git a/examples/job_shop_scheduling.jl b/examples/job_shop_scheduling.jl index 36d14e3..c4d1f0b 100644 --- a/examples/job_shop_scheduling.jl +++ b/examples/job_shop_scheduling.jl @@ -34,5 +34,7 @@ overlap_2 = all([or( t2[i] >= t2[j] + d2[j], t2[j] >= t2[i] + d2[i]) for (i,j) i status = sat!(working_hours, sequencing, overlap_1, overlap_2) println("status = $status") -println("t1 = $(value(t1))") -println("t2 = $(value(t2))") \ No newline at end of file +if status == :SAT + println("t1 = $(value(t1))") + println("t2 = $(value(t2))") +end \ No newline at end of file diff --git a/src/BoolExpr.jl b/src/BoolExpr.jl index 0cf1055..bc7601e 100644 --- a/src/BoolExpr.jl +++ b/src/BoolExpr.jl @@ -73,7 +73,7 @@ function Base.string(expr::AbstractExpr, indent=0)::String end end -"Test equality of two BoolExprs." +"Test equality of two AbstractExprs." function Base.isequal(expr1::AbstractExpr, expr2::AbstractExpr) return (expr1.op == expr2.op) && all(expr1.value .== expr2.value) && (expr1.name == expr2.name) && (__is_permutation(expr1.children, expr2.children)) end diff --git a/src/IntExpr.jl b/src/IntExpr.jl index ceed8b0..3d7d80f 100644 --- a/src/IntExpr.jl +++ b/src/IntExpr.jl @@ -92,7 +92,7 @@ __wrap_const(c::Union{Int, Bool}) = IntExpr(:CONST, AbstractExpr[], c, "const_$c a < b a < 0 -Returns the Boolean expression a < b. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. +Returns the Boolean expression a < b. Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia a = Int(n, "a") @@ -112,7 +112,7 @@ end a <= b a <= 0 -Returns the Boolean expression a <= b. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. +Returns the Boolean expression a <= b. Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia a = Int(n, "a") @@ -132,7 +132,7 @@ end a >= b a >= 0 -Returns the Boolean expression a >= b. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. +Returns the Boolean expression a >= b. Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia a = Int(n, "a") @@ -152,7 +152,7 @@ end a > b a > 0 -Returns the Boolean expression a > b. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. +Returns the Boolean expression a > b. Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia a = Int(n, "a") @@ -173,7 +173,20 @@ end # This is because (==) is already defined as a comparison operator between two AbstractExprs. # We can't swap the definitions eq and (==) because that breaks Base behavior. # For example, if (==) generates an equality constraint instead of making a Boolean, you can't write z ∈ [z1,...,zn]. +""" + a == b + a == 1.0 + +Returns the Boolean expression a == b (arithmetic equivalence). Use dot broadcasting for vector-valued and matrix-valued expressions. +```julia +a = Int(n, "a") +b = Int(n, m, "b") +a .== b +``` + +**Note:** To test whether two `AbstractExpr`s are eqivalent (in the sense that all properties are equal, not in the shared-memory-location sense of `===`), use `isequal`. +""" function Base.:(==)(e1::T, e2::T) where T <: AbstractExpr value = isnothing(e1.value) || isnothing(e2.value) ? nothing : e1.value == e2.value name = __get_hash_name(:EQ, [e1, e2]) @@ -203,10 +216,8 @@ eq(e1::NumericInteroperableConst, e2::AbstractExpr) = eq(wrap_const(e1), e2) Return the negative of an Int or Real expression. ```julia - a = Int(n, "a") - -a # this works - b = Int(n, m, "b") - -b # this also works + -Int(n, "a")# this works + -Int(n, m, "b") # this also works ``` """ @@ -281,29 +292,31 @@ end # NumericExpr + NumericExpr # NumericExpr + Const # Const + NumericExpr -#= + """ a + b a + 1 + true - Returns the `Int` | `Real` expression `a+b` (inherits the type of `a+b`). Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. +Return the `Int` | `Real` expression `a+b` (inherits the type of `a+b`). Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. + ```julia a = Int(n, "a") b = Int(n, m, "b") a .+ b -println("typeof a+b: $(typeof(a[1] + b[1]))") +println("typeof a+b: \$(typeof(a[1] + b[1]))") c = Real("c") -println("typeof a+c: $(typeof(a[1] + c))") +println("typeof a+c: \$(typeof(a[1] + c))") z = Bool("z") a .+ z -println("typeof a+z: $(typeof(a[1] + z))") +println("typeof a+z: \$(typeof(a[1] + z))") ``` -"""=# + +""" Base.:+(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :ADD) Base.:+(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :ADD) Base.:+(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = e2 + e1 -#= + """ a - b a - 2 @@ -314,18 +327,18 @@ Returns the `Int` | `Real` expression `a-b` (inherits the type of `a-b`). Use do a = Int(n, "a") b = Int(n, m, "b") a .- b -println("typeof a-b: $(typeof(a[1] - b[1]))") +println("typeof a-b: \$(typeof(a[1] - b[1]))") c = Real("c") -println("typeof a-c: $(typeof(a[1] - c))") +println("typeof a-c: \$(typeof(a[1] - c))") z = Bool("z") a .- z -println("typeof a-z: $(typeof(a[1] - z))") +println("typeof a-z: \$(typeof(a[1] - z))") ``` -"""=# +""" Base.:-(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :SUB) Base.:-(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :SUB) Base.:-(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :SUB) -#= + """ a * b a * 2 @@ -336,18 +349,18 @@ Returns the `Int` | `Real` multiplication expression `a*b` (inherits the type of a = Int(n, "a") b = Int(n, m, "b") a .* b -println("typeof a*b: $(typeof(a[1]*b[1]))") +println("typeof a*b: \$(typeof(a[1]*b[1]))") c = Real("c") -println("typeof a*c: $(typeof(a[1]*c))") +println("typeof a*c: \$(typeof(a[1]*c))") z = Bool("z") a .- z -println("typeof a*z: $(typeof(a[1]*z))") +println("typeof a*z: \$(typeof(a[1]*z))") ``` -"""=# +""" Base.:*(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :MUL) Base.:*(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :MUL) Base.:*(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = e2 * e1 -#= + """ a / b a / 1.0 @@ -358,9 +371,9 @@ Returns the `Real` division expression `a/b`. Note: `a` and `b` must be `Real`). a = Real(n, "a") b = Real(n, m, "b") a ./ b -println("typeof a/b: $(typeof(a[1]/b[1]))") +println("typeof a/b: \$(typeof(a[1]/b[1]))") ``` -"""=# +""" Base.:/(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :DIV) Base.:/(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :DIV) Base.:/(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :DIV) \ No newline at end of file