## Maximal sum in a matrix

**Authors:** Jean-Christophe Filliâtre

**Topics:** Matrices

**Tools:** Why3

see also the index (by topic, by tool, by reference, by year)

(* Given a nxn matrix m of nonnegative integers, we want to pick up one element in each row and each column, so that their sum is maximal. We generalize the problem as follows: f(i,c) is the maximum for rows >= i and columns in set c. Thus the solution is f(0,{0,1,...,n-1}). f is easily defined recursively, as we have f(i,c) = max{j in c} m[i][j] + f(i+1, C\{j}) As such, it would still be a brute force approach (of complexity n!) but we can memoize f and then the search space decreases to 2^n-1. The following code implements such a solution. Sets of integers are provided in theory Bitset. Hash tables for memoization are provided in module HashTable (see file hash_tables.mlw for an implementation). Code for f is in module MaxMatrixMemo (mutually recursive functions maximum and memo). *) theory Bitset "sets of small integers" use import int.Int constant size : int (* elements belong to 0..size-1 *) type set (* membership [mem i s] can be implemented as [s land (1 lsl i) <> 0] *) predicate mem int set (* removal [remove i s] can be implemented as [s - (1 lsl i)] *) function remove int set : set axiom remove_def1: forall x y: int, s: set. mem x (remove y s) <-> x <> y /\ mem x s (* the set {0,1,...,n-1} [below n] can be implemented as [1 lsl n - 1] *) function below int : set axiom below_def: forall x n: int. 0 <= n <= size -> mem x (below n) <-> 0 <= x < n function cardinal set : int axiom cardinal_empty: forall s: set. cardinal s = 0 <-> (forall x: int. not (mem x s)) axiom cardinal_remove: forall x: int. forall s: set. mem x s -> cardinal s = 1 + cardinal (remove x s) axiom cardinal_below: forall n: int. 0 <= n <= size -> cardinal (below n) = if n >= 0 then n else 0 end module HashTable use import option.Option use import int.Int use import map.Map type t 'a 'b model { mutable contents: map 'a (option 'b) } function ([]) (h: t 'a 'b) (k: 'a) : option 'b = Map.get h.contents k val create (n:int) : t 'a 'b requires { 0 < n } ensures { forall k: 'a. result[k] = None } val clear (h: t 'a 'b) : unit writes {h} ensures { forall k: 'a. h[k] = None } val add (h: t 'a 'b) (k: 'a) (v: 'b) : unit writes {h} ensures { h[k] = Some v /\ forall k': 'a. k' <> k -> h[k'] = (old h)[k'] } exception Not_found val find (h: t 'a 'b) (k: 'a) : 'b ensures { h[k] = Some result } raises { Not_found -> h[k] = None } end module MaxMatrixMemo use import int.Int use import int.MinMax use import map.Map use map.Const use import ref.Ref constant n : int axiom n_nonneg: 0 <= n use import Bitset axiom integer_size: n <= size constant m : map int (map int int) axiom m_pos: forall i j: int. 0 <= i < n -> 0 <= j < n -> 0 <= m[i][j] predicate solution (s: map int int) (i: int) = (forall k: int. i <= k < n -> 0 <= s[k] < n) /\ (forall k1 k2: int. i <= k1 < k2 < n -> s[k1] <> s[k2]) predicate permutation (s: map int int) = solution s 0 type mapii = map int int function f (s: map int int) (i: int) : int = m[i][s[i]] clone import sum.Sum with type container = mapii, function f = f lemma sum_ind: forall i: int. i < n -> forall j: int. forall s: map int int. sum s[i <- j] i n = m[i][j] + sum s (i+1) n use import option.Option use HashTable as H type key = (int, set) type value = (int, mapii) predicate pre (k: key) = let (i, c) = k in 0 <= i <= n /\ cardinal c = n-i /\ (forall k: int. mem k c -> 0 <= k < n) predicate post (k: key) (v: value) = let (i, c) = k in let (r, sol) = v in 0 <= r /\ solution sol i /\ (forall k: int. i <= k < n -> mem sol[k] c) /\ r = sum sol i n /\ (forall s: map int int. solution s i -> (forall k: int. i <= k < n -> mem s[k] c) -> r >= sum s i n) type table = H.t key value val table: table predicate inv (t: table) = forall k: key, v: value. H.([]) t k = Some v -> post k v let rec maximum (i:int) (c: set) : (int, map int int) variant {2*n-2*i} requires { pre (i, c) /\ inv table } ensures { post (i,c) result /\ inv table } = if i = n then (0, Const.const 0) else begin let r = ref (-1) in let sol = ref (Const.const 0) in for j = 0 to n-1 do invariant { inv table /\ ( (!r = -1 /\ forall k: int. 0 <= k < j -> not (mem k c)) \/ (0 <= !r /\ solution !sol i /\ (forall k: int. i <= k < n -> mem !sol[k] c) /\ !r = sum !sol i n /\ (forall s: map int int. solution s i -> (forall k: int. i <= k < n -> mem s[k] c) -> mem s[i] c -> s[i] < j -> !r >= sum s i n))) } if mem j c then let (r', sol') = memo (i+1) (remove j c) in let x = m[i][j] + r' in if x > !r then begin r := x; sol := sol'[i <- j] end done; assert { 0 <= !r }; (!r, !sol) end with memo (i:int) (c: set) : (int, map int int) variant {2*n-2*i+1} requires { pre (i,c) /\ inv table } ensures { post (i,c) result /\ inv table } = try H.find table (i,c) with H.Not_found -> let r = maximum i c in H.add table (i,c) r; r end let maxmat () ensures { exists s: map int int. permutation s /\ result = sum s 0 n } ensures { forall s: map int int. permutation s -> result >= sum s 0 n } = H.clear table; assert { inv table }; let (r, _) = maximum 0 (below n) in r end

download ZIP archive

# Why3 Proof Results for Project "max_matrix"

## Theory "max_matrix.MaxMatrixMemo": fully verified in 0.15 s

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | Z3 (3.2) | |||

sum_ind | 0.15 | --- | --- | |||

2. VC for maximum | --- | --- | --- | |||

split_goal_wp | ||||||

1. postcondition | 0.02 | --- | --- | |||

2. assertion | 0.01 | --- | --- | |||

3. postcondition | 0.01 | --- | --- | |||

4. loop invariant init | 0.00 | --- | --- | |||

5. variant decrease | 0.02 | --- | --- | |||

6. precondition | 0.03 | --- | --- | |||

7. loop invariant preservation | --- | --- | --- | |||

split_goal_wp | ||||||

1. VC for maximum | 0.01 | --- | --- | |||

2. VC for maximum | --- | --- | 0.78 | |||

8. loop invariant preservation | --- | 4.41 | --- | |||

9. loop invariant preservation | 0.07 | --- | --- | |||

10. assertion | 0.01 | --- | --- | |||

11. postcondition | --- | 0.08 | --- | |||

3. VC for memo | --- | --- | --- | |||

split_goal_wp | ||||||

1. postcondition | --- | --- | --- | |||

split_goal_wp | ||||||

1. VC for memo | 0.02 | --- | --- | |||

2. VC for memo | 0.00 | --- | --- | |||

2. variant decrease | 0.01 | 0.01 | 0.02 | |||

3. precondition | 0.00 | --- | --- | |||

4. postcondition | 0.04 | --- | --- | |||

4. VC for maxmat | --- | --- | --- | |||

split_goal_wp | ||||||

1. assertion | 0.01 | --- | --- | |||

2. precondition | --- | --- | --- | |||

inline_goal | ||||||

1. precondition | --- | --- | --- | |||

split_goal_wp | ||||||

1. VC for maxmat | 0.00 | --- | --- | |||

2. VC for maxmat | 0.01 | --- | --- | |||

3. VC for maxmat | 0.01 | --- | --- | |||

4. VC for maxmat | 0.01 | --- | --- | |||

5. VC for maxmat | 0.00 | --- | --- | |||

6. VC for maxmat | 0.01 | --- | --- | |||

3. postcondition | --- | --- | --- | |||

split_goal_wp | ||||||

1. postcondition | --- | --- | --- | |||

inline_goal | ||||||

1. postcondition | 0.10 | --- | --- | |||

4. postcondition | --- | --- | --- | |||

inline_goal | ||||||

1. postcondition | 0.01 | --- | --- |