py-yuclid 3.0.0

Python interface to Yuclid geometry solver

Yuclid

Yuclid is a fast plane geometry solver written in C++. It solves plane geometry problems like the ones that appear at IMO and other contests.

Yuclid is very fast: it solves 17 out of the 30 IMO problems from the AlphaGeometry benchmark and saturates the other 13 in less than 0.5s on a single Intel 3.1GHz core.

Yuclid uses STL and Boost libraries for generic utilities, including containers, safe numerics, and rational numbers.

Currently, it lacks a user-friendly interface, so the recommended way to use it is via Newclid. However, some of Yuclid's features are only available in C++.

Quickstart

The main user interface for Yuclid is Newclid. However, if you want to try some of the features that are not exposed via Newclid's interface, you can install it, generate a file in input format, and run

$ yuclid in-file.txt

This will show information about progress in solving the problem, then either print a solution, or say that it failed to solve the problem.

For automatic interaction with Yuclid, you can add --use-json, then the solution will be printed as a JSON object instead of plain text.

Note that the format of the JSON export is designed for Newclid, and can change in the future versions.

How does it work

Similarly to Alpha Geometry and Newclid 2.0, Yuclid uses deduction database (i.e., theorems from plane geometry) and algebraic reasoning, see below for more details.

First, it finds all theorems that match numerically on the diagram. Then, in a loop, it tries to prove the hypotheses and the conclusions of these matched theorems using already established statements and algebraic reasoning. This loop ends when either all goals of the problem are proved, or no new statements were established after going through all the theorems. In the latter case, the problem is "saturated", and can't be solved by DD/AR only.

The whole program is written aiming for higher speed. Here are some optimizations we use, besides writing the whole engine in C++.

• We numerically match theorems by matching certain common configurations (e.g., pairs of similar triangles, circumcenters etc), then adding all theorems about these configurations.
• The statements that appear in matched theorems are deduplicated, and we track the progress in proving each statement in the same object, no matter which theorem uses it as a hypothesis or a conclusion.
• Similarly, AR equations are deduplicated. Moreover, if we fail to prove an equation, then we store the row reduced form of this equation, so that next time we're trying to prove it we resume work instead of restarting it.

As a result of these optimizations of the solver, on a typical IMO problem, the main DD/AR loop is faster than numerically matching the theorems.

Features

The Yuclid engine is capable of

• applying rules from the Deduction Database (DD);
• performing algebraic reasoning (AR) on:
  • lengths (additive relations like |AB|+|BC|=|AC|);
  • squared lengths (additive relations like |AB|² + |BC|² = |AC|²);
  • lengths and sines of angles (multiplicative relations like |AB|:|BC|=|DE|:|EF| or the law of sines).

Extra AR tables allow us to state theorems like the law of sines and the Pythagoras theorem. Adding the law of sines to the mix makes Yuclid about 10x slower, so this feature is disabled by default.

Input format

Yuclid relies on a numerical graph of a problem to select theorems that apply in the problem and to verify the inequalities numerically. Currently, it expects the caller to build the graph.

An example input file looks like this

point a -0.40746902984670474446 -0.66665500610231753775
point b -0.11560335689440992546 -0.59371690741631888422
point g1 -0.44257354475251259318 -0.52618242659683756024
point g2 -0.17244267242498786952 -0.36627136967481344065
point m -0.40604502710432055501 -0.38607339777242094536
point n -0.30216699079418207763 -0.56155009778454667568
point c -0.54071880847663988945 -0.41972877579886108679
point d 0.043012537427953148605 -0.27385257842686294705
point e -0.27421925121677109827 -0.91358123640577104663
point p -0.032948325893715921242 -0.29283542382004185134
point q -0.77914172831492523041 -0.47931137172479987285
assume perp g1 a a b
assume perp g2 b b a
assume cong g1 m g1 a
assume cong g2 m g2 b
assume cong g1 n g1 a
assume cong g2 n g2 b
assume para c m a b
assume cong g1 c g1 a
assume para d m a b
assume cong g2 d g2 b
assume coll e a c
assume coll e b d
assume coll p a n
assume coll p c d
assume coll q b n
assume coll q c d
prove cong e p e q

Running yuclid < translated_imo_2000_p1.txt on this file produces a text proof. On the author's dev box (Intel(R) Xeon(R) CPU @ 3.10GHz), it takes 0.017s on a single core.

Python bindings

The module py_yuclid wraps a call to the yuclid command line utility in a Python interface which is just enough for Newclid to use it.

Only DD and the "multiplicative" AR without sines is exposed via Newclid at the moment.