ICFP 2010

This year, I took part in the ICFP Programming Contest as part of the team "cbv" (Cult of the Bound Variable). It was my first experience with a long-form programming contest, and I had a good time -- probably because the whole team was so fun to work with.

The rest of this post will make very little sense unless you read through the task description for the contest. Briefly, the contest involved creating systems of linear inequalities on matrix products (called "cars"), and matrices that satisfied these systems of inequalities (called "fuel"). Both cars and fuels needed to be encoded in trinary (base-three) strings, with the fuels further encoded as a network of 2-in 2-out trinary logic gates.

Over the course of the contest I wrote a few solvers (simple randomized search and exhaustive enumeration) that could generally succeed on 2x2's and the occasional 3x3 solution, as well as an ILP-based solver that could find almost all 1x1 solutions in a few seconds. These weren't the heaviest solvers we deployed, but they did manage to mop up probably 60-65 percent of the cars submitted to the contest.

However, probably the most useful thing I did during the contest was to write our second fuel-encoding program. It was about 3am Saturday; I had just gotten home and was taking a quick shower before bed, thinking about the contest. At this time, we already had a perfectly serviceable encoder which, unfortunately, required something between seven and fifteen gates for each trit. The large number of gates was a result of our encoding strategy relying on lots of constant generators.

What I realized in the shower was that, with the proper back-edges, the only values you care about are those your gates produce on the first tick. And -- better yet -- on the first tick you get as many zeroes as you want (back-edges from other gates) for free. I decided this would probably be my last real contribution to the team, so I set to work, finishing up around 10am (and -- as expected -- destroying myself for the remainder of the competition). In a fit of not-quite-movie-referencing, I called the final product gates motel.

Overview

Gates motel encodes a string of n trits using between 6 + n and 7 + 2n gates. Six of these gates are a zeroer (whatever in, zeroes out) to force a known input stream. Figuring out the server's input beyond the first 17 trits (X::X is a handy factory, by the way) would have allowed these six gates to be removed. The runtime of the encoder is O(n²), though an O(n) seems doable if one is clever.

You can download the source here. I describe the gist of the algorithm below.

The Problem

The goal of a fuel encoding program is to take a given string of trinary numbers and create a network of 2-in, 2-out logic gates to encode the string. This is complicated by three tricky things. The first tricky thing is that the only type of gate allowed is one that takes numbers x and y and outputs x - y and xy-1. Here's a picture of one of these fellows:

Input and output are handled through a special 0-in 1-out "input from world" gate and a special 1-in 0-out "output to world" gate. The second tricky thing is that no fan-out is allowed (that is: each input connects to exactly one output and each output connects to exactly one input). The third tricky thing is that the values appearing on the input gate each tick are unknown.

Gates are executed in a fixed order you get to choose (in my pictures this will always be top-to-bottom). When a gate is executed, it recomputes its output values from its input values. The outputs of all gates are initialized to zero at the beginning of execution.

As an example, this circuit, due to jcreed, takes as input an arbitrary string and produces a string of zeros:

The Algorithm

Gates motel builds an encoding circuit top-to-bottom, chunk-by-chunk. Before I get into how the details, let me introduce you to six special groups of gates:

The Z group is the aforementioned zeroer. One will be used in every circuit.

The remaining groups will be selected based on the input string. Each group has two inputs and two outputs. The left output is the "control" output. Each block is designed so that on the first tick the control output will take a specific value. The right output is the "junk" output. It takes an arbitrary value. The left input is the "junk" input. It will take a known value from the portion of the circuit above this group. The right input is the "control" input. Each group is designed such that by setting the control input to 0,1, or 2 the control output will assume 0,1, and 2 (in some permutation, which may change per-tick).

Additionally, given a certain "junk" input and a "control" input of zero, it is possible to get 0, 1, or 2 on the "control" output by choosing groups as follows:

		Control output
		0	1	2
Junk input	0	E	1	2
	1	0	E	N
	2	0	N	E

Gates motel encodes a string of trits by building a chain of these groups, one group per trit. For instance, this chain happens to encode the string 0220:

What if we wanted to encode 02201? Notice that because of the "control output is dependent on control input" property, supplying input x to the last group after tick 1 selects the output of the first group after tick 5:

Of course, the sign of x and the offset d are not known -- but we can simply simulate the circuit thrice to discover them. In this case, an input of 1 is required.

Also by simulation, we can determine that when running the first tick the right output of the current last group will be 2. So we need to add a group that will take a 2 on its junk input and a zero on its control input and produce a 1 on its control output. It turns out that N is such a group:

So this is an encoding of 02201.

The Groups

What are these magical groups? Here they are:

Notice that there is one special case to handle here: when the final group is a 0, an extra gate needs to be wired in between the junk output and the control input to ensure that it actually gets a zero on the first tick.

(Note: figures in this page available in a monolithic svg file if you are interested.)