# [On Satisfiability of Polynomial Equations over Large Prime Fields]

There are several desired properties for the system of polynomials:

- given a constraint system, check whether it represents a function, i.e. whether the output variables are uniquely determined by the input;
- given two constraint systems, check whether they are equisatisfiable;
- more generically, check whether a constraint system conforms to a spec;

This paper introduces the automated decision procedure on the satisfiability of zkSNARK constraint systems. zkSNARK constraint systems have the special property that the values are in the large prime field.

## Fast Algebraic Geometry Method

Assumes that the polynomial set defines a prime ideal and defines an absolutely irreducible algebraic set(a variety).
The [algorithm](https://www.ams.org/journals/mcom/2006-75-256/S0025-5718-06-01878-3/) for this case can find one common root in probabilistic polynomial time.

## Robust Algebraic Geometry Method

It recursively decomposes the problem's algebraic set until it either reaches a variety(then deciding for satisfiable) or it is no longer possible to decompose, deciding for unsatisfiable.

## Methods based on Groebner basis

What is Groebner basis? Check [this](https://hackmd.io/@OwahZGWKSdG_wE0NU1dUVA/ryudOLTVj).

The point is if Groebner basis of the basis is satisfiable by some assignment, then the original basis is also satisfiable by the same assignment. Given an arbitrary basis, an equivalent Groebner basis can be found by Buchberger's algorithm. The paper has implemented Buchberger's algorithm and this algorithm is capable of calculating Groebner basis in grevelx ordering.
What is the monomial ordering(e.g. grevlex, lexicographical)? Check this.

After computing Groebner basis, there are two ways to find the root of Groebner basis.

- Groebner basis into triangular format and then find the root of variables one by one
- Compute primary decomposition of the ideal defined by Groebner basis, and then compute the algebraic set for each primary ideals.

### Triangular system

Groebner basis in lexicographical ordering is in triangular format which has the elimination property. We can eliminate one variable at a time to solve the whole system. However, Groebner basis is much more faster to compute in grevlex ordering and the paper implemented the one. Thus the paper uses Groebner Walk to obtain lexicographical ordering from grevlex ordering.
Finding the root of a univariate polynomial is achieved by [Cantor-Zassenhaus algorithm](https://en.wikipedia.org/wiki/Cantor%E2%80%93Zassenhaus_algorithm) which has complexity of $O(d^3\log{p})$.

### Primary Decomposition Method

This method reduces the big problem into smaller sub-problems.

Every polynomial set defines an algebraic set, which is the set of points in $\mathbb{F}^n$ where all polynomials evaluate to zero.

The polynomial set defines an ideal, and it is the intersection of a finite set of primary ideals by Lasker-Noether theorem. What is Lasker-Noether theorem? Check this.

### Base field restriction

The following equation restricts the root of Groebner basis to the base field.

$$
x^p - x = 0
$$

## Local Search Method