Advanced Topics

Difference Logic

By default, Z3 uses dual Simplex to solve feasibility, and primal Simplex for optimality. For arithmetical constraints that only have differences between variables, known as difference logic, Z3 contains alternative decision procedures tuned for this domain. These have to be configured explicitly. There is a choice between a solver tuned for sparse constraints (where the ratio of variables is high compared to number of inequalities) and a solver tuned for dense constraints.

Weighted Max-SAT solvers, a portfolio

The default solver for MaxSAT problems is the MaxRes algorithm. Several alternative solvers are available. The default solver is chosen based on benchmarking against MaxSAT competition benchmarks, but other solver combinations, such as wmax, may work well for some domains. When the objectives have weights such as 1, 2, 4, 8, 16, such that the sum of weights in every prefix is lower than the next weight, the solver uses a lexicographic optimization algorithm that attempts to first solve for the highest weight before continuing with lower weights.

The other main MaxSAT algorithms available are

Pre-processing within the optimization solver will attempt to eliminate bounded arithmetical variables. For example, the constraints

are rewritten internally to a problem of the form

You can disable this transformation by setting

For problems that are already bit-vector or Boolean, or can be rewritten to this form, the engine uses a core solver based on a tuned SAT solver. You can turn off the use of the SAT solver by setting: