Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.

Doing better requires thinking differently. Traditionally, solvers want to have as little state as possible. Less state means fewer errors and less backtracking, and everything runs faster. But not here. With SAT, it makes more sense to add in many extra variables. The goal is to express everything as sparse bit arrays, because sparse is an easy constraint. A better solution to the soup problem uses a 26x7 bit array and only needs 450 clauses to establish window([26 terms], 1, 1) across the seven soups and window([7 soups], 0, 1) across the 26 seats.

Mail: (not shown)

Please type this: