# Gröbner basis used in circuits

## What is Gröbner basis?

Let's say we have a set of equations:

x^2 + y^2 + z^2 - 1 = 0
x^2 - y + z^2 = 0
x - z = 0

Using Gröbner basis we can transform the system into an equivalent system:

4 * z^4 + 2 * z^2 - 1 = 0
y - 2 * z^2 = 0
x - z = 0

This system is much easier to solve (the first equation is univariate) and this is what Gröbner basis is actually intended for - to get the zeros of the system of polynomial equations.

However, we could use Gröbner basis for circuite as well. Two potential uses might be:
1. Simplifying the constraint system.
2. Automate the witness assignment.
3. Checking whether there might be some problems in the circuit.
4. Checking whether two circuits are equivalent (for example, whether two different implementations of Keccak are the same).

## 1. Simplifying the constraint system

We have a constraint system and we try to simplify it. Let's say we have columns `a`, `b`, `c` and the constraint system:

a * b - b * c = 0
a^2 + c^2 - b = 0

We get the system of polynomial equations (just changing the names of the variables for the alignment with the example above):

x * y - y * z = 0
x^2 + z^2 - y = 0

### Rotations

Note, that if there are rotations involved, each rotation requires the introduction of a new variable.

For example, if we have a constraint system

a_cur * a_next + a_cur * a_cur
a_cur - a_next_next * a_next_next

we get:

x0 * x1 + x0 * x0
x0 - x2 * x2

### Fixed columns

We need to take the fixed columns into account because we want the output to be the system of the constraints that is equivalent to the original one.

There are two options how to handle the fixed columns:
* Introduce them as variables, but this makes the transformation to the Gröbner basis much slower.
* Resolve them to the actual values, so that they can be simplified in the process of the transformation to the Gröbner basis.

