🧩 Constraint Solving POTD:SMT — Scheduling Tasks with Mixed Boolean-Arithmetic Constraints

[github-actions[bot]]

Welcome to today's Constraint Solving Problem of the Day! Each post explores a different technique from the constraint solving and combinatorial optimisation world.

---

Problem Statement

Satisfiability Modulo Theories (SMT) extends Boolean SAT by attaching theory solvers that reason over richer domains — integers, reals, arrays, bit-vectors — while the SAT core handles the propositional skeleton. Today we explore a small but illuminating SMT instance: scheduling tasks with resource and timing constraints expressed as linear arithmetic over integers.

Concrete instance

We have 5 tasks T1 … T5, each with a duration d_i, and 2 machines. Each task must be assigned to exactly one machine, run without preemption, and no two tasks on the same machine may overlap. We also have a hard deadline: all tasks must finish by time D = 14.

Task	Duration
T1	3
T2	5
T3	2
T4	4
T5	3

Decision variables

• m_i ∈ {0, 1} — machine assignment for task i
• s_i ∈ ℤ, s_i ≥ 0 — start time for task i

Constraints

1. Deadline: s_i + d_i ≤ D for all i
2. No-overlap: for each pair (i, j) on the same machine, either s_i + d_i ≤ s_j or s_j + d_j ≤ s_i
3. Same-machine condition: pair (i, j) is co-located when m_i = m_j

Goal: find a satisfying assignment, or prove infeasibility.

---

Why It Matters

Software & hardware verification. SMT solvers (Z3, CVC5, Yices2) power bounded model checking, symbolic execution engines (KLEE, angr), and program synthesis tools. Timing and resource constraints map directly to linear arithmetic over integers.

Planning and scheduling under mixed constraints. Many real-world schedules mix Boolean control flow ("if task A runs on machine 1, then B must follow on machine 2") with linear arithmetic timing — a sweet spot for SMT.

Security analysis. Vulnerability scanners encode buffer offsets as bit-vector arithmetic and memory safety as Boolean reachability, then ask an SMT solver whether an exploit path exists.

---

Modelling Approaches

Approach 1 — Pure SMT (Linear Arithmetic + Booleans)

Encode the problem as a formula in QF_LIA (quantifier-free linear integer arithmetic) combined with Boolean connectives.

Element	Representation
Variables	s_i : Int, m_i : Bool
No-overlap	(m_i = m_j) ⟹ (s_i + d_i ≤ s_j ∨ s_j + d_j ≤ s_i)
Deadline	s_i + d_i ≤ D

Trade-offs: Very natural to express; the DPLL(T) architecture handles the Boolean structure while the LIA solver handles arithmetic. Works well for small-to-medium instances. The implication encoding requires case-splits that can blow up for dense instances.

Approach 2 — CP with Global no_overlap + Boolean Channeling

Model the same problem in a Constraint Programming solver using a global no_overlap (disjunctive) constraint.

Element	Representation
Variables	s_i ∈ 0..D, m_i ∈ {0,1}
No-overlap	`no_overlap([s_i
Channeling	m_i = 0 ↔ machine_of(i) = 0

Trade-offs: The no_overlap global constraint propagates via edge-finding and not-first/not-last rules, pruning far more aggressively than naïve SMT case-splits. CP is typically stronger here; SMT wins when the surrounding structure is highly propositional (e.g., large conditional dependency graphs).

Example Model (Z3 Python API)

from z3 import *

d = [3, 5, 2, 4, 3]   # durations
n = 5
D = 14                  # deadline

s = [Int(f's_{i}') for i in range(n)]
m = [Bool(f'm_{i}') for i in range(n)]  # True => machine 1

solver = Solver()

# Deadline and non-negativity
for i in range(n):
    solver.add(s[i] >= 0)
    solver.add(s[i] + d[i] <= D)

# No-overlap on same machine
for i in range(n):
    for j in range(i + 1, n):
        same = (m[i] == m[j])
        no_ov = Or(s[i] + d[i] <= s[j],
                   s[j] + d[j] <= s[i])
        solver.add(Implies(same, no_ov))

if solver.check() == sat:
    model = solver.model()
    for i in range(n):
        machine = 1 if is_true(model[m[i]]) else 0
        start   = model[s[i]].as_long()
        print(f"T{i+1}: machine={machine}, start={start}, end={start+d[i]}")
else:
    print("UNSAT")

---

Key Techniques

1. DPLL(T) — The SMT Architecture

The SAT solver (DPLL or CDCL) finds a propositionally consistent assignment; it then calls theory-specific T-solvers to check arithmetic/array/bit-vector consistency. Conflicts discovered by the T-solver are projected back to clauses, which are fed into the SAT core as theory lemmas (T-lemmas). This tight coupling between Boolean reasoning and domain reasoning is what makes SMT powerful.

2. Eager vs. Lazy Encoding of Disjunctions

The no-overlap constraint introduces a disjunction: s_i + d_i ≤ s_j ∨ s_j + d_j ≤ s_i. In eager encoding you introduce a selector Boolean b_ij and add both halves as conditional linear inequalities. In lazy mode the T-solver only instantiates clauses when needed. Lazy strategies dramatically reduce formula size for dense instances.

3. Symmetry Breaking

If all machines are identical, any permutation of machine assignments yields an equivalent solution. Add a lexicographic symmetry-breaking constraint such as m_1 = 0 (pin the first task to machine 0) to eliminate half the search space immediately.

---

Challenge Corner

Extension: Suppose each machine has a capacity (e.g., machine 0 can run at most 2 tasks simultaneously if they are splittable). How would you modify the SMT model to allow partial parallelism? Could you encode this with a single linear inequality per time step, or do you need auxiliary variables tracking the count of concurrent tasks?

Symmetry question: If you have k identical machines and n tasks, how many symmetry-breaking constraints are needed to eliminate all machine-permutation symmetries? What is the smallest set of constraints that achieves this?

---

References

1. Barrett, Clark, et al. "Satisfiability Modulo Theories." Handbook of Model Checking, Springer, 2018. — Authoritative survey of the DPLL(T) framework.
2. de Moura, L. & Bjørner, N. "Z3: An Efficient SMT Solver." TACAS 2008. — The paper behind the most widely-used SMT solver; highly readable.
3. Nieuwenhuis, R., Oliveras, A., & Tinelli, C. "Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T)." JACM 2006. — The theoretical foundation of modern SMT.
4. Rossi, F., van Beek, P., & Walsh, T. (eds.) Handbook of Constraint Programming, Elsevier, 2006 — Chapter 2 compares CP and SMT encodings for scheduling.

---

🔁 Yesterday's topic: Resource-Constrained Project Scheduling (RCPSP). Next time we'll look at another corner of the constraint solving world — stay tuned!

AI generated by Constraint Solving — Problem of the Day · history

• expires on Mar 31, 2026, 12:55 PM UTC

[github-actions[bot]]

This discussion has been marked as outdated by Constraint Solving — Problem of the Day.

A newer discussion is available at Discussion #22898.