3.7.216. SAT

A constraint for which a reference provides a reformulation in SAT. Encoding for the πšŠπš•πš•πšπš’πšπšπšŽπš›πšŽπš—πš and the πšŠπš–πš˜πš—πš constraints were respectively provided inΒ [GentNightingale04] and inΒ [Bacchus07]. Based on Fekete et al. model of the multi-dimensional orthogonal packing problemΒ [FeketeSchepersVeen07], an encoding for the πšπš’πšπšπš— constraint when all the sizes of all the orthotopes are fixed was described inΒ [GrandcolasPinto10].