Logic grid puzzles: how to encode "x is older than y"?

[MarcelloTheArcane]

I'm trying to solve logic grid puzzles using the python SAT solver. For example, this puzzle: https://www.brainzilla.com/logic/logic-grid/kart-racing/

If you're not familiar with these, it's where you have several lists of attributes, and you have to find the correct combination from a given list of clues. My code is inspired by https://wjholden.com/reindeer.html, where each attribute is given a boolean variable.

The thing I'm struggling with is clues like "Alan is one year younger than the pilot who finished third". The code I've come up with is this, but it doesn't feel right since there's a lot of manual variables:

## Alan is one year younger than third
third_is_16 = model.new_bool_var("third_is_16")
third_is_15 = model.new_bool_var("third_is_15")
third_is_14 = model.new_bool_var("third_is_14")
model.add_at_least_one([combinations[name, 16, "Third"] for name in names]).only_enforce_if(third_is_16)
model.add_at_least_one([combinations[name, 15, "Third"] for name in names]).only_enforce_if(third_is_15)
model.add_at_least_one([combinations[name, 14, "Third"] for name in names]).only_enforce_if(third_is_14)
alan_is_15 = model.new_bool_var("alan_is_15")
alan_is_14 = model.new_bool_var("alan_is_14")
alan_is_13 = model.new_bool_var("alan_is_13")
model.add_at_least_one([combinations["Alan", 15, position] for position in positions]).only_enforce_if(alan_is_15)
model.add_at_least_one([combinations["Alan", 14, position] for position in positions]).only_enforce_if(alan_is_14)
model.add_at_least_one([combinations["Alan", 13, position] for position in positions]).only_enforce_if(alan_is_13)
alan_is_15_third_is_16 = model.new_bool_var("alan_is_15_third_is_16")
alan_is_14_third_is_15 = model.new_bool_var("alan_is_14_third_is_15")
alan_is_13_third_is_14 = model.new_bool_var("alan_is_13_third_is_14")
model.add_bool_and([alan_is_15, third_is_16]).only_enforce_if(alan_is_15_third_is_16)
model.add_bool_and([alan_is_14, third_is_15]).only_enforce_if(alan_is_14_third_is_15)
model.add_bool_and([alan_is_13, third_is_14]).only_enforce_if(alan_is_13_third_is_14)
model.add_at_least_one([alan_is_15_third_is_16, alan_is_14_third_is_15, alan_is_13_third_is_14])

Is there a better way of writing this?

The complete code is here within this dropdown:

Complete code (click to reveal)

# https://www.brainzilla.com/logic/logic-grid/kart-racing/

from ortools.sat.python import cp_model
import itertools
import math

model = cp_model.CpModel()

names = ("Alan", "Fred", "Sam", "Ronald")
ages = (13, 14, 15, 16)
positions = ("First", "Second", "Third", "Fourth")

combinations = {}

for (name, age, position) in itertools.product(names, ages, positions):
    combinations[(name, age, position)] = model.new_bool_var(f"{name}_{age}_{position}")

for name in names:
    model.add_exactly_one(combinations[(name, age, position)] for (age, position) in itertools.product(ages, positions))

for age in ages:
    model.add_exactly_one(combinations[(name, age, position)] for (name, position) in itertools.product(names, positions))

for position in positions:
    model.add_exactly_one(combinations[(name, age, position)] for (name, age) in itertools.product(names, ages))

# The pilot who finished first is older than Sam
## Sam did not finish first
for age in ages:
    model.add(combinations[("Sam", age, "First")] == False)
## Sam is not 16
for position in positions:
    model.add(combinations[("Sam", 16, position)] == False)
## First is not 13
for name in names:
    model.add(combinations[(name, 13, "First")] == False)

# Ronald is 13 years old
model.add_at_least_one([combinations[("Ronald", 13, position)] for position in positions])

# Sam finished in second place
model.add_at_least_one([combinations[("Sam", age, "Second")] for age in ages])

# Alan is one year younger than the pilot who finished third.
## Alan is not 16
for position in positions:
    model.add(combinations[("Alan", 16, position)] == False)
## Alan is not third
for age in ages:
    model.add(combinations[("Alan", age, "Third")] == False)
## Third is not 13
for name in names:
    model.add(combinations[(name, 13, "Third")] == False)
## Alan is one year younger than third
third_is_16 = model.new_bool_var("third_is_16")
third_is_15 = model.new_bool_var("third_is_15")
third_is_14 = model.new_bool_var("third_is_14")
model.add_at_least_one([combinations[name, 16, "Third"] for name in names]).only_enforce_if(third_is_16)
model.add_at_least_one([combinations[name, 15, "Third"] for name in names]).only_enforce_if(third_is_15)
model.add_at_least_one([combinations[name, 14, "Third"] for name in names]).only_enforce_if(third_is_14)
alan_is_15 = model.new_bool_var("alan_is_15")
alan_is_14 = model.new_bool_var("alan_is_14")
alan_is_13 = model.new_bool_var("alan_is_13")
model.add_at_least_one([combinations["Alan", 15, position] for position in positions]).only_enforce_if(alan_is_15)
model.add_at_least_one([combinations["Alan", 14, position] for position in positions]).only_enforce_if(alan_is_14)
model.add_at_least_one([combinations["Alan", 13, position] for position in positions]).only_enforce_if(alan_is_13)
alan_is_15_third_is_16 = model.new_bool_var("alan_is_15_third_is_16")
alan_is_14_third_is_15 = model.new_bool_var("alan_is_14_third_is_15")
alan_is_13_third_is_14 = model.new_bool_var("alan_is_13_third_is_14")
model.add_bool_and([alan_is_15, third_is_16]).only_enforce_if(alan_is_15_third_is_16)
model.add_bool_and([alan_is_14, third_is_15]).only_enforce_if(alan_is_14_third_is_15)
model.add_bool_and([alan_is_13, third_is_14]).only_enforce_if(alan_is_13_third_is_14)
model.add_at_least_one([alan_is_15_third_is_16, alan_is_14_third_is_15, alan_is_13_third_is_14])

