## Solution to the FiveThirtyEight Riddler Classic puzzle for March 23, 2018

FiveThirtyEight’s weekly Riddler column has a really nice problem today:

From Joseph Converse, a puzzle of digital manipulation:

Imagine taking a number and moving its last digit to the front. For example, 1,234 would become 4,123. What is the smallest positive integer such that when you do this, the result is exactly double the original number? (For bonus points, solve this one without a computer.)

Here is the solution… (spoiler warning!)

## More problems that seem easy but are actually NP-hard

In the last post, I illustrated how the 0-1 integer linear programming problem can be reduced to solving a multivariate system of linear and quadratic polynomials over the complex numbers, demonstrating that the latter problem is NP-hard. Let’s see what other problems we can prove are NP-hard by reduction from 0-1 integer programming.

## How hard is determining whether an algebraic set is nonempty?

Suppose we are given a system of polynomial equations in $$n$$ variables, where each polynomial has degree at most $$d$$, and the coefficients are integers given as binary. We want to determine whether this system of equations has any solutions over the complex numbers. In other words, we want to determine whether the algebraic set specified by the system of polynomial equations is nonempty.

What computational complexity class class does this problem fall into? Can we do it in polynomial time if we take the degree $$d$$ to be a fixed constant?

As it turns out, this problem is NP-hard, even for $$d = 2$$. The proof is straightforward and requires no algebraic geometry or other “hard” math—you just have to know the trick.

## Exact (integer arithmetic only) capsule intersection test

The capsule (also called a “pill”) is one of a few common types of shape used for collision detection in games and other applications. A 3-D capsule is a cylinder capped by hemispheres. The 2-D equivalent, a rectangle capped by semicircles, is technically called a stadium, but they are commonly just called capsules as well. Capsules used for collision detection in Super Smash Bros. Melee. From here.

Capsules are nice because they can form both spherical and elongated shapes in any direction. The animation above shows how Super Smash Bros. Melee uses spherical hitboxes that are “stretched” across frames into capsules to prevent fast-moving attacks from going through opponents without hitting them. (Marvel vs. Capcom 3 uses the same trick.) What really makes capsules useful is that they have a very simple mathematical description: a capsule is the set of all points less than a certain radius from a line segment. This means you can check whether two capsules intersect each other by just finding the shortest distance between the two line segments and checking whether it is less than the sum of the radii.

Calculating the distance between two line segments is a well-known problem. This StackOverflow answer gives the code to do that with floating-point arithmetic. Sometimes, though, approximating the correct answer with floating-point isn’t good enough. What if we want an exact intersection test for capsules using only integer arithmetic?
Continue reading Exact (integer arithmetic only) capsule intersection test

## Propositional logic proofs are awful

In my last post, I gave an implementation for a program that searches through every proof in a particular proof notation for propositional logic, and collects all the theorems that it finds. The proof formalism used was Hindley–Milner, with types being the formulas of the theory and well-typed lambda terms the valid proofs (per the Curry–Howard correspondence).

The program’s output looked like this: \a. DoubleNegElim (\b. a) : forall a. False -> a. On the right side of the colon, we have our type/theorem: for every proposition $$a$$, $$\bot \rightarrow a$$. The notation there is about as good as you’re going to get in ASCII text. But then we have the proof, on the left side of the colon. It’s an inscrutable lambda term encoding a natural deduction proof. The type inference engine is filling in the steps in the proof based only on which deductive rules were used, with the result that, even if you know how to read the notation, you really have to stare at it for a while to figure out why the proof works. While this admittedly lends an aura of elegance and mystery to the proceedings, I think I’d prefer a proof that is comprehensible by a human without significant head-scratching.
Continue reading Propositional logic proofs are awful

## The shortest proof for every theorem

Suppose we want to show that there is a number $$n$$ such that no upper bound on the busy beaver number $$\Sigma(n)$$ is provable from, say, the axioms of ZFC. One possible proof is as follows: Assume that no such $$n$$ exists. That is, assume that for every $$n$$, there is a proof in first-order logic that uses only the axioms of ZFC and derives a sentence $$\Sigma(n) \leq m$$ for some $$m$$. Then we could compute an upper bound for $$\Sigma(n)$$ by exhaustively searching all of the possible valid ZFC proofs until we found one that deduced a theorem of the form $$\Sigma(n) \leq m$$; by assumption, we must eventually find such a proof. But we know that we cannot compute an upper bound on $$\Sigma(n)$$ for arbitrary $$n$$; thus, we have derived a contradiction, and the original assumption must be false.

Enumerating proofs until you find one with the desired properties is one of those grand CS traditions that, like calling an $$O(n^{12})$$ algorithm “efficient” while dismissing an $$O(1.001^n)$$ algorithm as “intractable”, is handy for theoretical purposes but has essentially no bearing on the real world whatsoever. After all, no one would really write a program that loops through all possible proofs and tests each one.