Multivariate Quadratic to SAT converter

mq2sat tool convert $m$ quadratic polynomials with $n$ variables over $GF(2^w)$ into CNF (DIMACS) file to a SAT solver. The input file format for this polynomials
\[p_1(x_1,\ldots,x_n)= \sum_{1\leq i \leq j \leq n} \alpha^{(1)}_{i,j}x_ix_j + \sum_{1\leq i \leq n} \beta^{(1)}_{i}x_i + \gamma^{(1)}=\delta^{(1)}\] \[p_2(x_1,\ldots,x_n)= \sum_{1\leq i \leq j \leq n} \alpha^{(2)}_{i,j}x_ix_j + \sum_{1\leq i \leq n} \beta^{(2)}_{i}x_i + \gamma^{(2)}=\delta^{(2)}\] \[\vdots \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \vdots\] \[p_m(x_1,\ldots,x_n)= \sum_{1\leq i \leq j \leq n} \alpha^{(m)}_{i,j}x_ix_j + \sum_{1\leq i \leq n} \beta^{(m)}_{i}x_i + \gamma^{(m)}=\delta^{(m)}\] is given by

$n \ \ m \ \ w$
$\delta^{(1)} \ \ \delta^{(2)} \ \ \delta^{(3)} \ \ \ldots \ \ \delta^{(m)}$
$\alpha^{(1)}_{1,1}$
$\alpha^{(1)}_{2,1} \ \ \alpha^{(2)}_{2,2}$
$\alpha^{(1)}_{3,1} \ \ \alpha^{(2)}_{3,2} \ \ \alpha^{(1)}_{3,3}$
$ \vdots$
$\alpha^{(1)}_{n,1} \ \ \alpha^{(2)}_{n,2} \ \ \ldots \ \ \alpha^{(1)}_{n,n}$
$\beta^{(1)}_{1} \ \ \beta^{(1)}_{2} \beta^{(1)}_{3} \ \ \ldots \ \ \beta^{(1)}_{n} \ \ \gamma^{(1)}$
$\alpha^{(2)}_{1,1}$
$\alpha^{(2)}_{2,1} \ \ \alpha^{(2)}_{2,2}$
$\alpha^{(2)}_{3,1} \ \ \alpha^{(2)}_{3,2} \ \ \alpha^{(2)}_{3,3}$
$ \vdots$
$\alpha^{(2)}_{n,1} \ \ \alpha^{(2)}_{n,2} \ \ \ldots \ \ \alpha^{(2)}_{n,n}$
$\beta^{(2)}_{1} \ \ \beta^{(2)}_{2} \beta^{(2)}_{3} \ \ \ldots \ \ \beta^{(2)}_{n} \ \ \gamma^{(2)}$
$\vdots$
$\alpha^{(m)}_{1,1}$
$\alpha^{(m)}_{2,1} \ \ \alpha^{(m)}_{2,2}$
$\alpha^{(m)}_{3,1} \ \ \alpha^{(m)}_{3,2} \ \ \alpha^{(m)}_{3,3}$
$ \vdots$
$\alpha^{(m)}_{n,1} \ \ \alpha^{(m)}_{n,2} \ \ \ldots \ \ \alpha^{(m)}_{n,n}$
$\beta^{(m)}_{1} \ \ \beta^{(m)}_{2} \beta^{(m)}_{3} \ \ \ldots \ \ \beta^{(m)}_{n} \ \ \gamma^{(m)}$

For instance, consider 3 polynomials with 2 variables over $GF(2^2)$ \[p_1(x_1,x_2)=2x_1^2 + x_1x_2 + 2x_1+1=3\] \[p_2(x_1,x_2)=x_1^2 + 3x_2^2 + 3x_1x_2+2=0\] \[p_3(x_1,x_2)=3x_1^2 + x_2^2 + 2x_1x_2+3x_2=1\]

The input file for mq2sat tool is given by
3 2 2
3 0 1
2
1 0
2 0 1
1
3 3
0 0 2
3
2 1
0 3 0

Then we can run mq2sat and it return

$ mq2sat input.mq
SATISFIABLE
X1=3
X2=0
SOLUTION IS CONFIRMED

The overall process generate two files tmp.anf and tmp.cnf.