## 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, p x In this way clauses for all 125 cells are defined. If two arbitrary variables x ¬ x 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 |

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 |