Have you ever faced a programming problem where you knew exactly what the solution should look like, but writing the algorithm to find it felt like a nightmare? Usually, we write imperative code: we tell the computer exactly how to find the answer, step by step. But what if we could just describe the rules of the problem and let the computer figure out the rest?
It's a bit similar to how we use Large Language Models (LLMs). Instead of writing an algorithm to parse and generate text, we just give the LLM a prompt that describes what we want, and it generates the text for us.
Z3 is perfect for problems that are well-defined and have clear constraints, like scheduling, optimization, or logical puzzles.
In this blog post, we'll explore how to use Z3 with Go to solve a variety of problems.
What is Z3? ¶
Z3 is an open-source theorem prover developed by Microsoft Research. More specifically, it's an SMT (Satisfiability Modulo Theories) solver.
You can think of Z3 as a highly advanced "magic box" for constraint satisfaction. You feed it a set of variables and rules (constraints), and Z3 will either:
- Give you a valid assignment for those variables that satisfies all the rules (a "Model").
- Tell you that it's mathematically impossible to satisfy the rules ("Unsatisfiable").
Under the hood, Z3 combines a SAT (Boolean Satisfiability) solver with specialized solvers for different "theories" like integers, real numbers, bit-vectors, and strings. This means it doesn't just blindly guess values; it uses advanced mathematical heuristics to prune the search space and find solutions incredibly fast.
What problems can I solve with Z3 and what are the limitations? ¶
Z3 excels at solving problems that can be expressed as a set of strict logical or mathematical constraints. This includes scheduling, resource allocation, package dependency resolution, and even verifying that software or security policies behave as expected.
However, Z3 is not a silver bullet. Because many of these constraint satisfaction problems are NP-hard, Z3's execution time can grow exponentially as the problem size increases. Additionally, Z3 requires problems to be perfectly well-defined—it cannot handle ambiguity, fuzzy logic, or open-ended creative tasks, which are better suited for machine learning models.
Setting up Z3 with Go ¶
While Z3 is written in C++, it has bindings for many languages, including Go. The official Go bindings are available at github.com/Z3Prover/z3/src/api/go.
Because the Go bindings rely on CGO to talk to the underlying C++ library, setting it up requires a bit of plumbing (like having a C compiler and the Z3 binaries available). Here is how you can set it up on different operating systems:
Windows ¶
On Windows, the easiest way to get CGO working with Z3 is to use a MinGW toolchain. In my local setup, I use llvm-mingw to compile the Go code and link it against the Z3 DLLs.
- Download the pre-compiled Z3 Windows release from the Z3 GitHub releases page.
- Download llvm-mingw.
- Unzip both and place them in any directory (e.g.,
C:\z3andC:\llvm). - When building your Go code, you'll need to set the following environment variables to point to your extracted Z3 and MinGW folders:
set CGO_ENABLED=1 set CGO_CFLAGS="-I/path/to/z3/include" set CGO_LDFLAGS="-L/path/to/z3/bin -lz3" set CC="/path/to/llvm-mingw/bin/gcc.exe" - You also need to ensure
libz3.dllis in the same directory as your compiled executable when running it.
Linux ¶
On Linux, setting up Z3 is usually as simple as installing it via your package manager. You will also need a C compiler like gcc installed for CGO to work.
For Ubuntu/Debian:
sudo apt-get update
sudo apt-get install build-essential libz3-dev
This installs gcc (via build-essential), the shared libraries, and the C headers required by CGO. You will also need to tell CGO where to find them by setting the following environment variables:
export CGO_ENABLED=1
export CGO_CFLAGS="-I/usr/include"
export CGO_LDFLAGS="-L/usr/lib/x86_64-linux-gnu -lz3"
You can then build your Go project normally with go build.
macOS ¶
On macOS, you can easily install Z3 using Homebrew:
brew install z3
Like on Linux, this will install the necessary headers and libraries:
export CGO_ENABLED=1
export CGO_CFLAGS="-I/opt/homebrew/include"
export CGO_LDFLAGS="-L/opt/homebrew/lib"
export LD_LIBRARY_PATH="/opt/homebrew/lib"
Make sure that the C/C++ toolchain is properly set up on your Mac.
xcode-select --install
You can then compile your Go code using go build.
Let's dive into some code and see how we can use Z3 to solve problems.
Core Concepts ¶
Before we look at the examples, here are the basic building blocks you'll use in a Z3 program:
- Context: The main environment. Everything you create (variables, formulas) belongs to a context.
- Solver: The engine that actually checks your constraints and finds solutions.
- Constants (Variables): The unknowns you want Z3 to find values for.
- Assertions: The rules or constraints you apply to your variables.
- Model: If the solver finds a solution, the model contains the concrete values assigned to your variables.
A Simple Example: Rabbits and Pheasants ¶
Let's start with a classic math puzzle:
"There are 9 heads and 24 legs in a cage. How many rabbits and how many pheasants are there?"
We know rabbits have 4 legs and pheasants have 2. We also know there are 9 animals in total.
With mathematical reasoning, we can set up the equations with two variables: rabbits and pheasants.
rabbits + pheasants = 9(total heads)4 * rabbits + 2 * pheasants = 24(total legs)rabbits >= 0(can't have negative rabbits)pheasants >= 0(can't have negative pheasants)
Instead of writing an algorithm to solve these equations, we express them as constraints in Z3 and let the solver find the solution. The following Go example shows the approach:
Create the context and solver
ctx := z3.NewContext()
solver := ctx.NewSolver()
example_rabbits_and_pheasants.go
Define the two variables to solve for: rabbits and pheasants. These are integer variables, so MkIntConst is used to create them.
rabbits := ctx.MkIntConst("rabbits")
pheasants := ctx.MkIntConst("pheasants")
example_rabbits_and_pheasants.go
Next, add the constraints. The first constraint is rabbits + pheasants = 9. MkAdd adds the two variables, and MkEq (equal to) asserts that their sum must equal 9.
solver.Assert(ctx.MkEq(ctx.MkAdd(rabbits, pheasants), ctx.MkInt(9, ctx.MkIntSort())))
example_rabbits_and_pheasants.go
The next constraint is 4 * rabbits + 2 * pheasants = 24. MkMul multiplies the variables by their leg counts, MkAdd sums them, and MkEq asserts that this sum must equal 24.
solver.Assert(ctx.MkEq(ctx.MkAdd(ctx.MkMul(ctx.MkInt(4, ctx.MkIntSort()), rabbits), ctx.MkMul(ctx.MkInt(2, ctx.MkIntSort()), pheasants)), ctx.MkInt(24, ctx.MkIntSort())))
example_rabbits_and_pheasants.go
The last two constraints ensure that neither rabbits nor pheasants can be negative. MkGe (greater than or equal to) is used for this.
solver.Assert(ctx.MkGe(rabbits, ctx.MkInt(0, ctx.MkIntSort())))
solver.Assert(ctx.MkGe(pheasants, ctx.MkInt(0, ctx.MkIntSort())))
example_rabbits_and_pheasants.go
Next, Z3 checks whether a model satisfies all constraints. If one exists, values can be extracted from the model.
if status := solver.Check(); status != z3.Satisfiable {
return fmt.Errorf("%s returned %s", "rabbits-and-pheasants", status.String())
}
example_rabbits_and_pheasants.go
The Check method returns a status of Satisfiable, Unsatisfiable, or Unknown. If it is Satisfiable, call Model() to get the model and evaluate the variables.
model := solver.Model()
rVal, rOk := model.Eval(rabbits, true)
if !rOk {
return fmt.Errorf("failed to evaluate %s", rabbits.String())
}
r, err := parseIntExpr(rVal.String())
if err != nil {
return err
}
pVal, pOk := model.Eval(pheasants, true)
if !pOk {
return fmt.Errorf("failed to evaluate %s", pheasants.String())
}
p, err := parseIntExpr(pVal.String())
if err != nil {
return err
}
fmt.Printf("Rabbits: %d, Pheasants: %d\n", r, p)
if r != 3 || p != 6 {
return fmt.Errorf("unexpected solution: rabbits=%d pheasants=%d", r, p)
}
example_rabbits_and_pheasants.go
When we run this, Z3 instantly tells us: Rabbits: 3, Pheasants: 6.
Notice how we didn't write any logic to solve the problem. We just translated formulas into Z3's API calls (MkAdd, MkEq, MkMul) and let the solver do the heavy lifting. Note that the Solver we use here is designed to find any model that satisfies the constraints. In more complex problems, we might want to find the best model according to some criteria, which is where Optimizer comes in (we'll see that in the next example).
Real-World Example: Package Dependency Resolution ¶
In this section, we take a look at a more complex, real-world problem: package dependency resolution. This is the problem that package managers like npm, pip, and go mod solve every day. These tools have to figure out which versions of which libraries to install so that nothing conflicts. This is a classic constraint satisfaction problem.
Let's say we have an app that depends on core@1.0 or core@2.0.
core@1.0requirestls@1.0.core@2.0requirestls@2.0.- We also have a
legacy-plugin@1.0that conflicts withtls@2.0.
We can model this in Z3 by treating each package version as a boolean variable (1 if installed, 0 if not). The following code does not use a boolean type directly, but instead uses integers constrained to be either 0 or 1.
In the previous example, we used a Solver to find any valid model. In this example, an Optimizer is used to find the best model according to certain criteria (prefer newer versions, minimize the number of installed packages). The Optimizer allows us to set optimization goals in addition to constraints.
The code first creates an integer variable for each package version. Each variable can be either 0 (not installed) or 1 (installed).
opt := ctx.NewOptimize()
app := ctx.MkIntConst("app_1_0")
core1 := ctx.MkIntConst("core_1_0")
core2 := ctx.MkIntConst("core_2_0")
tls1 := ctx.MkIntConst("tls_1_0")
tls2 := ctx.MkIntConst("tls_2_0")
legacyPlugin := ctx.MkIntConst("legacy_plugin_1_0")
The following constraints make sure that these variables can only be 0 or 1.
all := map[string]*z3.Expr{
"app@1.0": app,
"core@1.0": core1,
"core@2.0": core2,
"tls@1.0": tls1,
"tls@2.0": tls2,
"legacy-plugin@1.0": legacyPlugin,
}
printOrder := []string{"app@1.0", "core@1.0", "core@2.0", "tls@1.0", "tls@2.0", "legacy-plugin@1.0"}
for _, v := range all {
opt.Assert(ctx.MkGe(v, ctx.MkInt(0, ctx.MkIntSort())))
opt.Assert(ctx.MkLe(v, ctx.MkInt(1, ctx.MkIntSort())))
}
This constraint makes sure that the app has the value 1, meaning it must be installed.
opt.Assert(ctx.MkEq(app, ctx.MkInt(1, ctx.MkIntSort())))
This constraint ensures that only one version of core can be installed. The trick here is to add the values
of core1 and core2 together and assert that their sum must equal the value of app. Because app is always 1, this means that exactly one of core1 or core2 must be 1 (installed) and the other must be 0 (not installed). If both were 0, then the sum would be 0, which would not satisfy the constraint. If both were 1, then the sum would be 2, which also would not satisfy the constraint. Only one of them can be 1 to satisfy the equation.
opt.Assert(ctx.MkEq(ctx.MkAdd(core1, core2), app))
The next two constraints represent the dependency chains. If core1 is installed (equals 1), then tls1 must also be installed (equals 1). Similarly, if core2 is installed, then tls2 must be installed. MkImplies is used to express these implications (if this is true then that must also be true).
opt.Assert(ctx.MkImplies(ctx.MkEq(core1, ctx.MkInt(1, ctx.MkIntSort())), ctx.MkEq(tls1, ctx.MkInt(1, ctx.MkIntSort()))))
opt.Assert(ctx.MkImplies(ctx.MkEq(core2, ctx.MkInt(1, ctx.MkIntSort())), ctx.MkEq(tls2, ctx.MkInt(1, ctx.MkIntSort()))))
Next constraint ensures that only one TLS version can be installed at a time. The sum of tls1 and tls2 must be less than or equal to 1, meaning at most one of them can be 1 (installed).
opt.Assert(ctx.MkLe(ctx.MkAdd(tls1, tls2), ctx.MkInt(1, ctx.MkIntSort())))
Next line adds a constraint to ensure that the legacy-plugin cannot be installed at the same time as tls2. The sum of legacyPlugin and tls2 must be less than or equal to 1, meaning they cannot both be 1 (installed) at the same time.
opt.Assert(ctx.MkLe(ctx.MkAdd(legacyPlugin, tls2), ctx.MkInt(1, ctx.MkIntSort())))
The next code block sets up optimization goals. To prefer newer package versions, higher scores are assigned to core2 and tls2. Multiplying package variables by scores (100 for core2 and 50 for tls2) creates a scoring system where newer versions contribute more to the total score. Calling opt.Maximize(modernScore) tells Z3 to maximize that score. That means if there are multiple solutions Z3 will choose the one with the highest score, which corresponds to the newer package versions.
The total number of installed packages is also minimized by adding an optimization goal on the sum of all package variables. Summing these variables gives the package count. Calling opt.Minimize(installedCount) tells Z3 if it finds multiple solutions choose the one with fewer installed packages.
modernScore := ctx.MkAdd(
ctx.MkMul(core2, ctx.MkInt(100, ctx.MkIntSort())),
ctx.MkMul(tls2, ctx.MkInt(50, ctx.MkIntSort())),
)
installedCount := ctx.MkAdd(app, core1, core2, tls1, tls2, legacyPlugin)
bestModern := opt.Maximize(modernScore)
bestSmall := opt.Minimize(installedCount)
As in the previous example, Check() verifies whether a satisfying model (solution) exists. If one exists, the model shows which packages are installed.
if status := opt.Check(); status != z3.Satisfiable {
return fmt.Errorf("%s returned %s", "package-resolver-sat", status.String())
}
model := opt.Model()
if upper := opt.GetUpper(bestModern); upper != nil {
fmt.Printf(" modern-score: %s\n", upper.String())
}
if lower := opt.GetLower(bestSmall); lower != nil {
fmt.Printf(" installed-count: %s\n", lower.String())
}
fmt.Println(" selected packages:")
for _, name := range printOrder {
expr := all[name]
val, ok := model.Eval(expr, true)
if !ok {
return fmt.Errorf("failed to evaluate %s", name)
}
num, err := parseIntExpr(val.String())
if err != nil {
return err
}
if num == 1 {
fmt.Printf(" - %s\n", name)
}
}
This code will print the following output.
modern-score: 150
installed-count: 3
selected packages:
- app@1.0
- core@2.0
- tls@2.0
To see what happens when we install the legacy-plugin, add the following line to assert that legacyPlugin must be installed (equals 1).
opt.Assert(ctx.MkEq(legacyPlugin, ctx.MkInt(1, ctx.MkIntSort())))
Because the legacy-plugin conflicts with tls2, Z3 has to choose the older versions of core and tls to satisfy all constraints.
modern-score: 0
installed-count: 4
selected packages:
- app@1.0
- core@1.0
- tls@1.0
- legacy-plugin@1.0
Real-World Example: RBAC and Security Policies ¶
Another area where we can use Z3 is in verifying security policies. Imagine you have a complex Role-Based Access Control (RBAC) system. You want to know if a specific user can access a specific resource.
This example shows that Z3 not only works with numbers, but also with strings and even supports regular expressions.
Like in the previous examples, this code creates a context and solver, defines variables, and adds constraints. In this case, user_country, node_location, and node_running are string variables. A constant string fooapp represents the application checked for access.
The constraint then ensures that node_location must be equal (MkEq) to user_country and node_running must be equal to fooapp.
ctx := z3.NewContext()
strSort := ctx.MkStringSort()
userCountry := ctx.MkConst(ctx.MkStringSymbol("user_country"), strSort)
nodeLocation := ctx.MkConst(ctx.MkStringSymbol("node_location"), strSort)
nodeRunning := ctx.MkConst(ctx.MkStringSymbol("node_running"), strSort)
fooapp := ctx.MkString("fooapp")
policy := ctx.MkAnd(
ctx.MkEq(nodeLocation, userCountry),
ctx.MkEq(nodeRunning, fooapp),
)
solver := ctx.NewSolver()
solver.Assert(policy)
When a user tries to access the resource, the following constraints represent that user's role. In this example, the user is from Canada, the node is also in Canada, and the node is running fooapp.
solver.Assert(ctx.MkEq(userCountry, ctx.MkString("Canada")))
solver.Assert(ctx.MkEq(nodeLocation, ctx.MkString("Canada")))
solver.Assert(ctx.MkEq(nodeRunning, fooapp))
if solver.Check() == z3.Satisfiable {
fmt.Println("User 1: Access Allowed")
} else {
fmt.Println("User 1: Access Denied")
}
Because all constraints are satisfied, this code will print "User 1: Access Allowed".
Checking a user from Canada who runs the app on a node located in the USA makes Z3 unable to find a model because of the constraint that node_location must equal user_country. The program prints "User 2: Access Denied".
solver.Reset()
solver.Assert(policy)
solver.Assert(ctx.MkEq(userCountry, ctx.MkString("Canada")))
solver.Assert(ctx.MkEq(nodeLocation, ctx.MkString("USA")))
solver.Assert(ctx.MkEq(nodeRunning, fooapp))
if solver.Check() == z3.Satisfiable {
fmt.Println("User 2: Access Allowed")
} else {
fmt.Println("User 2: Access Denied")
}
Note that solver.Reset() removes all the constraints from the solver, therefore we need to re-add the policy constraint before checking the second user. This allows us to reuse the same solver instance for multiple checks.
The following code block uses Z3's regular-expression support to create a more complex policy. In this example, the policy allows access if the node is running fooapp and the node location starts with "us-east-" followed by 1 or more lowercase letters a to z. MkReConcat concatenates the fixed string "us-east-" with the regex [a-z]+. The policy is then tested against different node locations and running applications.
az := ctx.MkReRange(ctx.MkString("a"), ctx.MkString("z"))
locationRegex := ctx.MkReConcat(
ctx.MkToRe(ctx.MkString("us-east-")),
ctx.MkRePlus(az),
)
policy3 := ctx.MkAnd(
ctx.MkInRe(nodeLocation, locationRegex),
ctx.MkEq(nodeRunning, fooapp),
)
testCases := []struct{ loc, run string }{
{"us-east-virginia", "fooapp"},
{"us-west-oregon", "fooapp"},
{"us-east-123", "fooapp"}, // digits don't match [a-z]+
{"us-east-a", "fooapp"},
{"us-east-virginia", "barapp"},
}
for _, tc := range testCases {
solver := ctx.NewSolver()
solver.Assert(policy3)
solver.Assert(ctx.MkEq(nodeLocation, ctx.MkString(tc.loc)))
solver.Assert(ctx.MkEq(nodeRunning, ctx.MkString(tc.run)))
access := "Denied"
if solver.Check() == z3.Satisfiable {
access = "Allowed"
}
fmt.Printf(" location=%-20s running=%-8s => %s\n", tc.loc, tc.run, access)
}
Only the user with us-east-virginia and the user with us-east-a are allowed access because their node location matches the regular expression and they are running fooapp.
Real-World Example: Scheduling (Organize Your Day) ¶
Scheduling is another classic constraint problem. Imagine you have a list of tasks to complete in a day, each with a duration, and some tasks must happen before others.
Let's say we have four tasks:
- Work (4 hours)
- Mail (1 hour)
- Bank (2 hours)
- Shopping (1 hour)
We have some rules:
- All tasks must start after 9:00 and finish before 17:00.
- No two tasks can overlap.
- Work must start at or after 11:00.
- Mail must be finished before Work starts.
- Bank must be finished before Shopping starts.
As in the examples above, a complex scheduling algorithm is unnecessary when the rules are expressed directly as Z3 constraints.
ctx := z3.NewContext()
solver := ctx.NewSolver()
This example uses four integer variables representing task start times. Z3 assigns values to these variables to find a model that satisfies all constraints.
workStart := ctx.MkIntConst("work_start")
mailStart := ctx.MkIntConst("mail_start")
bankStart := ctx.MkIntConst("bank_start")
shoppingStart := ctx.MkIntConst("shopping_start")
The first constraints ensure that all tasks start after 9:00 and finish before 17:00. MkGe (greater than or equal to) ensures each start time is at least 9, and MkLe (less than or equal to) ensures each end time (start time plus duration via MkAdd) is at most 17.
tasks := []*z3.Expr{workStart, mailStart, bankStart, shoppingStart}
durations := []int64{4, 1, 2, 1}
names := []string{"work", "mail", "bank", "shopping"}
for i := range tasks {
solver.Assert(ctx.MkGe(tasks[i], ctx.MkInt(9, ctx.MkIntSort())))
solver.Assert(ctx.MkLe(ctx.MkAdd(tasks[i], ctx.MkInt64(durations[i], ctx.MkIntSort())), ctx.MkInt(17, ctx.MkIntSort())))
}
The next set of constraints ensures that no two tasks overlap. For each pair of tasks, either the first task must finish before the second starts, or the second task must finish before the first starts. This is expressed by comparing start times and durations with less-than-or-equal constraints.
for i := range tasks {
for j := i + 1; j < len(tasks); j++ {
left := ctx.MkLe(ctx.MkAdd(tasks[i], ctx.MkInt64(durations[i], ctx.MkIntSort())), tasks[j])
right := ctx.MkLe(ctx.MkAdd(tasks[j], ctx.MkInt64(durations[j], ctx.MkIntSort())), tasks[i])
solver.Assert(ctx.MkOr(left, right))
}
}
The next set of constraints implement the rules 3 to 5.
MkGe (greater than or equal to) ensures that workStart is at least 11, and MkLe ensures that mail ends before or at workStart and bank ends before or at shoppingStart.
solver.Assert(ctx.MkGe(workStart, ctx.MkInt(11, ctx.MkIntSort())))
solver.Assert(ctx.MkLe(ctx.MkAdd(mailStart, ctx.MkInt(1, ctx.MkIntSort())), workStart))
solver.Assert(ctx.MkLe(ctx.MkAdd(bankStart, ctx.MkInt(2, ctx.MkIntSort())), shoppingStart))
The code checks with solver.Check() if there is a valid model that satisfies all the constraints. If there is, the program extracts the model and prints out the schedule for each task, showing the start and end times.
if status := solver.Check(); status != z3.Satisfiable {
return fmt.Errorf("%s returned %s", "organize-your-day", status.String())
}
model := solver.Model()
fmt.Println("Schedule:")
for i := range tasks {
startVal, startOk := model.Eval(tasks[i], true)
if !startOk {
return fmt.Errorf("failed to evaluate %s", tasks[i].String())
}
start, err := parseIntExpr(startVal.String())
if err != nil {
return err
}
fmt.Printf(" %s: %d:00 - %d:00 (%d hour(s))\n", names[i], start, start+durations[i], durations[i])
}
return nil
With the constraints above, Z3 finds a model that satisfies all the constraints and prints out the following schedule:
Schedule:
work: 12:00 - 16:00 (4 hour(s))
mail: 9:00 - 10:00 (1 hour(s))
bank: 10:00 - 12:00 (2 hour(s))
shopping: 16:00 - 17:00 (1 hour(s))
Fun Puzzles: The Knapsack Problem ¶
To wrap things up, let's look at a classic optimization puzzle: the Knapsack Problem.
Imagine you are packing a backpack for a trip. The backpack has a maximum weight capacity, and you have a list of items you want to bring. Each item has a weight and a value (how much you want it). Your goal is to maximize the total value of the items you pack without exceeding the weight limit.
This is a classic dynamic programming problem, but with Z3, we can just describe the rules and ask it to find the optimal combination.
The following code defines a list of six items, each with a name, weight, and value. In the for loop, the application creates integer variables for each item with the name take_<item_name>. For each variable, the code adds two constraints to ensure that the value can only be 0 (not taken) or 1 (taken).
ctx := z3.NewContext()
opt := ctx.NewOptimize()
items := []struct {
name string
weight int64
value int64
}{
{"laptop", 3, 10},
{"camera", 2, 8},
{"phone", 1, 5},
{"book", 2, 3},
{"snacks", 1, 2},
{"headphones", 1, 4},
}
capacity := 6
take := make([]*z3.Expr, len(items))
for i := range items {
take[i] = ctx.MkIntConst("take_" + items[i].name)
opt.Assert(ctx.MkGe(take[i], ctx.MkInt(0, ctx.MkIntSort())))
opt.Assert(ctx.MkLe(take[i], ctx.MkInt(1, ctx.MkIntSort())))
}
The next block of code calculates total weight and total value based on the take variables. Each take[i] variable is multiplied by the corresponding item's weight and value, and the results are summed to get totalWeight and totalValue. If an item is not taken (take[i] = 0), it contributes 0. If an item is taken (take[i] = 1), it contributes its full weight and value.
weightTerms := make([]*z3.Expr, len(items))
valueTerms := make([]*z3.Expr, len(items))
for i := range items {
weightTerms[i] = ctx.MkMul(take[i], ctx.MkInt64(items[i].weight, ctx.MkIntSort()))
valueTerms[i] = ctx.MkMul(take[i], ctx.MkInt64(items[i].value, ctx.MkIntSort()))
}
totalWeight := ctx.MkAdd(weightTerms...)
totalValue := ctx.MkAdd(valueTerms...)
totalWeight is then constrained to be less than or equal to the backpack's capacity (6).
opt.Assert(ctx.MkLe(totalWeight, ctx.MkInt(capacity, ctx.MkIntSort())))
totalValue is used as the optimization objective. Calling opt.Maximize(totalValue) tells Z3 to choose the model with the highest total value if multiple models exist.
objective := opt.Maximize(totalValue)
As usual, the Check() returns if there a model that satisfies all the constraints. If there is, the application extracts the model and prints out the selected items.
if status := opt.Check(); status != z3.Satisfiable {
return fmt.Errorf("%s returned %s", "knapsack", status.String())
}
model := opt.Model()
if upper := opt.GetUpper(objective); upper != nil {
fmt.Printf("Maximum value: %s\n", upper.String())
}
usedWeight := int64(0)
fmt.Println("Selected items:")
for i := range items {
takeVal, takeOk := model.Eval(take[i], true)
if !takeOk {
return fmt.Errorf("failed to evaluate %s", take[i].String())
}
takeNum, err := parseIntExpr(takeVal.String())
if err != nil {
return err
}
if takeNum == 1 {
fmt.Printf(" %s (weight: %d, value: %d)\n", items[i].name, items[i].weight, items[i].value)
usedWeight += items[i].weight
}
}
fmt.Printf("Total weight: %d / %d\n", usedWeight, capacity)
Output:
Maximum value: 23
Selected items:
laptop (weight: 3, value: 10)
camera (weight: 2, value: 8)
phone (weight: 1, value: 5)
Total weight: 6 / 6
Multiple models (solutions) ¶
In the previous examples, we have seen that Z3 only returns one model that satisfies the constraints. With the Optimizer, we can get the optimal model according to our optimization goals, but what if we want to find all possible models that satisfy the constraints?
To find multiple models, we can use a loop to repeatedly call Check() and extract the model. After extracting a model, we can add a new constraint to the solver that excludes that specific model, and then call Check() again to find another model. We can repeat this process until Check() returns Unsatisfiable, which means there are no more models that satisfy the constraints.
You can find an example of this approach in the XKCD 287 example. This example models the puzzle from XKCD 287, where you have to select a combination of appetizers to reach a total of exactly $15.05.
After initializing the context, solver, variables, and constraints, the code enters an endless loop that checks for a satisfying model. If one exists, the model is extracted and printed. The loop then adds new constraints to block that specific model from being found again. This is done by creating a list of constraints that requires at least one variable to have a different value than in the current model. Adding these blocking constraints prevents Check() from returning the same model and allows enumeration of all appetizer combinations that total $15.05.
solutions := 0
for {
status := solver.Check()
if status == z3.Unsatisfiable {
break
}
if status != z3.Satisfiable {
return fmt.Errorf("%s returned %s", "xkcd287", status.String())
}
solutions++
model := solver.Model()
fmt.Printf("Solution %d:\n", solutions)
blocking := make([]*z3.Expr, 0, len(itemNames))
for i, name := range itemNames {
qtyVal, qtyOk := model.Eval(quantities[i], true)
if !qtyOk {
return fmt.Errorf("failed to evaluate %s", quantities[i].String())
}
qty, err := parseIntExpr(qtyVal.String())
if err != nil {
return err
}
if qty > 0 {
fmt.Printf(" %d x %s = $%.2f\n", qty, name, float64(qty)*float64(prices[i])/100.0)
}
blocking = append(blocking, ctx.MkNot(ctx.MkEq(quantities[i], ctx.MkInt64(qty, ctx.MkIntSort()))))
}
solver.Assert(ctx.MkOr(blocking...))
if solutions >= 10 {
fmt.Println("Stopping after 10 solutions")
break
}
}
Wrapping Up ¶
Z3 makes it possible to solve complex problems by simply describing the rules and constraints. This obviously only works for problems that can be expressed in a well-defined way, but for those problems, Z3 is an incredibly powerful tool.
To find more examples, check out the GitHub repository for this blog post. You'll find additional examples like solving the Einstein Riddle, the N-Queens problem, Sudoku, Magic Squares, Graph Coloring, and more.
To dig deeper into Z3 and its capabilities, I recommend checking out the official Z3 documentation.