Declare matrix with unknown size in Z3

Question

I am aware that I can declare a matrix of z3.Real in Z3 by declaring its elements individually (maybe through list comprehension). Is there a way to represent a matrix with unknown size?

For example, consider the following example: In image filtering, given an image I of size [X,Y] and a filter kernel K of size [M,N], the convolution between the image I and the filter kernel K is I*K. I would like Z3 to prove (or disprove) that there exists filter F1 and F2 of any size, such that I*K == I*F1*F2.

The problem itself is totally made up and probably doesn't make sense. The idea is whether I can ask Z3 to find a matrix of unknown size such that the matrix satisfy certain property that can be expressed by linear function. Thanks!

Answer 1

Z3 supports simply typed first-order logic specifications. In a sense, the first question is how you would express your properties of interest in logic. For bounded size models you can instantiate sizes X,Y, M, N and express the counter-example queries for a suitable finite domain. If you want parametric sizes, you would express the behavior of * as a ternary relation. E.g., you can use functions I, K, I_K that take two arguments and express how I_K(x,y) relates to entries in I, K. You will then face issues such as proofs really require induction. Environments with good support for interaction, such as Lean, PVS, Coq, Isabelle, or environments, such as Dafny, are more suitable for setting up proofs.

Answer 2

Nikolaj's answer seems to hit the nail on the head. I think Z3 (or any SMT solver) wouldn't be the best tool to tackle such problems where you expect to reason about matrices of "unknown" sizes, as you put it. When you have concrete instances of the problem, I think Z3 can be quite effective; but not in the general "forall sizes" case. Those sort of claims usually would need inductive proofs and are better suited for other tools.

However, you might get away with uninterpreted functions. If you represent your matrix and filters as uninterpreted functions and code your convolution in terms of that. You'll probably have to assume an upper bound on NxM (i.e., N < 100, M < 100; or similar), and code accordingly so that anything out-of-the-bounds produces suitable results. (What that means would, of course, depend on the problem at hand.)

You might be surprised how cool Z3 can be under that setting, as I suspect it would give you quite good results. I'd love to hear what you find out if you try this approach.