A bit of testing (some experiments [here](https://github.com/miha-stopar/polynomial-solver), based on Edu's [polyexen](https://github.com/Dhole/polyexen) and [polynomial-solver](https://github.com/lvella/polynomial-solver) by Lucas Clemente Vella) showed that fixed columns make the transformation to the Gröbner basis very slow. This is somehow expected, as the fixed column `q` in many cases acts as a multiplifer of the whole constraint and it increases the degree of all terms, like:

q * (a^2 + b - 1) = 0

So, due to efficiency reasons, the second option is used. However, now you need to reintroduce the fixed columns after the transformation is finished.

For example, the constraint might have two fixed columns `q1`, `q2`:

`q1^2 * a1^2 + q2 * a2^3`

Let's say that this constraint is rewritten using Gröbner basis into:

`(q1 + 1) * a1 + q2 * a2`

As we chose the second option to handle the fixed columns, `q1` and `q2` are concrete numbers in our new constraint system.

However, we know at which rows each constraint is fired - `polyexen` resolves the fixed columns and for each row returns only the non-zero constraints.

We prepare a new fixed column for each of the constraints.

{"Byte to Byte row 2": [0, 1, 1,...], "Header row 1": [0, 1, 1, ...], "Header to byte row 4": [1,0,0,...], ...}

When the fixed columns are prepared we iterate over them to see whether some of the constraints use the same fixed column. In most cases, all the constraints will use the same fixed column, so we end up only with one fixed column. The following dictionary maps the constraints to the index of the fixed column (most of them show to the fixed column with index 1).

{"Byte to Byte row 2": 1, "Header row 1": 1, "Header to byte row 4": 1, "Header to byte row 2": 1, "Header to byte row 0": 1, "Byte to Byte row 1": 1, "Header to header row 0": 1, "Byte to Byte row 0": 1, "Byte row 0": 1, "Header to byte row 3": 1, "Header to header row 1": 1, "Header row 0": 1, "is_zero gate 0": 0, "Header to byte row 1": 1, "Byte to Header row 0": 1, "Byte to Byte row 4": 1, "Byte to Byte row 3": 1, "first and last row 0": 0}

### Examining subsets of constraints

We can use the transformation on different sets of constraints separately. Let's say we have a set of constraints `S1 = {c1, c2, c3}` that are fired at some subset of rows, and another set of constraints `S2 = {c4, c5, c6, c7}` that are fired at some other subset of rows.

We can try to get the Gröbner basis for `S1` and another Gröbner basis for `S2`.

### Efficiency

Number of variables / duration of transformation (for 20 polynomials):
- 11: immediate result
- 13: 17 sec
- 14: 102 sec

Given the number of columns (that is: variables) in the ZKEVM circuits (for example, MPT circuit around 120 columns), the transformation might take a really long time.

Still, this is to be run only once, so there might still be value if we get a simpler constraint system.

The constraint system is simplified if the highest degree of the polynomials is reduced - that means we have a smaller extended domain in Halo2.

But can the transformation to the Gröbner basis reduce the highest degree?

An example:

Original constraint system:
-1*x2*x1^2*x0 + x1*x0
-1*x5*x4*x3*x0 + x5*x3*x0 + x4*x3*x0
x6*x5*x3*x0 + -1*x6*x5*x0 + -1*x6*x3*x0 + x6*x0
-1*x8*x5*x3*x0 + x8*x5*x0 + x8*x3*x0 + -1*x8*x0 + x7*x5*x3*x0 + -1*x7*x5*x0 + -1*x7*x3*x0 + x7*x0
-1*x9*x5*x3*x0 + x9*x3*x0 + -1*x5*x3*x2*x1*x0 + x5*x3*x0 + x3*x2*x1*x0 + -1*x3*x0
=============
variables count: 10
Gröbner Basis constraint system:
-1*x2*x1^2*x0 + x1*x0
-1*x5*x4*x3*x0 + x5*x3*x0 + x4*x3*x0
x6*x3^2*x0 + -1*x6*x3*x0
x6*x5*x3*x0 + -1*x6*x5*x0 + -1*x6*x3*x0 + x6*x0
x6*x5*x4*x0 + -1*x6*x5*x0 + -1*x6*x4*x0 + -1*x6*x3*x0 + x6*x0
-1*x8*x3^2*x0 + x8*x3*x0 + x7*x3^2*x0 + -1*x7*x3*x0
-1*x8*x5*x3*x0 + x8*x5*x0 + x8*x3*x0 + -1*x8*x0 + x7*x5*x3*x0 + -1*x7*x5*x0 + -1*x7*x3*x0 + x7*x0
-1*x8*x5*x4*x0 + x8*x5*x0 + x8*x4*x0 + x8*x3*x0 + -1*x8*x0 + x7*x5*x4*x0 + -1*x7*x5*x0 + -1*x7*x4*x0 + -1*x7*x3*x0 + x7*x0
x9*x3*x0 + x3*x2*x1*x0 + -1*x3*x0
x9*x6*x5*x0 + -1*x9*x6*x0 + x6*x5*x2*x1*x0 + -1*x6*x5*x0 + -1*x6*x2*x1*x0 + x6*x0
-1*x9*x8*x5*x0 + x9*x8*x0 + x9*x7*x5*x0 + -1*x9*x7*x0 + -1*x8*x5*x2*x1*x0 + x8*x5*x0 + x8*x2*x1*x0 + -1*x8*x0 + x7*x5*x2*x1*x0 + -1*x7*x5*x0 + -1*x7*x2*x1*x0 + x7*x0

Both two constraint systems above have the same degree - meaning we didn't achieve much by the transformation to the Gröbner basis.

If you observe the example at the top of the page, you can see that the situation is even worse. Yes, the second system is simpler too solve, but the degree of the first polynomial is increased by 2 (a bigger extended domain is needed).

There are cases when the degree is reduced, but they are most probably rare.

For example:

a^2 * b^2 - 2**8 = 0
b^2 - 2**2 = 0

In this case the transformation would get us to:

a^2 - 2**6 = 0

The degree is reduced in this case, but most likely such reduction would be noticed and applied already at the time of writing the circuit constraints.

## 2. Automate witness assignment

Differently as for the simplifying case above, the Gröbner is probably very useful for the automation of the witness assignment.

In this case, we can resolve the fixed columns. We have some initial witness data which is resolved too and then we can try to compute the other parts of the witness.

We first have a system of equations like:

"is_zero gate 0" BYTECODE_push_data_left[0]*(1 - BYTECODE_push_data_left[0]*BYTECODE_push_data_left_inv[0])
-1*x1*x0^2 + x0
"first and last row 0" tag[0]
x2
"Header row 0" index[0]*(1 - tag[0])
-1*x3*x2 + x3
"Header row 1" (1 - tag[0])*(value[0] - BYTECODE_length[0])
x5*x2 + -1*x5 + -1*x4*x2 + x4
"Byte row 0" tag[0]*(is_code[0] - (1 - BYTECODE_push_data_left[0]*BYTECODE_push_data_left_inv[0]))
x6*x2 + x2*x1*x0 + -1*x2
"Header to header row 0" BYTECODE_length[0]*(1 - (1 - (1 - tag[0])*(1 - tag[1])))
x7*x5*x2 + -1*x7*x5 + -1*x5*x2 + x5
"Header to header row 1" (1 - (1 - (1 - tag[0])*(1 - tag[1])))*(code_hash[0] - (112*1234^0 + 164*1234^1 + 133*1234^2 + 93*1234^3 + 4*1234^4 + 216*1234^5 + 250*1234^6 + 123*1234^7 + 59*1234^8 + 39*1234^9 + 130*1234^10 + 202*1234^11 + 83*1234^12 + 182*1234^13 + 229*1234^15 + 192*1234^16 + 3*1234^17 + 199*1234^18 + 220*1234^19 + 178*1234^20 + 125*1234^21 + 126*1234^22 + 146*1234^23 + 60*1234^24 + 35*1234^25 + 247*1234^26 + 134*1234^27 + 1234^28 + 70*1234^29 + 210*1234^30 + 197*1234^31))
-197*x9^31*x7*x2 + 197*x9^31*x7 + 197*x9^31*x2 + -197*x9^31 + -210*x9^30*x7*x2 + 210*x9^30*x7 + 210*x9^30*x2 + -210*x9^30 + -70*x9^29*x7*x2 + 70*x9^29*x7 + 70*x9^29*x2 + -70*x9^29 + -1*x9^28*x7*x2 + x9^28*x7 + x9^28*x2 + -1*x9^28 + -134*x9^27*x7*x2 + 134*x9^27*x7 + 134*x9^27*x2 + -134*x9^27 + -247*x9^26*x7*x2 + 247*x9^26*x7 + 247*x9^26*x2 + -247*x9^26 + -35*x9^25*x7*x2 + 35*x9^25*x7 + 35*x9^25*x2 + -35*x9^25 + -60*x9^24*x7*x2 + 60*x9^24*x7 + 60*x9^24*x2 + -60*x9^24 + -146*x9^23*x7*x2 + 146*x9^23*x7 + 146*x9^23*x2 + -146*x9^23 + -126*x9^22*x7*x2 + 126*x9^22*x7 + 126*x9^22*x2 + -126*x9^22 + -125*x9^21*x7*x2 + 125*x9^21*x7 + 125*x9^21*x2 + -125*x9^21 + -178*x9^20*x7*x2 + 178*x9^20*x7 + 178*x9^20*x2 + -178*x9^20 + -220*x9^19*x7*x2 + 220*x9^19*x7 + 220*x9^19*x2 + -220*x9^19 + -199*x9^18*x7*x2 + 199*x9^18*x7 + 199*x9^18*x2 + -199*x9^18 + -3*x9^17*x7*x2 + 3*x9^17*x7 + 3*x9^17*x2 + -3*x9^17 + -192*x9^16*x7*x2 + 192*x9^16*x7 + 192*x9^16*x2 + -192*x9^16 + -229*x9^15*x7*x2 + 229*x9^15*x7 + 229*x9^15*x2 + -229*x9^15 + -182*x9^13*x7*x2 + 182*x9^13*x7 + 182*x9^13*x2 + -182*x9^13 + -83*x9^12*x7*x2 + 83*x9^12*x7 + 83*x9^12*x2 + -83*x9^12 + -202*x9^11*x7*x2 + 202*x9^11*x7 + 202*x9^11*x2 + -202*x9^11 + -130*x9^10*x7*x2 + 130*x9^10*x7 + 130*x9^10*x2 + -130*x9^10 + -39*x9^9*x7*x2 + 39*x9^9*x7 + 39*x9^9*x2 + -39*x9^9 + -59*x9^8*x7*x2 + 59*x9^8*x7 + 59*x9^8*x2 + -59*x9^8 + -123*x9^7*x7*x2 + 123*x9^7*x7 + 123*x9^7*x2 + -123*x9^7 + -250*x9^6*x7*x2 + 250*x9^6*x7 + 250*x9^6*x2 + -250*x9^6 + -216*x9^5*x7*x2 + 216*x9^5*x7 + 216*x9^5*x2 + -216*x9^5 + -4*x9^4*x7*x2 + 4*x9^4*x7 + 4*x9^4*x2 + -4*x9^4 + -93*x9^3*x7*x2 + 93*x9^3*x7 + 93*x9^3*x2 + -93*x9^3 + -133*x9^2*x7*x2 + 133*x9^2*x7 + 133*x9^2*x2 + -133*x9^2 + -164*x9*x7*x2 + 164*x9*x7 + 164*x9*x2 + -164*x9 + x8*x7*x2 + -1*x8*x7 + -1*x8*x2 + x8 + -112*x7*x2 + 112*x7 + 112*x2 + -112
"Header to byte row 0" tag[1]*(1 - tag[0])*(BYTECODE_length[1] - BYTECODE_length[0])
-1*x10*x7*x2 + x10*x7 + x7*x5*x2 + -1*x7*x5
"Header to byte row 1" tag[1]*index[1]*(1 - tag[0])
-1*x11*x7*x2 + x11*x7
"Header to byte row 2" tag[1]*(1 - tag[0])*(-1 + is_code[1])
-1*x12*x7*x2 + x12*x7 + x7*x2 + -1*x7
"Header to byte row 3" tag[1]*(1 - tag[0])*(code_hash[1] - code_hash[0])
-1*x13*x7*x2 + x13*x7 + x8*x7*x2 + -1*x8*x7
"Header to byte row 4" tag[1]*(1 - tag[0])*(BYTECODE_value_rlc[1] - value[1])
x15*x7*x2 + -1*x15*x7 + -1*x14*x7*x2 + x14*x7
"Byte to Byte row 0" tag[0]*tag[1]*(BYTECODE_length[1] - BYTECODE_length[0])
x10*x7*x2 + -1*x7*x5*x2
"Byte to Byte row 1" tag[0]*tag[1]*(index[1] - (1 + index[0]))
x11*x7*x2 + -1*x7*x3*x2 + -1*x7*x2
"Byte to Byte row 2" tag[0]*tag[1]*(code_hash[1] - code_hash[0])
x13*x7*x2 + -1*x8*x7*x2
"Byte to Byte row 3" tag[0]*tag[1]*(BYTECODE_value_rlc[1] - (value[1] + 1234*BYTECODE_value_rlc[0]))
-1*x16*x9*x7*x2 + -1*x15*x7*x2 + x14*x7*x2
"Byte to Byte row 4" tag[0]*tag[1]*(BYTECODE_push_data_left[1] - (is_code[0]*BYTECODE_push_data_size[0] + (1 - is_code[0])*(-1 + BYTECODE_push_data_left[0])))
-1*x18*x7*x6*x2 + x17*x7*x2 + x7*x6*x2*x0 + -1*x7*x6*x2 + -1*x7*x2*x0 + x7*x2
"Byte to Header row 0" tag[0]*(1 - tag[1])*(1 + index[0] - BYTECODE_length[0])
x7*x5*x2 + -1*x7*x3*x2 + -1*x7*x2 + -1*x5*x2 + x3*x2 + x2
"is_zero gate 0" BYTECODE_push_data_left[1]*(1 - BYTECODE_push_data_left[1]*BYTECODE_push_data_left_inv[1])
-1*x19*x17^2 + x17
"first and last row 0" tag[1]*(1 - )
0

And after transformation:

-1*x1*x0^2 + x0
x2
x3
-1*x5 + x4
-1*x7*x4 + x4
197*x9^31*x7 + -197*x9^31 + 210*x9^30*x7 + -210*x9^30 + 70*x9^29*x7 + -70*x9^29 + x9^28*x7 + -1*x9^28 + 134*x9^27*x7 + -134*x9^27 + 247*x9^26*x7 + -247*x9^26 + 35*x9^25*x7 + -35*x9^25 + 60*x9^24*x7 + -60*x9^24 + 146*x9^23*x7 + -146*x9^23 + 126*x9^22*x7 + -126*x9^22 + 125*x9^21*x7 + -125*x9^21 + 178*x9^20*x7 + -178*x9^20 + 220*x9^19*x7 + -220*x9^19 + 199*x9^18*x7 + -199*x9^18 + 3*x9^17*x7 + -3*x9^17 + 192*x9^16*x7 + -192*x9^16 + 229*x9^15*x7 + -229*x9^15 + 182*x9^13*x7 + -182*x9^13 + 83*x9^12*x7 + -83*x9^12 + 202*x9^11*x7 + -202*x9^11 + 130*x9^10*x7 + -130*x9^10 + 39*x9^9*x7 + -39*x9^9 + 59*x9^8*x7 + -59*x9^8 + 123*x9^7*x7 + -123*x9^7 + 250*x9^6*x7 + -250*x9^6 + 216*x9^5*x7 + -216*x9^5 + 4*x9^4*x7 + -4*x9^4 + 93*x9^3*x7 + -93*x9^3 + 133*x9^2*x7 + -133*x9^2 + 164*x9*x7 + -164*x9 + -1*x8*x7 + x8 + 112*x7 + -112
-1*x10*x4 + x4^2
x10*x7 + -1*x4
197*x10*x9^31 + 210*x10*x9^30 + 70*x10*x9^29 + x10*x9^28 + 134*x10*x9^27 + 247*x10*x9^26 + 35*x10*x9^25 + 60*x10*x9^24 + 146*x10*x9^23 + 126*x10*x9^22 + 125*x10*x9^21 + 178*x10*x9^20 + 220*x10*x9^19 + 199*x10*x9^18 + 3*x10*x9^17 + 192*x10*x9^16 + 229*x10*x9^15 + 182*x10*x9^13 + 83*x10*x9^12 + 202*x10*x9^11 + 130*x10*x9^10 + 39*x10*x9^9 + 59*x10*x9^8 + 123*x10*x9^7 + 250*x10*x9^6 + 216*x10*x9^5 + 4*x10*x9^4 + 93*x10*x9^3 + 133*x10*x9^2 + 164*x10*x9 + -1*x10*x8 + 112*x10 + -197*x9^31*x4 + -210*x9^30*x4 + -70*x9^29*x4 + -1*x9^28*x4 + -134*x9^27*x4 + -247*x9^26*x4 + -35*x9^25*x4 + -60*x9^24*x4 + -146*x9^23*x4 + -126*x9^22*x4 + -125*x9^21*x4 + -178*x9^20*x4 + -220*x9^19*x4 + -199*x9^18*x4 + -3*x9^17*x4 + -192*x9^16*x4 + -229*x9^15*x4 + -182*x9^13*x4 + -83*x9^12*x4 + -202*x9^11*x4 + -130*x9^10*x4 + -39*x9^9*x4 + -59*x9^8*x4 + -123*x9^7*x4 + -250*x9^6*x4 + -216*x9^5*x4 + -4*x9^4*x4 + -93*x9^3*x4 + -133*x9^2*x4 + -164*x9*x4 + x8*x4 + -112*x4
-1*x11*x4
x11*x7
197*x11*x9^31 + 210*x11*x9^30 + 70*x11*x9^29 + x11*x9^28 + 134*x11*x9^27 + 247*x11*x9^26 + 35*x11*x9^25 + 60*x11*x9^24 + 146*x11*x9^23 + 126*x11*x9^22 + 125*x11*x9^21 + 178*x11*x9^20 + 220*x11*x9^19 + 199*x11*x9^18 + 3*x11*x9^17 + 192*x11*x9^16 + 229*x11*x9^15 + 182*x11*x9^13 + 83*x11*x9^12 + 202*x11*x9^11 + 130*x11*x9^10 + 39*x11*x9^9 + 59*x11*x9^8 + 123*x11*x9^7 + 250*x11*x9^6 + 216*x11*x9^5 + 4*x11*x9^4 + 93*x11*x9^3 + 133*x11*x9^2 + 164*x11*x9 + -1*x11*x8 + 112*x11
-1*x12*x4 + x4
x12*x7 + -1*x7
197*x12*x9^31 + 210*x12*x9^30 + 70*x12*x9^29 + x12*x9^28 + 134*x12*x9^27 + 247*x12*x9^26 + 35*x12*x9^25 + 60*x12*x9^24 + 146*x12*x9^23 + 126*x12*x9^22 + 125*x12*x9^21 + 178*x12*x9^20 + 220*x12*x9^19 + 199*x12*x9^18 + 3*x12*x9^17 + 192*x12*x9^16 + 229*x12*x9^15 + 182*x12*x9^13 + 83*x12*x9^12 + 202*x12*x9^11 + 130*x12*x9^10 + 39*x12*x9^9 + 59*x12*x9^8 + 123*x12*x9^7 + 250*x12*x9^6 + 216*x12*x9^5 + 4*x12*x9^4 + 93*x12*x9^3 + 133*x12*x9^2 + 164*x12*x9 + -1*x12*x8 + 112*x12 + -197*x9^31 + -210*x9^30 + -70*x9^29 + -1*x9^28 + -134*x9^27 + -247*x9^26 + -35*x9^25 + -60*x9^24 + -146*x9^23 + -126*x9^22 + -125*x9^21 + -178*x9^20 + -220*x9^19 + -199*x9^18 + -3*x9^17 + -192*x9^16 + -229*x9^15 + -182*x9^13 + -83*x9^12 + -202*x9^11 + -130*x9^10 + -39*x9^9 + -59*x9^8 + -123*x9^7 + -250*x9^6 + -216*x9^5 + -4*x9^4 + -93*x9^3 + -133*x9^2 + -164*x9 + x8 + -112
-1*x13*x4 + x8*x4
x13*x7 + -1*x8*x7
197*x13*x9^31 + 210*x13*x9^30 + 70*x13*x9^29 + x13*x9^28 + 134*x13*x9^27 + 247*x13*x9^26 + 35*x13*x9^25 + 60*x13*x9^24 + 146*x13*x9^23 + 126*x13*x9^22 + 125*x13*x9^21 + 178*x13*x9^20 + 220*x13*x9^19 + 199*x13*x9^18 + 3*x13*x9^17 + 192*x13*x9^16 + 229*x13*x9^15 + 182*x13*x9^13 + 83*x13*x9^12 + 202*x13*x9^11 + 130*x13*x9^10 + 39*x13*x9^9 + 59*x13*x9^8 + 123*x13*x9^7 + 250*x13*x9^6 + 216*x13*x9^5 + 4*x13*x9^4 + 93*x13*x9^3 + 133*x13*x9^2 + 164*x13*x9 + -1*x13*x8 + 112*x13 + -197*x9^31*x8 + -210*x9^30*x8 + -70*x9^29*x8 + -1*x9^28*x8 + -134*x9^27*x8 + -247*x9^26*x8 + -35*x9^25*x8 + -60*x9^24*x8 + -146*x9^23*x8 + -126*x9^22*x8 + -125*x9^21*x8 + -178*x9^20*x8 + -220*x9^19*x8 + -199*x9^18*x8 + -3*x9^17*x8 + -192*x9^16*x8 + -229*x9^15*x8 + -182*x9^13*x8 + -83*x9^12*x8 + -202*x9^11*x8 + -130*x9^10*x8 + -39*x9^9*x8 + -59*x9^8*x8 + -123*x9^7*x8 + -250*x9^6*x8 + -216*x9^5*x8 + -4*x9^4*x8 + -93*x9^3*x8 + -133*x9^2*x8 + -164*x9*x8 + x8^2 + -112*x8
x15*x4 + -1*x14*x4
-1*x15*x7 + x14*x7
-197*x15*x9^31 + -210*x15*x9^30 + -70*x15*x9^29 + -1*x15*x9^28 + -134*x15*x9^27 + -247*x15*x9^26 + -35*x15*x9^25 + -60*x15*x9^24 + -146*x15*x9^23 + -126*x15*x9^22 + -125*x15*x9^21 + -178*x15*x9^20 + -220*x15*x9^19 + -199*x15*x9^18 + -3*x15*x9^17 + -192*x15*x9^16 + -229*x15*x9^15 + -182*x15*x9^13 + -83*x15*x9^12 + -202*x15*x9^11 + -130*x15*x9^10 + -39*x15*x9^9 + -59*x15*x9^8 + -123*x15*x9^7 + -250*x15*x9^6 + -216*x15*x9^5 + -4*x15*x9^4 + -93*x15*x9^3 + -133*x15*x9^2 + -164*x15*x9 + x15*x8 + -112*x15 + 197*x14*x9^31 + 210*x14*x9^30 + 70*x14*x9^29 + x14*x9^28 + 134*x14*x9^27 + 247*x14*x9^26 + 35*x14*x9^25 + 60*x14*x9^24 + 146*x14*x9^23 + 126*x14*x9^22 + 125*x14*x9^21 + 178*x14*x9^20 + 220*x14*x9^19 + 199*x14*x9^18 + 3*x14*x9^17 + 192*x14*x9^16 + 229*x14*x9^15 + 182*x14*x9^13 + 83*x14*x9^12 + 202*x14*x9^11 + 130*x14*x9^10 + 39*x14*x9^9 + 59*x14*x9^8 + 123*x14*x9^7 + 250*x14*x9^6 + 216*x14*x9^5 + 4*x14*x9^4 + 93*x14*x9^3 + 133*x14*x9^2 + 164*x14*x9 + -1*x14*x8 + 112*x14
-1*x19*x17^2 + x17

For example, we can see from

x2
x3
-1*x5 + x4

that:

x2 = 0
x3 = 0
x4 = x5

## 3. Checking whether there might be some problems in the circuit

Gröbner basis might be useful to detect if the system is underconstrained. For example, if the number of the polynomials is reduced during the transformation to the Gröbner basis, this might be a sign of the system being underconstrained.

## 4. Checking whether two circuits are equivalent

For example, in ZKEVM, there are multiple implementations of Keccak. Can we check whether they are equivalent.

Maybe, but the large number of polynomials and columns might make the transformation not possible.

Currently, F4 and F5 algorithms to compute the Gröbner basis can deal with several hundreds of polynomials, having each several hundreds of terms and coefficients of several hundreds of digits.

Note that if the subsets of the constraints are examined separately as suggested above, it makes the comparison of the two implementations difficult because of different fixed columns.

## Conclusion

1. Simplifying the constraint system: not very likely.
2. Automate the witness assignment: helpful.
3. Checking whether there might be some problems in the circuit: might be helpful.
4. Checking whether two circuits are equivalent: might be helpful, but there are obstacles (we might not be able to observe the subsets of constraints).