SatPack: a SAT encoding of the orthogonal packing problem

SatPack encodes S.P. Fekete and J. Schepers modelization of OPP in the two-dimensional case. SatPack generatesa SAT formula which can be solved using a SAT solver. A solution of the formula corresponds to a solution of S.P. Fekete and J. Schepers modelization.

Read: Stéphane Grandcolas - Cédric Pinto "A SAT Encoding for Multi-dimensional Packing Problems", Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR 2010), pp. 141-146, Bologna, Italy, 2010.

Download: SatPack for PC x86_64 on Linux.

generates the formula:
$ ./satpack -file benchs-clautiaux/E04F19.txt > E04F19.fomula
solves the SAT formula with an external solver
$ minisat E04F19.formula E04F19.sol
verifies that the solution of the formula is a solution of the packing problem
$ ./satpack -file benchs-clautiaux/E04F19.txt -validate E04F19.sol

This work is supported by the Region Provence-Cote d'Azur and the ICIA Technologies company.