Day 20 – Propositional combinatorics in Perl 6

Advent is an exciting time, a time of anticipation. And not only for us humans — it is the time when elves become most inventive. Today, I want to take some leisure time out of the Christmas stress to report about some pioneering work that is being done in the area of gift wrapping. Even if you didn’t anticipate any news from there, this report might still help you improve your technique, as — I don’t have to remind you — Christmas is approaching fast.

Do you know which presents small children like most? Large presents. Therefore, the Present Enlargement Research Lab at Northpole is tasked with finding practical ways to make presents larger. Now, “large” can mean multiple things. I will admit that the 6th unit is bending the meaning a bit, but their work is by far the most interesting: they increase the volume of presents, by increasing the dimension of the gift boxes.

«How are you supposed to wrap a 6-dimensional present?» is a valid question raised by management. It was as though genius struck the UX elf who responded: «Just wrap it so that from every 3d perspective it looks like a normal present» (a trick they actually learned from gaussoids, but who doesn’t want to be seen as the genius once in a while?). Management was satisfied, funding secured, and the math elves loved the complexity reduction proposed by the UX elf — it’s just that manufacturing technology is not quite there yet to produce those high-dimensional boxes. So they decided to do their programming in Perl 6, because what’s better to use when waiting for technology to catch up than a 100-year language?

«Let us get to work,» they said, and to work they got.

How do you wrap a gift, mathematically?

What I really took home from my stay at the lab was that there are only so many socially acceptable, or physically possible, ways to wrap a gift. First, you need a gift and then a box. You absolutely have to put gift wrap around the box. These steps are so natural that the elves take them for granted. For them, a “gift” is a gift inside a box wrapped with gift wrap. The challenge of “wrapping,” and the point that separates the packer from the virtuoso, is when ribbon and bows come into play. You think this should be easy enough? Well, think again!

A Cube Carol

A gift in this setting is modeled by the n-dimensional cube, or “n-cube” for short. The n-cube is a really nice thing because all of its faces are cubes in smaller dimensions. Computer scientists like it because its vertices are really just the strings of 0s and 1s of length n. Here, we care about the 2-dimensional faces, or “squares,” of the n-cube. The usual 3-cube has six squares, as you know from dice.

The approach taken by the elves treats these squares as variables and assigns to them

• nothing if this part of the gift box has only gift wrap on it, as we agreed to require,
• ribbon if there is gift ribbon running across it, or
• bow if there is a bow or loop on this side of the cube.

It’s time to see some code:

#|« A square on the n-cube with wrapping.
In the n-cube there are 3*(n choose 2)*2**(n-2) WrapSquare variables,
one for every square and every kind of value that can be assigned to it.
»
class WrapSquare is Cube::Face does Propositional::Variable {
    has $.kind is required;

    method WHICH {
        ValueObjAt.new: "WrapSquare|$!kind|{callsame}"
    }

    # ...
}

This snippet tells you that WrapSquare is a face of the cube, where the Cube::Face class implements much of the functionality that we expect from a cube face. It is also a type of variable and has a $.kind attribute which will hold the string □, ■ or , depending on which value (nothing, ribbon or bow) was assigned to this square.

There are some neat operators

multi prefix: (Str $s) {
    WrapSquare.new: :kind<□>,
        Cube::Face.from-word($s)
}

multi prefix: (Str $s) {
    WrapSquare.new: :kind<■>,
        Cube::Face.from-word($s)
}

multi prefix: (Str $s) {
    WrapSquare.new: :kind<>,
        Cube::Face.from-word($s)
}

which let you make WrapSquares by writing for instance ■<0**010>. The string 0**010 specifies a square in the 6-dimensional cube: let the * symbols in it be wildcards which vary between 0 and 1. Then you get four binary strings 000010, 001010, 010010 and 011010. Recall that binary strings of length n (here n = 6) are the vertices of the n-cube, and these four happen to bound a 2-dimensional face of it. These WrapSquare literals will later appear all over.

After all these explanations about WrapSquare, I can almost hear an itch in the back of your mind asking to be satisfied: «Why is the WrapSquare Variable Propositional?»

The Satisfying Tale of SAT-a-Clause

Recall that the suggestion of the UX elf was: «Just wrap it so that from every 3d perspective it looks like a normal present». While this sounds beautifully simple, it creates a very intricate problem.

