# Solving the Problem with SAT

There are 960 different positions p of an Y-pentomino in the 5x5x5 box. For each of the 125 cells c of the box there are up to 72 position p which share this cell. We define boolean variables for all the possible (c, p) pairs and get 4800 boolean variables.

A SAT solver has as input a formula in Conjunctive normal form (CNF) - usually coded in the DIMACS format.

If for a fixed cell c the possible (c,p) pairs are (c, p1 ), (c, p2 ), (c, p3 ), ... (c, pn ) corresponding to the variables x1, x2, x3, ... xn at least one of the variables has to be true because a cell may not be empty in the solution. This leads to the clause

x1 v x2 v x3 v ... v xn

In this way clauses for all 125 cells are defined.

If two arbitrary variables xa and xb correspond to the pairs ( ca, pa) and ( cb, pb) and the intersection of the positions pa and pb is not empty then xa and xb cannot both be true (unless pa= pb ). This is equivalent to the clause

¬ xa v ¬ xb

Checking all the 4800*4799 / 2 variable pairs leads to more than 1.5 million clauses.

Finally we add about 71000 clauses for all variable pairs xa and xb such that the positions pa and pb are adjacent in a way that a spike exchange is possible. Since we want to avoid this we again add the clause ¬ xa v ¬ xb.

Setting up the cnf-file takes about a second. I used sat4j SAT solver for the SAT part. When we take rotational symmetry into account there are only three cases for the position of the puzzle piece which covers the central cell of the 5x5x5 box. Only for one of these cases (the "spike" takes the position of the central cell) isolated solution exist.We got within an hour 10 solutions in 5 pairs which are related by a reflection. So essentially there are 5 isolated solutions

If you want you can take a look at the undocumented source code.

A generalized version which allows up to 8 arbitrary polycubes in an arbitrary sized box is here. I used it for example to find solutions for Y-pentacubes in a 5x5x4, 4x4x5, 4x5x3 and a 5x6x2 box.