Checking distance one proofs

Armin Biere, Manuel Kauers, Daniela Ritirc

We want to decide if two two-dimensional points (x1,y1) and (x2,y2) have exact distance 1. Therefore we check if the square of euclidean norm (x1-x2)^2 + (y1-y2)^2 is equal to 1.

Approach

To gain a precise calculation we use an approach based on computer algebra, more precisely we will use Groebner basis theory.

Let p = -1 + (x1-x2)^2 + (y1-y2)^2

At first we encode every occurring square root "Sqrt[i]" in p by a unique variable "si", e.g. "s3" represents Sqrt[3]. For each such variable we need to define a describing polynomial of the form "si^2 - i", which specifies the root(s) of the variable. For "s3" the describing polynomial would be "s3^2-3".

If Sqrt[i] occurrs in the denominator we need a special variable "ri", which represents "1/Sqrt[i]". Otherwise the encoded polynomials would have variables in the denominator, which does not match the definition of a polynomial. Also for "ri" describing polynomials are needed. These have the form "ri * si - 1", expressing that "ri" is the inverse of "si".

A very important restriction is that for "Sqrt[i]" the value "i" is prime, e.g. Sqrt[55] needs to be encoded to Sqrt[5]*Sqrt[11], otherwise we would need further describing polynomials "s55 = s5*s11".

Example: 3*Sqrt[55]/Sqrt[3] translates to 3*s5*s11*r3

The describing polynomials B={si^2-i,.. ri*si-1,..} generate an ideal I in the polynomial ring QQ [ri,si]. Informally said the ideal I is the set of polynomials which become zero if the elements of B become zero.

We now want to check if the polynomial p= -1 + (x1-x2)^2 + (y1-y2)^2 is contained in I, i.e. has the same roots.

Therefore we need to have a Groebner basis G of I, because if we know a Groebner basis for an ideal I we can decide ideal membership by applying multivariate division with remainder, i.e. we divide p by the elements of G until no further division is possible. If the unique remainder is equal to zero than p is contained in I.

For the Groebner basis calculation we need to define a variable ordering and there we use the convention that for any pair "ri, si" it holds that "ri" > "si".

Download

Python script for rewriting the graph: [ check_dist_one.zip ]

Singular can be downloaded here.

Usage

The zip-file contains a python file (check_dist_one.py) which takes the vertices and edges as input, rewrites the vertices, defines the ideal and adds a calculation instruction for each edge. The output is a file which can be passed on to the computer algebra system Singular, where the actual reduction is applied.

'python3 check_dist_one.py file.vtx file.edge'

'Singular file.singular'

PAC Proofs

For checking that the verification is correct, we generate polynomial proofs in the PAC format which are then verified by our proof checker PacTrim. Proofs in the PAC format generate the polynomial p as a linear combination of the polynomials B resp. G using polynomial addition and multiplication rules. A precise definition of the proof format can be found in the paper [ A Practical Polynomial Calculus for Arithmetic Circuit Verification | bibtex ].

Example

[ Running example including log files ]

[ (Checked) PAC proofs for running example ]