Here I made implementation of integer coefficients matrix inversion
Note: invertible matrix should have det = 1 or det = -1
How it works
- converting integers to bit-vectors in two’s complement format
- addition is implemented with FullAdder primitives
- multiplication is implemented with Baugh-Wooley circuit
- Boolean circuits are converted to CNF with Tseytin transformation
- CNFs are solved by Z3 solver
- Note: no control of integer overflow, but it could be implemented easily
Details
Addition circuit
for 4-bit signed integers
Multiplication circuit
for 4-bit signed integers
I have found typo in original paper, so here is fixed circuit
Usage
Note: z3 should be available in your PATH
Call program with following arguments provided:
-bw,--bitwidth <arg> bit width of bit vectors (8 for example)
-c,--cnf <arg> Path to file for output CNF in DIMACS format
-m,--matrix <arg> Path to text file with matrix
Example
--bitwidth 8 --matrix matrix/4x4.txt --cnf out.cnf
Gives following output
== input ==
2 1 0 1
3 2 0 -2
0 1 1 0
-1 2 3 4
== cnf summary ==
gates count = 28817
variables count = 28705
clauses count = 94145
== z3 time ==
168 millis
== output ==
6 -5 12 -4
-10 9 -21 7
10 -9 22 -7
-1 1 -3 1
