Solving Scheduling With Z3 from Rust
A translation of a Z3 example from Python to Rust
This post is a translation of a Z3 example from Python to Rust. It is not very inspired: Please read the original Python article 1 for more background. However, at the bottom of this page, I provide a few more links and resources with a few notes.
The Z3 crate does not have any examples, so it makes it a bit tough to get started. I found one article that explains how to use Z3 for scheduling tasks in Python.
Result
Here’s the result of running the scheduler. The goal is to minimize the total time taken for the tasks. Each row has to be done in order (t1, t2, t3, then t4). And tasks of the same color cannot be scheduled at the same time.
Table of Python to RustPython | Rust | |
---|---|---|
Initialization | opt = Optimize() |
let cfg = Config::new(); let ctx = Context::new(&cfg); let opt = Optimize::new(&ctx); |
opt.add(tx[i] + task_length[i] <= tx[j]) |
opt.assert(&(&tasks[&i] + &task_length[&i]).le(&tasks[&j])); |
|
Operators | a < b 🙂 |
a.lt(&b) 😕 2 |
If | If(a, b, c) |
a.ite(b, c) |
The Translation
I’ve kept the code as close to possible as to the original Python. Personally, I
would make few simplifications, like using itertools::choose
function to get
all combinations of the color groupings.
use std::collections::BTreeMap;
use z3::ast::Bool;
use z3::*;
fn main() {
// Python: opt = Optimize()
let cfg = Config::new();
let ctx = Context::new(&cfg);
let opt = Optimize::new(&ctx);
let task_length: BTreeMap<i32, u64> = BTreeMap::from([
(1, 20),
(2, 50),
(3, 80),
(4, 50),
(5, 60),
(6, 45),
(7, 20),
(8, 25),
(9, 50),
(10, 30),
(11, 40),
(12, 50),
]);
// tasks = {k: Int("t{}".format(k)) for k in task_length.keys()}
let tasks: BTreeMap<_, _> = task_length
.keys()
.map(|k| (k, ast::Int::new_const(&ctx, format!("t{}", k))))
.collect();
// opt.add(And([t >= 0 for t in tasks.values()]))
let zero = ast::Int::from_u64(&ctx, 0);
for t in tasks.values() {
opt.assert(&t.ge(&zero));
}
// tend = Int("tend")
let tend = ast::Int::new_const(&ctx, "tend");
let edges = [
(1, 2),
(2, 3),
(3, 4),
(5, 6),
(6, 7),
(7, 8),
(9, 10),
(10, 11),
(11, 12),
];
for (i, j) in edges {
opt.assert(&(&tasks[&i] + task_length[&i]).le(&tasks[&j]));
}
let ends = [4, 8, 12];
for i in ends {
opt.assert(&(&tasks[&i] + task_length[&i]).le(&tend));
}
// Coloring restrictions
let add_related_constraint = |a, b| {
let bo = Bool::new_const(&ctx, format!("b{},{}", a, b));
opt.assert(&bo.ite(
&(&tasks[&a] + task_length[&a]).le(&tasks[&b]),
&(&tasks[&b] + task_length[&b]).le(&tasks[&a]),
));
};
add_related_constraint(1, 5);
add_related_constraint(5, 11);
add_related_constraint(1, 11);
add_related_constraint(2, 7);
add_related_constraint(7, 9);
add_related_constraint(2, 9);
add_related_constraint(3, 8);
add_related_constraint(8, 10);
add_related_constraint(3, 10);
add_related_constraint(4, 6);
add_related_constraint(6, 12);
add_related_constraint(4, 12);
// opt.minimize(tend)
opt.minimize(&tend);
assert_eq!(opt.check(&[]), SatResult::Sat);
// m = opt.model()
let m = opt.get_model().unwrap();
for i in task_length.keys() {
println!("{} {}", tasks[i], &m.eval(&tasks[i], true).unwrap());
}
println!("{} {}", tend, m.eval(&tend, true).unwrap());
}
Notes
- My z3 version:
z3 = {version="0.11.2", features = ["static-link-z3"]}
Further Reading
- The documentation of the high level
z3
crate. - It is helpful but not sufficient for beginners. (I’m a beginner.)
- Scheduling and SAT by Emmanuel Hebrard of LAAS-CNRS, Toulouse
- Explanations!
- Graphs and in-detail example exactly the same as in the code in my post.
https://sat-smt.codes/SAT_SMT_by_example.pdf
- A good explanation
https://github.com/alex-chew/z3d-rs
- Has examples
- Last commit 3 years ago
- Uses
z3
crate but adds macros on top. - You can write:
opt.assert(&exp!((num >= 0) & (num <= 9) in ctx));
. i.e. you can usex > y
etc instead ofx.gt(&y)
. - Does not work on Rust stable due to the usage features box_patterns and proc_macro_hygiene.
- Extremely slow to compile.
https://github.com/prove-rs/z3.rs/tree/master/z3/tests
- Tests serve as examples
https://fitzgeraldnick.com/2020/01/13/synthesizing-loop-free-programs.html
- Links to this: https://github.com/fitzgen/synth-loop-free-prog
https://cprimozic.net/blog/a-rusty-aoc/#day-23-using-the-z3-smt-solver
- Example code (not complete)
- Great descriptions and explanations, not too long.
- Got code from here (which is complete): https://gitlab.com/KonradBorowski/advent-of-code-2018/blob/master/src/day23/mod.rs
https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- Examples in Python
- See my table of Python to Rust for help in translating.
https://github.com/prove-rs/z3.rs/issues/151
- A GitHub ticket with a request for more examples
- Links to further resources