Boolean matrix times vector multiplication in Z3

Question

How to multiply a variable Boolean matrix by a Boolean vector in Z3 in a nice way? The sizes of the matrix and of vectors are known and fixed.

In my case there is only one matrix and there is no need to pass it as an argument or return it as a result of a function, so the matrix can be global.

Does it help if the matrix is a square matrix?

My current solution is:

; Maybe some other matrix representation would be better?
(declare-datatypes () ((ColumnIndex c0 c1 c2)))
(declare-fun column (ColumnIndex) (_ BitVec 4))

(define-fun scalarTimesVector ((a (_ BitVec 1)) (v (_ BitVec 4))) (_ BitVec 4)
  (ite (= a #b1) v (_ bv0 4))
)

(define-fun matrixTimesVector ((vector (_ BitVec 3))) (_ BitVec 4)
  (bvor
    (scalarTimesVector ((_ extract 0 0) vector) (column c0))
    (scalarTimesVector ((_ extract 1 1) vector) (column c1))
    (scalarTimesVector ((_ extract 2 2) vector) (column c2))
  )
)

score 0 · Accepted Answer · answered Jul 13 '18 at 17:39

0

What you are doing is just fine, especially given your matrix size is constant and never change. SMTLib has no notion of loops, although recent versions do allow recursive definitions of functions that can be used for this effect. See this answer for a different but related question on how to use recursion: https://stackoverflow.com/a/51140049/936310. However, I'd recommend sticking to your current code for simplicity and wider support from a variety of solvers.

In my mind, SMTLib should really be "generated" instead of directly used; and most tools use it this way. If your programming needs get more complicated, I'd recommend using a higher-level interface instead. There are interfaces to Z3 and other solvers from pretty much any language you can imagine. Python and Haskell provide really high-level bindings that get rid of most of the boilerplate for you. You also have low-level bindings from C/C++/Java if that's your choice. See using floating point arithmetic with Z3 C++ APIs for a comparison of the styles.

answered Jul 13 '18 at 17:39

alias

28,120
2
23
40

Thanks for the answer! I was trying to avoid the repetitive parts in my sample code. Even if objects corresponding to these repetitive lines in my matrixTimesVector function were created in some host language (Python, Haskell, …) then still it is not obvious that this is the right way of doing things. It looks a bit like adding a lot of "simple" constraints. One could ponder if Z3 has some natural and compact way of expressing this as a one "complex" constraint which perhaps can be better understood and optimized by the solver. – km9c3uwc Jul 13 '18 at 18:28
1

I think "repetitive" constraints are just fine in the generated SMTLib code. When it comes to solving, you want as simple constraints as possible with as many constants around, without any clever coding tricks. When you code in a high-level language you can be concise and readable, but when it comes to solving, the simpler the better. (I think of it as writing in a high-level language and having the compiler turn it into "simple" machine code that can be repetitive but is understood by the underlying metal. SMTLib is the assembly for SMT solvers, and the simpler the better.) – alias Jul 16 '18 at 21:48

Boolean matrix times vector multiplication in Z3

1 Answers1