«How many ways are there to wrap an n-dimensional gift?» was likely the first question the elves asked themselves. What the UX elf wants us to do is choose a proper 3d wrapping, in which the elves are experts already, for every 3-cube on the surface of the n-cube, but in a way that all these 3d wrappings fit together in the high-dimensional cube. The n-cube has ½n⋅(n-1)⋅2ⁿ⁻² squares but by choosing 3d wrappings, you make choices for ½n⋅(n-1)⋅(n-2)⋅2ⁿ⁻² squares, this is (n-2) times as many choices as you have variables. The reason for that is that the 3-cubes share squares with each other in the n-cube, just like in 3 dimensions, the sides of a dice have edges of the cube in common.

The problem created by the UX elf is to choose 3d wrappings for the 3-cubes on the n-cube which are compatible with each other wherever they have a common square. But how bad is this really? In dimension 4, you have 24 squares, so 3²⁴ = 282,429,536,481 ways of choosing a wrapping. If you did it at random, your chance of finding a UX-approved wrapping is not even 0.0000007%. There are exactly 1848 of those proper wrappings, as we will see.

«How can we possibly explore such a gigantic space?» — the elves were shocked. Until they found out about SAT solvers. SAT refers to the Propositional SATisfiability Problem, the task of deciding whether a formula using Boolean variables and operations has an assignment which makes the formula true, “satisfies” it. This problem is NP-complete but SAT solvers can still accomplish incredible feats.

It turns out that gift wrapping can be turned into an instance of this type of satisfiability problem. For simplicity, the elves decided to allocate three Boolean variables for every square of the n-cube. They stand for whether this square is decorated with □, ■ or . Exactly one of these variables must be true. Then they encode the requirements that each 3-cube must contain a proper 3d wrapping and that the chosen wrappings are compatible in the n-cube into a propositional formula. They called the constituents of this formula the giftoid axioms — rules for wrapping higher-dimensional gifts.

There are solvers that go further than finding a single satisfying assignment (or determining the impossibility of finding one): they can return the exact number of such assignments or even list all of them. Just what the elves needed, and, luckily, propositional calculus and SAT solvers are available to Perl 6.

The input to SAT solvers is a Boolean formula in Conjunctive Normal Form. The Propositional module has a particularly nice implementation of that, although I might be biased:

method NNF {
    self.rewrite(
        (  ^:p ⇔ ^:q ) => { ($:p ⇒  $:q) ∧ ($:q ⇒ $:p) },
        (  ^:p ⇒ ^:q ) => { ¬$:p ∨  $:q },
        (¬(^:p ∨ ^:q)) => { ¬$:p ∧ ¬$:q },
        (¬(^:p ∧ ^:q)) => { ¬$:p ∨ ¬$:q },
        (¬¬^:p)        => {  $:p        },
    )
    andthen .squish
}

method CNF {
    self.NNF.rewrite(
        (^:p ∨ (^:q ∧ ^:r)) => { ($:p ∨ $:q) ∧ ($:p ∨ $:r) },
        ((^:q ∧ ^:r) ∨ ^:p) => { ($:p ∨ $:q) ∧ ($:p ∨ $:r) },
    )
    andthen .squish
}

The CNF method first turns the formula into an intermediate form, called Negation Normal Form and then turns it into CNF. Both of these methods use one of the central gears of the module, the rewrite method. As its name suggests, it rewrites a formula based on rules, which are given to it as pairs, e.g. (^:p ⇔ ^:q ) => { ($:p ⇒ $:q) ∧ ($:q ⇒ $:p) }. The key is a formula object, here just the equivalence ⇔ of two variables ^:p and ^:q, which is pattern-matched inside the entire formula. The “cap sigil” in front of the variables indicates that subformulas found on either side of an ⇔ operator should be captured inside named arguments p and q which are passed to the code block on the right-hand side of the pair fatarrow to determine what the replacement of the ⇔ expression is. In this case, the equivalence is replaced by two implications — this rewrite rule implements the definition of ⇔. The next rule above implements the definition of ⇒. Indeed, both of these symbols must be eliminated, among other things, if you want an NNF.

The rewrite engine performs all listed rewrites until it couldn’t find any more matches. Now, logicians will tell you that if you do precisely that, you will turn any propositional formula into CNF. This should suffice from the internals. Let’s axiomatize gifts!

More than you ever wanted to know about 3d gift wrapping

