The Lean Language Reference

17.9. Linear Integer Arithmetic Solver

The linear integer arithmetic solver, cutsat, implements a model-based decision procedure for linear integer arithmetic, inspired by Section 4 of "Cutting to the Chase: Solving Linear Integer Arithmetic". The implementation in grind includes several enhancements and modifications such as

  • Extended constraint support (equality and disequality).

  • Optimized encoding of the Cooper-Left rule using a "big"-disjunction instead of fresh variables.

  • Decision variable tracking for case splits (disequalities, Cooper-Left, Cooper-Right).

The solver can process four categories of linear polynomial constraints (where p is a linear polynomial):

  1. Equality: p = 0

  2. Divisibility: d ∣ p

  3. Inequality: p ≤ 0

  4. Disequality: p ≠ 0

The procedure builds a model incrementally, resolving conflicts through constraint generation. For example, given a partial model {x := 1} and constraint 3 ∣ 3*y + x + 1:

  • The solve cannot extend the model to y because 3 ∣ 3*y + 2 is unsatisfiable.

  • Thus, it resolves the conflict by generating the implied constraint 3 ∣ x + 1.

  • The new constraint forces the solver to find a new assignment for x.

When assigning a variable y, the solver considers:

  • The best upper and lower bounds (inequalities).

  • A divisibility constraint.

  • All disequality constraints where y is the maximal variable.

The Cooper-Left and Cooper-Right rules handle the combination of inequalities and divisibility. For unsatisfiable disequalities p ≠ 0, the solver generates the case split: p + 1 ≤ 0 ∨ -p + 1 ≤ 0.

The following examples demonstrate goals that can be decide by cutsat.

example {x y : Int} : 2 * x + 4 * y ≠ 5 := x:Inty:Int⊢ 2 * x + 4 * y ≠ 5 All goals completed! 🐙 -- Mixing equalities and inequalities. example {x y : Int} : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := x:Inty:Int⊢ 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 All goals completed! 🐙 -- Linear divisibility constraints. example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2*a := a:Intb:Int⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬2 ∣ b + 2 * a All goals completed! 🐙

You can disable this solver using the option grind -cutsat.

example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2*a := a:Intb:Int⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬2 ∣ b + 2 * a `grind` failed case grind a b : Int h : 2 ∣ a + 1 h_1 : 2 ∣ a + b h_2 : 2 ∣ 2 * a + b ⊢ False [grind] Goal diagnostics [facts] Asserted facts [prop] 2 ∣ a + 1 [prop] 2 ∣ a + b [prop] 2 ∣ 2 * a + b [eqc] True propositions [prop] 2 ∣ a + b [prop] 2 ∣ a + 1 [prop] 2 ∣ 2 * a + b [linarith] Linarith assignment for `Int` [assign] a := 0 [assign] b := 0a:Intb:Int⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬2 ∣ b + 2 * a

The solver is complete for linear integer arithmetic. The following example has a rational solution, but does not have integer ones.

example {x y : Int} : 27 ≤ 13*x + 11*y → 13*x + 11*y ≤ 30 → -10 ≤ 9*x - 7*y → 9*x - 7*y > 4 := x:Inty:Int⊢ 27 ≤ 13 * x + 11 * y → 13 * x + 11 * y ≤ 30 → -10 ≤ 9 * x - 7 * y → 9 * x - 7 * y > 4 All goals completed! 🐙

The search can become vast with very few constraints, but cutsat was not designed to perform massive case-analysis. You can reduce the search space by instructing cutsat to accept rational solutions using the option grind +qlia.

example {x y : Int} : 27 ≤ 13*x + 11*y → 13*x + 11*y ≤ 30 → -10 ≤ 9*x - 7*y → 9*x - 7*y > 4 := x:Inty:Int⊢ 27 ≤ 13 * x + 11 * y → 13 * x + 11 * y ≤ 30 → -10 ≤ 9 * x - 7 * y → 9 * x - 7 * y > 4 `grind` failed case grind x y : Int h : -13 * x + -11 * y + 27 ≤ 0 h_1 : 13 * x + 11 * y + -30 ≤ 0 h_2 : -9 * x + 7 * y + -10 ≤ 0 h_3 : 9 * x + -7 * y + -4 ≤ 0 ⊢ False [grind] Goal diagnostics [facts] Asserted facts [prop] -13 * x + -11 * y + 27 ≤ 0 [prop] 13 * x + 11 * y + -30 ≤ 0 [prop] -9 * x + 7 * y + -10 ≤ 0 [prop] 9 * x + -7 * y + -4 ≤ 0 [eqc] True propositions [prop] -9 * x + 7 * y + -10 ≤ 0 [prop] -13 * x + -11 * y + 27 ≤ 0 [prop] 9 * x + -7 * y + -4 ≤ 0 [prop] 13 * x + 11 * y + -30 ≤ 0 [cutsat] Assignment satisfying linear constraints [assign] x := 62/117 [assign] y := 2x:Inty:Int⊢ 27 ≤ 13 * x + 11 * y → 13 * x + 11 * y ≤ 30 → -10 ≤ 9 * x - 7 * y → 9 * x - 7 * y > 4

