Solving Scheduling With Z3 from Rust

May 19, 2022

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 Rust

	Python	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"]}

Solving Scheduling With Z3 from Rust

A translation of a Z3 example from Python to Rust

Result

The Translation

Notes

Further Reading