Solving the Problem with SAT

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, p₁ ), (c, p₂ ), (c, p₃ ), ... (c, p_n ) corresponding to the variables x₁, x₂, x₃, ... x_n 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

x₁ v x₂ v x₃ v ... v x_n

In this way clauses for all 125 cells are defined.

If two arbitrary variables x_a and x_b correspond to the pairs ( c_a, p_a) and ( c_b, p_b) and the intersection of the positions p_a and p_b is not empty then x_a and x_b cannot both be true (unless p_a= p_b ). This is equivalent to the clause

¬ x_a v ¬ x_b

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 x_a and x_b such that the positions p_a and p_b are adjacent in a way that a spike exchange is possible. Since we want to avoid this we again add the clause ¬ x_a v ¬ x_b.

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.

< Home > <Description> <5 isolated Solutions>

© 2018  Herbert Kociemba