# Enumerate all solutions, to verify that a unique solution is found.
solver = cp_model.CpSolver()
class VarArraySolutionCollector(cp_model.CpSolverSolutionCallback):
    def __init__(self, combinations, keys):
        cp_model.CpSolverSolutionCallback.__init__(self)
        self._combinations = combinations
        self._keys = keys
        self.solution_list = []

    def on_solution_callback(self):
        solution = [
            k for k in itertools.product(*self._keys)
            if self.Value(self._combinations[k])
        ]
        self.solution_list.append(solution)

solution_collector = VarArraySolutionCollector(combinations, (names, ages, positions))
solver.SearchForAllSolutions(model, solution_collector)
solution_count = len(solution_collector.solution_list)
if solution_count == 1:
    print("Solution found:")
    solution = solution_collector.solution_list[0]
    print(f"{solution[0]} is {solution[1]} years old and finished {solution[2]}")
elif solution_count == 0:
    print("No solution found")
elif solution_count < 10:
    print(f"Found {solution_count} possibilities:")
    for candidate in solution_collector.solution_list:
        for s in candidate:
            print(f"  {s[0]} is {s[1]} years old and finished {s[2]}")
        print("")
else:
    print(f"Found {solution_count} possibilities")

[MarcelloTheArcane]

In another puzzle, there's the constraint "Rachel carried 4 more apples than the girl who used the red basket". I've written the following code for this, but it looks a bit excessive!

# Rachel carried four more apples than the girl that used the red basket

# If Rachel collected 24...
name_rachel_amount_24 = model.new_bool_var("name_rachel_amount_24")
model.add_at_least_one(combinations[v] for v in itertools.product(names, amounts, colours) if v[0] == "Rachel" and v[1] == "24").only_enforce_if(name_rachel_amount_24)
model.add(sum(combinations[v] for v in itertools.product(names, amounts, colours) if v[0] == "Rachel" and v[1] == "24") == 0).only_enforce_if(name_rachel_amount_24.Not())

# ...then red collected 20
colour_red_amount_20 = model.new_bool_var("colour_red_amount_20")
model.add_at_least_one(combinations[v] for v in itertools.product(names, amounts, colours) if v[2] == "red" and v[1] == "20").only_enforce_if(colour_red_amount_20)
model.add(sum(combinations[v] for v in itertools.product(names, amounts, colours) if v[2] == "red" and v[1] == "20") == 0).only_enforce_if(colour_red_amount_20.Not())

model.add(colour_red_amount_20 == 1).only_enforce_if(name_rachel_amount_24)
model.add(colour_red_amount_20 == 0).only_enforce_if(name_rachel_amount_24.Not())

name_rachel_amount_24_colour_red_amount_20 = model.new_bool_var("name_rachel_amount_24_colour_red_amount_20")
model.add_bool_and([name_rachel_amount_24, colour_red_amount_20]).only_enforce_if(name_rachel_amount_24_colour_red_amount_20)
model.add(sum([name_rachel_amount_24, colour_red_amount_20]) == 0).only_enforce_if(name_rachel_amount_24_colour_red_amount_20.Not())

# If Rachel collected 26...
name_rachel_amount_26 = model.new_bool_var("name_rachel_amount_26")
model.add_at_least_one(combinations[v] for v in itertools.product(names, amounts, colours) if v[0] == "Rachel" and v[1] == "26").only_enforce_if(name_rachel_amount_26)
model.add(sum(combinations[v] for v in itertools.product(names, amounts, colours) if v[0] == "Rachel" and v[1] == "26") == 0).only_enforce_if(name_rachel_amount_26.Not())

# ...then red collected 22
colour_red_amount_22 = model.new_bool_var("colour_red_amount_22")
model.add_at_least_one(combinations[v] for v in itertools.product(names, amounts, colours) if v[2] == "red" and v[1] == "22").only_enforce_if(colour_red_amount_22)
model.add(sum(combinations[v] for v in itertools.product(names, amounts, colours) if v[2] == "red" and v[1] == "22") == 0).only_enforce_if(colour_red_amount_22.Not())

model.add(colour_red_amount_22 == 1).only_enforce_if(name_rachel_amount_26)
model.add(colour_red_amount_22 == 0).only_enforce_if(name_rachel_amount_26.Not())

name_rachel_amount_26_colour_red_amount_22 = model.new_bool_var("name_rachel_amount_26_colour_red_amount_22")
model.add_bool_and([name_rachel_amount_26, colour_red_amount_22]).only_enforce_if(name_rachel_amount_26_colour_red_amount_22)
model.add(sum([name_rachel_amount_26, colour_red_amount_22]) == 0).only_enforce_if(name_rachel_amount_26_colour_red_amount_22.Not())

# Either (Rachel collected 24 and red collected 20) or (Rachel collected 26 and red collected 22)
model.add_at_least_one([name_rachel_amount_24_colour_red_amount_20, name_rachel_amount_26_colour_red_amount_22])

PS, I'm using combinations[v] for v in itertools.product(names, amounts, colours) if v[0] == "Rachel" and v[1] == "24" instead of combinations[("Rachel", "24", colour)] for colour in colours because I'm trying to write a helper class so I can encode this type of constraint in one line rather than all this boilerplate.