Updated documentation with Real and Int, job shop example md and general

wording updates. Added an FAQ page.

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
 

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"
+        ],
     ]
 )

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
+```

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
 

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!
+

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)
+```

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.
 

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))")
+```
+
+

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))")
+if status == :SAT
+    println("t1 = $(value(t1))")
+    println("t2 = $(value(t2))")
+end

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