17.6. Linear Integer Arithmetic🔗

The linear integer arithmetic solver, cutsat, implements a model-based decision procedure for linear integer arithmetic. The solver can process four categories of linear polynomial constraints (where p is a linear polynomial):

Equality: p = 0
Divisibility: d ∣ p
Inequality: p ≤ 0
Disequality: p ≠ 0

It is complete for linear integer arithmetic, and natural numbers are supported by converting them to integers with Int.ofNat. Support for additional types that can be embedded into Int can be added via instances of Lean.Grind.ToInt. Nonlinear terms (e.g. x * x) are allowed, and are represented as variables. The solver is additionally capable of propagating information back to the metaphorical grind whiteboard, which can trigger further progress from the other subsystems.

Examples of cutsat

All of these statements can be proved using cutsat. In the first example, the left-hand side must be a multiple of 2, and thus cannot be 5:

example {x y : Int} : 2 * x + 4 * y ≠ 5 := byx:Inty:Int⊢ 2 * x + 4 * y ≠ 5
  grindAll goals completed! 🐙

The solver supports mixing equalities and inequalities:

example {x y : Int} :
    2 * x + 3 * y = 0 →
    1 ≤ x →
    y < 1 := byx:Inty:Int⊢ 2 * x + 3 * y = 0 → 1 ≤ x → y < 1
  grindAll goals completed! 🐙

It also supports linear divisibility constraints:

example (a b : Int) :
    2 ∣ a + 1 →
    2 ∣ b + a →
    ¬ 2 ∣ b + 2 * a := bya:Intb:Int⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬2 ∣ b + 2 * a
  grindAll goals completed! 🐙

Without cutsat, grind cannot prove the statement:

example (a b : Int) :
    2 ∣ a + 1 →
    2 ∣ b + a →
    ¬ 2 ∣ b + 2 * a := bya:Intb:Int⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬2 ∣ b + 2 * a
  `grind` failed
grinda b:Inth:2 ∣ a + 1h_1:2 ∣ a + bh_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 := 0
grind -cutsata:Intb:Int⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬2 ∣ b + 2 * a

`grind` failed
grinda b:Inth:2 ∣ a + 1h_1:2 ∣ a + bh_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 := 0

17.6.1. Rational Solutions🔗

The solver is complete for linear integer arithmetic. However, the search can become vast with very few constraints, but cutsat was not designed to perform massive case-analysis. The qlia option to grind reduces the search space by instructing cutsat to accept rational solutions. With this option, cutsat is likely to be faster, but it is incomplete.

Rational Solutions

The following example has a rational solution, but does not have integer solutions:

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

Because it uses the rational solution, grind fails to refute the negation of the goal when +qlia is specified:

example {x y : Int} :
    27 ≤ 13 * x + 11 * y →
    13 * x + 11 * y ≤ 30 →
    -10 ≤ 9 * x - 7 * y →
    9 * x - 7 * y > 4 := byx:Inty:Int⊢ 27 ≤ 13 * x + 11 * y → 13 * x + 11 * y ≤ 30 → -10 ≤ 9 * x - 7 * y → 9 * x - 7 * y > 4
  `grind` failed
grindx y:Inth:-13 * x + -11 * y + 27 ≤ 0h_1:13 * x + 11 * y + -30 ≤ 0h_2:-9 * x + 7 * y + -10 ≤ 0h_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 := 2
grind +qliax:Inty:Int⊢ 27 ≤ 13 * x + 11 * y → 13 * x + 11 * y ≤ 30 → -10 ≤ 9 * x - 7 * y → 9 * x - 7 * y > 4

`grind` failed
grindx y:Inth:-13 * x + -11 * y + 27 ≤ 0h_1:13 * x + 11 * y + -30 ≤ 0h_2:-9 * x + 7 * y + -10 ≤ 0h_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 := 2

The rational model constructed by cutsat is in the section Assignment satisfying linear constraints in the goal diagnostics.

17.6.2. Nonlinear Constraints

The solver currently does support nonlinear constraints, and treats nonlinear terms such as x * x as variables.

Nonlinear Terms

cutsat fails to prove this theorem:

example (x : Int) : x * x ≥ 0 := byx:Int⊢ x * x ≥ 0
  `grind` failed
grindx:Inth: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」 := -1
grindx:Int⊢ x * x ≥ 0

`grind` failed
grindx:Inth: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」 := -1

From the perspective of cutsat, it is equivalent to:

example {y : Int} (x : Int) : y ≥ 0 := byy:Intx:Int⊢ y ≥ 0
  `grind` failed
grindy x:Inth:y + 1 ≤ 0⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] y + 1 ≤ 0
[eqc] True propositions
[prop] y + 1 ≤ 0
[cutsat] Assignment satisfying linear constraints
[assign] y := -1
grindy:Intx:Int⊢ y ≥ 0

`grind` failed
grindx:Inth: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」 := -1

This can be seen by setting the option trace.grind.cutsat.assert to true, which traces all constraints processed by cutsat.