Seeing all the high-level ingredients fall into place and everyone getting advently excited, I had to pause and ask: «What about the base case? How do you wrap a 3d gift?». Ask this to an elf and their eyes to start glow. It is second nature to them, even the research elves. Those are the rules that every elf learns in school:

• Just wrapping: It’s fine for a gift to have no ribbon or bow at all, but never forget the gift wrap,
• Glued bow: it can have a single bow glued on one side and no ribbon,
• Ribbon belt: if you use ribbon, you have to wrap it on a “belt” around the box,
• Bow belt: you can incorporate a bow into a ribbon belt,
• One bow: you may only use one bow or none,
• Disambiguation: if all sides have ribbon, there must be a bow.

The last axiom is different from the others. It is not part of the elementary school wrappification tables and was discovered later by the elves working on higher-dimensional wrapping. (Maybe one day is will make its way into the curriculum?) The “squares of the cube” formulation is a simplification when talking about ribbons, since there are two ways a ribbon can wrap a given square of the cube, vertically or horizontally. The Ribbon belt axiom takes care of defining the orientation of the ribbon in case there is only one belt. Similarly, there are really three ways to wrap ribbon around a cube so that all result in every side being touched by ribbon, namely one possibility for each way to pick two belts out of the three in total. Consequently, this “wrapping” of the cube is ambiguous and must be forbidden. The Disambiguation axiom places a bow on one of the sides, which specifies where the ribbon belts cross, just like in reality.

The Propositional package can take any object that does the Propositional::Variable role as a variable in a formula. The usual logical connectives are overloaded, as shown above, so that you can write a formula in a Perl 6 program almost like you would on paper. To require only a variable role is a significant design decision and has some neat implications. For instance, the rewrite captures ^:p that we have seen earlier, are also Propositional::Variable objects which behave specially when smartmatched.

In the elves’ case, the Variable is the WrapSquare class and another advantage of allowing arbitrary objects as variables reveals itself: arbitrary variables can have arbitrary methods or operators acting on them. The elves use this to accomplish another complexity reduction. They only have to axiomatize one corner of the 3-cube and then act with the symmetry group of the 3-cube. This group action moves the axiomatized corner into every corner of the cube, so concatenating the orbit of that action gives a full axiomatization of 3d gift wrapping. Now that we agree that this sounds awesome, let’s see how it is done in Perl 6. (Note: the axiomatization involves logical connectives which you may want to get familiar with and follow along with the human-readable axioms above.)

multi axioms ($n = 3) {
    my \φ = .CNF with [∧] gather {
        take □<**0> ∨ ■<**0> ∨ <**0>;
        take □<**0> ⇒ ¬(■<**0> ∨ <**0>);
        take ■<**0> ⇒ ¬(□<**0> ∨ <**0>);
        take <**0> ⇒ ¬(□<**0> ∨ ■<**0>);

We pick the 2-dimensional face **0 as our specific corner to axiomatize. There are three Boolean variables associated with it, namely □<**0>, ■<**0> and <**0> (conveniently, they can also be called that in the Perl 6 code, thanks to our WrapSquare constructor operators). To have a well-defined wrapping, at least one of those three variables must be set.

The axiom □<**0&> ∨ ■<**0> ∨ <**0> says that at least one of the three variables must be set. The next axiom □<**0> ⇒ ¬(■<**0> ∨ <**0>) rules that if □<**0> happens to be active (meaning there is only gift wrap on the square), then (⇒) it cannot (¬) be true that ■<**0> or (∨) <**0> are also set. Any satisfying assignment, that a SAT solver will find for us, to the final formula will fulfill this axiom, as we take a big AND over the gather block.

You are invited to trace the other formulas back to the wrappification table:

        take ■<**0> ⇒ (■<**1> ∨ <**1>);
        take (■<**0> ∧ ■<**1>) ⇒ (■<*0*> ∨ <*0*> ∨ ■<0**> ∨ <0**>);
        take (<**0> ∧ ■<**1>) ⇒ (■<*0*> ∨ ■<0**>);
        take (<**0> ∧ (■<*0*> ∨ ■<0**>)) ⇒ ■<**1>;
        take <**0> ⇒ ¬(<**1> ∨ <*0*> ∨ <*1*> ∨ <0**> ∨ <1**>);
    }

Now that we axiomatized one corner of the 3-cube, we act with the hyperoctahedral group. This can be implemented by a combination of the so-called duality, which is the &postfix:<°> operator implemented for Cube::Face, and permutation of the axes of the cube, for which the &infix:<⤩> operator exists.

    my \ψ = φ.rewrite(:1ce,
        (^:s(WrapSquare)) => { $:s° }
    );
    return [∧] gather for (1,2,3).permutations -> \π {
        take (φ ∧ ψ).rewrite(:1ce,
            (^:s(WrapSquare)) => { $:s ⤩ π }
        );

The rewrite method shines again here. The capture variables can be constrained with a smartmatcher, such as the type WrapSquare. They will only match and capture what matches the constraint. Thus the above rewrite rules only act on the variables in the formula and they only do it :1ce — because otherwise the rewrite engine would keep rewriting the same variables over and over because they match anew in every iteration.

Did you notice anything? It looks like the elves forgot the Disambiguation axiom. But — it was not forgotten. It is already symmetric and didn’t have to participate in the symmetrization process above. If it did, it would just be needlessly repeated. Here it comes:

        LAST take ¬(■<**0> ∧ ■<**1> ∧ ■<*0*> ∧ ■<*1*> ∧ ■<0**> ∧ ■<1**>);
    }
}

