Sites like stackoverflow and math stackexchange are packed with people working on geometry intensive applications like games asking for code snippets to decide whether shapes do or don't overlap:

https://math.stackexchange.com/questions/166863/intersection-between-a-cylinder-and-an-axis-aligned-bounding-box

http://stackoverflow.com/questions/401847/circle-rectangle-collision-detection-intersection

http://stackoverflow.com/questions/22093749/c-plane-sphere-collision-detection

The answers are usually given by human ingenuity, but as the answerer of the first question listed above points out algorithms to solve these kinds of shape intersection problems can be automatically invented by a procedure called *cylindrical algebraic decomposition* (CAD).

CAD is the most popular algorithm used for *real quantifier elimination* (RQE). RQE takes any problem in nonlinear real arithmetic (first order logic where all the atomic formulas are real polynomial equations and inequalities) and spits out a logically equivalent formula with no quantifiers.

To get a feel for RQE here are some formulas and their quantifier free equivalents:

is

is

is

is

This procedure can be used to generate intersection tests for 2 shapes like so: Come up with a logical formula, , that is true when the point is in shape 1. Then come up with a formula, , that is true when the point is in shape 2. To find an intersection test perform quantifier elimination on:

and transliterate the resulting formula into the programming language of your choice.

This method can automatically generate intersection tests for any number of shapes, but before we get to that lets look at an example.

# Example: Circle Square Intersection

A formula using quantifiers to describe whether a circle centered at point with radius , and a square with bottom left corner at and side length intersect is:

where:

Using the quantifier elimination command in redlog we can produce a new formula that is logically equivalent to the original one, but does not contain or .

Since this formula only uses known values (, , , , , and ) and has no quantifiers it can be transliterated into an executable intersection test in a programming language of the users choice.

After using redlog to eliminate quantifiers we can pretty print the resulting formula as a c++ function:

#include<cmath>
bool test( const double r,
const double l,
const double b,
const double d,
const double a,
const double c ) {
return ( ( ( ( ( ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d >= 0.0 ) ) && ( b - d - l <= 0.0 ) ) && ( a - c - r >= 0.0 ) ) && ( a - c - l - r <= 0.0 ) ) || ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d >= 0.0 ) ) && ( b - d - l <= 0.0 ) ) && ( a - c + r >= 0.0 ) ) && ( a - c - l + r <= 0.0 ) ) ) || ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) || ( ( pow( b, 2 ) - 2.0 * b * d + pow( d, 2 ) - pow( r, 2 ) <= 0.0 ) && ( ( ( ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d >= 0.0 ) ) && ( a - c >= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + pow( d, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( b - d - l <= 0.0 ) || ( l * 2.0 * b - 2.0 * d - l >= 0.0 ) ) ) && ( ( a - c - l <= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) || ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d >= 0.0 ) ) && ( a - c - l <= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( b - d - l <= 0.0 ) || ( l * 2.0 * b - 2.0 * d - l >= 0.0 ) ) ) && ( ( a - c >= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + pow( d, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) ) || ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d - l <= 0.0 ) ) && ( l * 2.0 * b - 2.0 * d - l <= 0.0 ) ) && ( a - c >= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + pow( d, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( a - c - l <= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) ) || ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d - l <= 0.0 ) ) && ( l * 2.0 * b - 2.0 * d - l <= 0.0 ) ) && ( a - c - l <= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( a - c >= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + pow( d, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) ) ) ) || ( ( pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( d, 2 ) + 2.0 * d * l + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) && ( ( ( ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d >= 0.0 ) ) && ( l * 2.0 * b - 2.0 * d - l >= 0.0 ) ) && ( a - c >= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + pow( d, 2 ) + 2.0 * d * l + pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( a - c - l <= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) || ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d >= 0.0 ) ) && ( l * 2.0 * b - 2.0 * d - l >= 0.0 ) ) && ( a - c - l <= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( a - c >= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + pow( d, 2 ) + 2.0 * d * l + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) ) || ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d - l <= 0.0 ) ) && ( a - c >= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + pow( d, 2 ) + 2.0 * d * l + pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( b - d >= 0.0 ) || ( l * 2.0 * b - 2.0 * d - l <= 0.0 ) ) ) && ( ( a - c - l <= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) ) || ( ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d - l <= 0.0 ) ) && ( a - c - l <= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( b - d >= 0.0 ) || ( l * 2.0 * b - 2.0 * d - l <= 0.0 ) ) ) && ( ( a - c >= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + pow( d, 2 ) + 2.0 * d * l + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) ) ) ) || ( ( pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( d, 2 ) + 2.0 * d * l + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) && ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( a - c >= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + pow( d, 2 ) + 2.0 * d * l + pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( a - c - l <= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) || ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( a - c - l <= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( a - c >= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + pow( d, 2 ) + 2.0 * d * l + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) ) ) ) || ( ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( c, 2 ) + 2.0 * c * l + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) && ( ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d >= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( b - d - l <= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) || ( ( ( ( ( r != 0.0 ) && ( l != 0.0 ) ) && ( b - d - l <= 0.0 ) ) && ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d - 2.0 * b * l + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + 2.0 * d * l + 2.0 * pow( l, 2 ) - pow( r, 2 ) >= 0.0 ) ) && ( ( b - d >= 0.0 ) || ( pow( a, 2 ) - 2.0 * a * c - 2.0 * a * l + pow( b, 2 ) - 2.0 * b * d + pow( c, 2 ) + 2.0 * c * l + pow( d, 2 ) + pow( l, 2 ) - pow( r, 2 ) <= 0.0 ) ) ) ) ) ); }

As you can see, the result isn't pretty. The downside of automatically generated formulas is that there is no human intuition behind them to make them comprehensible.

# Other Shapes

In theory this method can handle just about any 3D shape. A few 3D shapes that can be handled with fairly compact formulas:

Spheres:

Axis aligned cubes and cuboids:

Axis aligned ellipses:

# Performance

Below are results for several other shape intersections

Shape Combination | Generated in under 10 seconds |

Circle-Square | Yes |

Circle-Circle | Yes |

Sphere-Cube | Yes |

Line-Line | Yes |

Ellipse-Line | Yes |

Ellipse-Square | Yes |

Circle-Ellipse | |

Ellipse-Rectangle | Yes |

Rectangle-Circle | Yes |

Sphere-Plane | Yes |

Sphere-Halfspace below plane | yes |

# Limitations

RQE is extremely slow. Any algorithm for RQE is at best , though there are specialized algorithms for the linear and quadratic cases that are faster in practice than general methods.

Redlog seems capable of generating intersection tests for 2D shapes, and some simple 3D shape combinations like sphere-cube intersection.

More complicated 3D shapes like cylinders seem out of reach for Redlog since the logical formulas that can be used to represent them have more variables and higher degree polynomials (4+) that are difficult to eliminate.

**Redlog code link**