example (x : Int) : x*x ≥ 0 := byx:Int⊢ x * x ≥ 0
  set_option trace.grind.cutsat.assert true in
  [grind.cutsat.assert] -1*「x ^ 2 + 1」 + 「x ^ 2」 + 1 = 0[grind.cutsat.assert] 「x ^ 2」 + 1 ≤ 0`grind` failed
grindx:Inth: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」 := -1
grindx:Int⊢ x * x ≥ 0

[grind.cutsat.assert] -1*「x ^ 2 + 1」 + 「x ^ 2」 + 1 = 0[grind.cutsat.assert] 「x ^ 2」 + 1 ≤ 0

The term x ^ 2 is “quoted” in 「x ^ 2」 + 1 ≤ 0 to indicate that x ^ 2 is treated as a variable.

17.6.3. Division and Modulus

The solver supports linear division and modulo operations.

Linear Division and Modulo with cutsat

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

17.6.4. Algebraic Processing

The cutsat solver normalizes commutative (semi)ring expressions.

Commutative (Semi)ring Normalization

Commutative ring normalization allows this goal to be solved:

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

17.6.5. Propagating Information🔗

The solver also implements model-based theory combination, which is a mechanism for propagating equalities back to the metaphorical shared whiteboard. These additional equalities may in turn trigger new congruences. Model-based theory combination increases the size of the search space; it can be disabled using the option grind -mbtc.

Propagating Equalities

In the example above, the linear inequalities and disequalities imply y = 0:

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

Consequently x = x + y, so f x = f (x + y) by congruence. Without model-based theory combination, the proof gets stuck:

example (f : Int → Int) (x y : Int) :
    f x = 0 →
    0 ≤ y → y ≤ 1 → y ≠ 1 →
    f (x + y) = 0 := byf:Int → Intx:Inty:Int⊢ f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0
  `grind` failed
grindf:Int → Intx y:Inth:f x = 0h_1:-1 * y ≤ 0h_2:y + -1 ≤ 0h_3:¬y = 1h_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 = 0
grind -mbtcf:Int → Intx:Inty:Int⊢ f x = 0 → 0 ≤ y → y ≤ 1 → y ≠ 1 → f (x + y) = 0

`grind` failed
grindf:Int → Intx y:Inth:f x = 0h_1:-1 * y ≤ 0h_2:y + -1 ≤ 0h_3:¬y = 1h_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 = 0

17.6.6. Other Types🔗

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

Natural Numbers with cutsat

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

There is an extensible mechanism via the Lean.Grind.ToInt type class 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 := bya:Fin 11b:Fin 11c:Fin 11⊢ a ≤ 2 → b ≤ 3 → c = a + b → c ≤ 5
  grindAll goals completed! 🐙

example (a : Fin 2) : a ≠ 0 → a ≠ 1 → False := bya:Fin 2⊢ a ≠ 0 → a ≠ 1 → False
  grindAll goals completed! 🐙

example (a b c : UInt64) : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := bya:UInt64b:UInt64c:UInt64⊢ a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5
  grindAll goals completed! 🐙

type class

Lean.Grind.ToInt.{u} (α : Type u)
  (range : outParam Lean.Grind.IntInterval) : Type u
Lean.Grind.ToInt.{u} (α : Type u)
  (range :
    outParam Lean.Grind.IntInterval) :
  Type u

ToInt α I asserts that α can be embedded faithfully into an interval I in the integers.

Instance Constructor

Lean.Grind.ToInt.mk.{u}

Methods

toInt : α → Int

The embedding function.

toInt_inj : ∀ (x y : α), ↑x = ↑y → x = y

The embedding function is injective.

toInt_mem : ∀ (x : α), ↑x ∈ range

The embedding function lands in the interval.

inductive type

Lean.Grind.IntInterval : Type
Lean.Grind.IntInterval : Type

An interval in the integers (either finite, half-infinite, or infinite).

Constructors

co (lo hi : Int) : Lean.Grind.IntInterval

The finite interval [lo, hi).

ci (lo : Int) : Lean.Grind.IntInterval

The half-infinite interval [lo, ∞).

io (hi : Int) : Lean.Grind.IntInterval

The half-infinite interval (-∞, hi).

ii : Lean.Grind.IntInterval

The infinite interval (-∞, ∞).

17.6.7. Implementation Notes

The implementation of cutsat is inspired by Section 4 of Jovanović and de Moura (2023)Dejan Jovanović and Leonardo de Moura, 2023. “Cutting to the Chase: Solving Linear Integer Arithmetic”. In Automated Deduction: CADE '23. (LNCS 6803). Compared to the paper, it includes several enhancements and modifications such as:

extended constraint support (equality and disequality),
an optimized encoding of the Cooper-Left rule using a “big”-disjunction instead of fresh variables, and
decision variable tracking for case splits (disequalities, Cooper-Left, Cooper-Right).

The cutsat procedure builds a model (that is, an assignment of the variables in the term) incrementally, resolving conflicts through constraint generation. For example, given a partial model {x := 1} and constraint 3 ∣ 3 * y + x + 1:

The solver 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.