Finally the 3-dimensional gift wrapping axioms are complete. The elves dance gleefully.

Wrapping it up

Let’s summarize. To wrap higher-dimensional gifts, we wrap 3-dimensional gifts and puzzle the wrappings together. To axiomatize 3-dimensional wrappings, it is sufficient to axiomatize around one of its corners and turn the cube around and repeat the process, so that every corner of the cube was the axiomatized corner once. This gives a Boolean formula describing all the proper wrappings.

But hey, we aren’t done quite yet! Where are the giftoids and the SAT solvers? To axiomatize n-giftoids, the 3-cube axiomatization constructed above has to be replicated in every 3-face of the n-cube. Another Cube::Face operator shows up here, again in a rewrite. It embeds a square into some 3-face of the n-cube, just what we needed:

multi axioms ($n where * > 3) {
    my \Φ = axioms;
    [∧] gather for Faces($n, 3) -> \Δ {
        take Φ.rewrite(:1ce,
            (^:s(WrapSquare)) => { $:s  Δ }
        )
    }
}

Using the SAT facilities of Propositional, we can now get the real numbers of 3-, 4- and 5-giftoids:

say count-sat Giftoid::axioms(3), :now;
#= OUTPUT: 28
say count-sat Giftoid::axioms(4), :now;
#= OUTPUT: 1848
say count-sat Giftoid::axioms(5), :now;
#= OUTPUT: 58213276

To have a feeling for the amazing work the SAT solver did, consider that it found the number of 28 3-giftoids among 729 possibilities, the 1848 4-giftoids among 282429536481 possibilities and the 58213276 5-giftoids among a whooping total of 147808829414345923316083210206383297601 possibilities.

What you should know when you try the code examples above yourself is that SAT solvers, and in particular counters, are very memory-hungry. 5-giftoid counting needs 5:14 processor minutes with 4 GiB RAM on my laptop, not without swapping, but it can be done on a laptop! Most of the solvers allow time and memory use to be constrained but solver configuration is not yet implemented in the Perl 6 modules.

What is definitely feasible is getting a list of 3-giftoids where the assignments to all the six squares of the 3-cube are listed in a particular order:

.put for all-sat(Giftoid::axioms).map({ Giftoid.new: n => 3, deco => $_ })
#=« OUTPUT:
■■■■■
□□■■■
■■■■■
■■■■■
■■■■■
■■■■■
□□■■■
□□■■■
□□■■■
□□■■■■
■■□□■
■■□□■
...
»

or determine the mean number of bows in giftoids of a fixed dimension, although you won’t come too far with these:

sub mean-bows ($n) {
    my ($sum, $count);
    all-sat(Giftoid::axioms($n)).map({
        $sum += +.keys.grep(*.kind eq <>);
        $count++;
    });
    $sum / $count;
}

say mean-bows(3);
#= OUTPUT: 0.857143
say mean-bows(4);
#= OUTPUT: 2.766234

The budget elf cautiously raises a question: «If you increase the dimension of giftoids arbitrarily, does this mean stay bounded? Bows are the most expensive ones, after all…»

I’ll let you ponder this question over the holidays. Happy wrapping.