Solving a corn puzzle with CP-SAT

This describes using Google's OR-Tools CP-SAT solver to solve a 3D "corn" packing puzzle: a grooved cob and many multi-kernel pieces that must slide in with no overlaps or gaps. Instead of recursive backtracking, the puzzle is modeled with binary variables that represent each distinct placement of each piece. Two families of constraints enforce a valid solution: for every piece exactly one of its placement variables must be true, and for every cob cell exactly one covering placement must be true. The heavy lifting is enumerating all possible placements for each piece; once those are generated, the solver invocation is just a few straightforward additions of sum-equals-one constraints and a call to solve. An assistant-produced Python script handled the enumeration and produced a working model quickly.

To reinforce the approach, a classic Sudoku example is shown as an easier, analogous CP-SAT application: integer variables for cells constrained by all-different on rows, columns and boxes, which the solver resolves rapidly. The practical lesson is concrete: for constraint-heavy, exact-cover-style puzzles, model the variables and constraints and rely on an industrial CP-SAT solver rather than hand-rolled search. Links provided include the conversational exchange, the solver scripts, and slides from a short talk.