Solving a large number of very simple queries with minimal latency

[jonathan-laurent]

I am using Z3 on a workload where I have to solve a large number of very simple SAT queries (only a handful of clauses) as fast as possible. To figure out the best way to do it using the Z3 API, I generated a simple benchmark of queries such as:

And(x <= y, x >= 9, y <= 8)
And(y >= -2, y <= -4)
And(y <= 1, z <= y, z >= 8)
And(y <= -7, y >= 1)
And(x <= z, x >= 10, z <= 1)
And(z >= 8, z <= 1)
...

Then, I compared several uses of the Z3 API:

# ...


def sat_reset(make_solver):
    solver = make_solver()
    for fml in BENCHMARK:
        solver.reset()
        solver.add(fml)
        assert solver.check() == z3.unsat


def sat_push_pop(make_solver):
    solver = make_solver()
    for fml in BENCHMARK:
        solver.push()
        solver.add(fml)
        assert solver.check() == z3.unsat
        solver.pop()


# ...


benchmark_method(lambda: sat_reset(z3.Solver), "Solver")
benchmark_method(lambda: sat_reset(z3.SimpleSolver), "SimpleSolver")
benchmark_method(lambda: sat_reset(z3.Tactic('smt').solver), "SMT Tactic")
benchmark_method(lambda: sat_push_pop(z3.Solver), "Incremental")

Results:

Solver               6448us
SimpleSolver          259us
Tactic                182us
Incremental            77us

Full benchmark code

import z3
import random
import timeit


BENCH_SIZE = 1000


#####
## Prepare the benchmark
#####


VARS = [*z3.Ints("x y z")]


def is_unsat(fml):
    solver = z3.SimpleSolver()
    solver.add(fml)
    res = solver.check()
    return res == z3.unsat


def random_const():
    return random.choice(list(range(-10, 10 + 1)))


def random_var():
    return random.choice(VARS)


def random_formula():
    typ = random.choice(["comp", "lb", "ub"])
    if typ == "comp":
        while True:
            x = random_var()
            y = random_var()
            if str(x) != str(y):
                break
        return x <= y
    elif typ == "lb":
        return random_var() <= random_const()
    elif typ == "ub":
        return random_var() >= random_const()
    else:
        assert False


def random_unsat_problem():
    clauses = []
    while not is_unsat(z3.And(*clauses)):
        clauses.append(random_formula())
    minimal = False
    while not minimal:
        clauses, minimal = find_smaller_unsat(clauses)
    return z3.And(*clauses)


def find_smaller_unsat(clauses):
    for i in range(len(clauses)):
        sub = clauses[:i] + clauses[i + 1 :]
        if is_unsat(sub):
            return sub, False
    return clauses, True


BENCHMARK = [random_unsat_problem() for _ in range(BENCH_SIZE)]


#####
## Solving methods
#####


def sat_reset(make_solver):
    solver = make_solver()
    for fml in BENCHMARK:
        solver.reset()
        solver.add(fml)
        assert solver.check() == z3.unsat


def sat_push_pop(make_solver):
    solver = make_solver()
    for fml in BENCHMARK:
        solver.push()
        solver.add(fml)
        assert solver.check() == z3.unsat
        solver.pop()


#####
## Running the benchmark
#####


def benchmark_method(f, label):
    t = timeit.Timer(f).timeit(1) / BENCH_SIZE
    print(f"{label:20s} {t*1e6:4.0f}us")


print(f"Random benchmark of size {BENCH_SIZE}:")
for i in range(6):
    print(BENCHMARK[i])
print("...")
print("")


benchmark_method(lambda: sat_reset(z3.Solver), "Solver")
benchmark_method(lambda: sat_reset(z3.SimpleSolver), "SimpleSolver")
benchmark_method(lambda: sat_reset(z3.Tactic('smt').solver), "SMT Tactic")
benchmark_method(lambda: sat_push_pop(z3.Solver), "Incremental")

My questions:

1. I am surprised to see the incremental solver performing significantly better, especially since I am only using push and pop to implement a resetting behavior. Do you have any idea why this is the case?
2. Do you have any other tip about solving very simple queries as fast as possible using the Z3 API (in Python or in other languages)?

Also, given the large discrepancy between Solver and SimpleSolver on this benchmark, I am wondering whether more discussion about this should be warranted in the documentation / tutorials.

[Jupiter-19]

I simplify your question:

import z3
import timeit

x = z3.Bool('x')
BENCH_SIZE = 1000

def sat_reset(make_solver):
    solver = make_solver()
    for _ in range(BENCH_SIZE):
        solver.reset()
        solver.add(x)

def sat_push_pop(make_solver):
    solver = make_solver()
    for _ in range(BENCH_SIZE):
        solver.push()
        solver.add(x)
        solver.pop()

def benchmark_method(f, label):
    t = timeit.Timer(f).timeit(1) / BENCH_SIZE
    print(f"{label:20s} {t*1e6:4.0f}us")
    
benchmark_method(lambda: sat_reset(z3.Solver), "Solver")
benchmark_method(lambda: sat_push_pop(z3.Solver), "Incremental1")
benchmark_method(lambda: sat_reset(z3.SimpleSolver), "SimpleSolver")
benchmark_method(lambda: sat_push_pop(z3.SimpleSolver), "Incremental2")

Result:

Solver               6163us
Incremental1           47us
SimpleSolver          186us
Incremental2           40us

It looks like the problem isn't with the Solver, but with the reset .

[jonathan-laurent]

It seems that the problem is with reset indeed.
I also ran a benchmark using the OCaml API, which enables passing assumptions to the Solver.check function directly without adding them to the solver state.

OCaml benchmark:

open Z3
open Z3.Arithmetic

let is_unsat = function
  | Solver.UNSATISFIABLE -> true
  | _ -> false

let bench () =
  let ctx = mk_context [("model", "false"); ("proof", "false")] in
  let real = Real.mk_sort ctx in
  let x = Expr.mk_const ctx (Symbol.mk_string ctx "x") real in
  let zero = Real.mk_numeral_i ctx 0 in
  let one = Real.mk_numeral_i ctx 1 in
  let fml = Boolean.mk_implies ctx (mk_gt ctx x one) (mk_gt ctx x zero) in
  let fml_neg = Boolean.mk_not ctx fml in
  let solver = Solver.mk_simple_solver ctx in
  let check () = begin
    assert (Solver.get_num_assertions solver = 0);
    assert (is_unsat (Solver.check solver [fml_neg]));
  end in
  let check_reset () = begin
    Solver.add solver [fml_neg];
    assert (is_unsat (Solver.check solver []));
    Solver.reset solver;
  end in
  let check_push_pop () = begin
    Solver.push solver;
    Solver.add solver [fml_neg];
    assert (is_unsat (Solver.check solver []));
    Solver.pop solver 1;
  end in
  let open Core_bench in
  let benchs = [
    Bench.Test.create ~name:"Check" check;
    Bench.Test.create ~name:"Reset" check_reset;
    Bench.Test.create ~name:"Push-pop" check_push_pop
  ] in
  benchs |> Bench.make_command |> Core.Command.run

let () = bench ()

Output:

┌──────────┬──────────┬─────────┬────────────┐
│ Name     │ Time/Run │ mWd/Run │ Percentage │
├──────────┼──────────┼─────────┼────────────┤
│ Check    │  31.32us │  16.00w │     16.54% │
│ Reset    │ 189.33us │  17.00w │    100.00% │
│ Push-pop │  25.37us │  20.00w │     13.40% │
└──────────┴──────────┴─────────┴────────────┘