In the example above, you can inspect the rational model constructed by cutsat by expanding the section "Assignment satisfying linear constraints" in the goal diagnostics.

The solver currently does not have support for nonlinear constraints, and treats nonlinear terms such as x*x as variables. Thus, it fails to solve the following goal. You can use the option trace.grind.cutsat.assert to trace all constraints processed by cutsat. Note that the term x*x is "quoted" in 「x * x」 + 1 ≤ 0 to indicate that x*x is treated as a variable.

example (x : Int) : x*x ≥ 0 := x:Int⊢ x * x ≥ 0 set_option trace.grind.cutsat.assert true in [grind.cutsat.assert] -1*「1」 + 1 = 0 [grind.cutsat.assert] -1*「x ^ 2 + 1」 + 「x ^ 2」 + 1 = 0 [grind.cutsat.assert] 「x ^ 2」 + 1 ≤ 0`grind` failed case grind x : Int h : x * x + 1 ≤ 0 ⊢ False [grind] Goal diagnostics [facts] Asserted facts [prop] x * x + 1 ≤ 0 [eqc] True propositions [prop] x * x + 1 ≤ 0 [cutsat] Assignment satisfying linear constraints [assign] x := 4 [assign] 「x ^ 2」 := -1x:Int⊢ x * x ≥ 0

The solver also implements model-based theory combination. This is a mechanism for propagating equalities back to the core module that might trigger new congruences.

example (f : Int → Int) (x y : Int) : f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0 := f:Int → Intx:Inty:Int⊢ f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0 All goals completed! 🐙

In the example above, the linear inequalities and disequalities imply y = 0, and consequently x = x + y, and f x = f (x + y) by congruence. Model-based theory combination increases the size of the search space, and you can disable it using the option grind -mbtc

example (f : Int → Int) (x y : Int) : f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0 := f:Int → Intx:Inty:Int⊢ f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0 `grind` failed case grind f : Int → Int x y : Int h : f x = 0 h_1 : -1 * y ≤ 0 h_2 : y + -1 ≤ 0 h_3 : ¬y = 1 h_4 : ¬f (x + y) = 0 ⊢ False [grind] Goal diagnostics [facts] Asserted facts [prop] f x = 0 [prop] -1 * y ≤ 0 [prop] y + -1 ≤ 0 [prop] ¬y = 1 [prop] ¬f (x + y) = 0 [eqc] True propositions [prop] y + -1 ≤ 0 [prop] -1 * y ≤ 0 [eqc] False propositions [prop] y = 1 [prop] f (x + y) = 0 [eqc] Equivalence classes [eqc] {f x, 0} [cutsat] Assignment satisfying linear constraints [assign] x := 0 [assign] y := 0 [assign] f x := 0 [assign] f (x + y) := 4 [ring] Ring `Int` [diseqs] Disequalities [_] ¬y + -1 = 0f:Int → Intx:Inty:Int⊢ f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0

The cutsat solver can also process linear constraints containing natural numbers. It converts them into integer constraints by using Int.ofNat.

example (x y z : Nat) : x < y + z → y + 1 < z → z + x < 3*z := x:Naty:Natz:Nat⊢ x < y + z → y + 1 < z → z + x < 3 * z All goals completed! 🐙

The solver also supports linear division and modulo operations.

example (x y : Int) : x = y / 2 → y % 2 = 0 → y - 2*x = 0 := x:Inty:Int⊢ x = y / 2 → y % 2 = 0 → y - 2 * x = 0 All goals completed! 🐙

The cutsat solver normalizes commutative (semi)ring expressions, so can solve goals like

example (a b : Nat) (h₁ : a + 1 ≠ a * b * a) (h₂ : a * a * b ≤ a + 1) : b * a^2 < a + 1 := a:Natb:Nath₁:a + 1 ≠ a * b * ah₂:a * a * b ≤ a + 1⊢ b * a ^ 2 < a + 1 All goals completed! 🐙

There is an extensible mechanism via the Lean.Grind.ToInt typeclass to tell cutsat that a type embeds in the integers. Using this, we can solve goals such as:

example (a b c : Fin 11) : a ≤ 2 → b ≤ 3 → c = a + b → c ≤ 5 := a:Fin 11b:Fin 11c:Fin 11⊢ a ≤ 2 → b ≤ 3 → c = a + b → c ≤ 5 All goals completed! 🐙 example (a : Fin 2) : a ≠ 0 → a ≠ 1 → False := a:Fin 2⊢ a ≠ 0 → a ≠ 1 → False All goals completed! 🐙 example (a b c : UInt64) : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := a:UInt64b:UInt64c:UInt64⊢ a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 All goals completed! 🐙

Planned future features: improved constraint propagation.