SAT: optimal interval selection

We are tasked with the following:

Cut rectangular slices of pizza. The pizza is divided into cells. Each slice must contain at least L tomato cells (T) and L mushroom cells (M). Each slice must contain at most H cells [1]. Maximize the total number of cells in the cuts. Example pizza:

TTTTT
TMMMT
TTTTT

L = 1, H = 6

Optimal solution:

TT | T | TT
TM | M | MT
TT | T | TT

I want to find (almost) optimal solutions using SAT. In this first version, I reduce it to a 1D problem, assuming that we only cut row by row. In other words, no slice cover more than one row.

Some problem analysis:

• Without involving the SAT solver, we can calculate which slices are allowed in the solution.
• Also without invoking in SAT, we can calculate which slices cannot overlap. 
• Determining which cells are covered by which slices can also be done easily without modelling. 
• With all this data known beforehand, we can reduce the slicing to something very abstract. We can see it as a selection problem: select some elements of a set with some mutual constraints and some objective. 

The key here is that the mutual constraints and the objective can be easily expressed using clauses. First we enumerate all feasible slices. Then, for each pair of slices (s_0, s_1), we add the following clause if they overlap:


For each cell, c, we find the slices s_0, s_1,...s_k that overlap it. Then for each cell we add an indicator:

Now we want to find the largest S such that adding

is satisfiable. For this, we can use pysat's ITotalizer [2]. It is based on technology that allows for some optimizations when trying different values of S [3]. I applied it to a binary search. The code:

For the instances medium.in and big.in in the input data [1], this algorithm can solve row-wise optimality in reasonable time. Sample output medium.in (max score is 250):

Row time: 0.510
Row score: 250

Row time: 0.484
Row score: 242

Row time: 0.519
Row score: 247

Sample output big.in (max score is 1000):

Row time: 4.096
Row score: 880

Row time: 3.108
Row score: 904

Row time: 3.336
Row score: 881

For medium I get a total score of 48977, which is not particularly good, because it can be beaten by a greedy algorithm (49567) [4]. The max score is 50000 (250x200). Still, it is interesting that we get so close to the real optimum with such a silly constraint as row-wise maximization. 

[1] pizza.pdf
[2] PySAT: SAT technology in Python
[3] Martins, Ruben, et al. "Incremental cardinality constraints for MaxSAT." International Conference on Principles and Practice of Constraint Programming. Springer, Cham, 2014.
[4] sagishporer/hashcode-practice-pizza