Maximizing sum of And()ed BoolVars in Python ortools

Given a set of cards, I have a list of combos that each involve one or more of these cards. I want to find a subset of these cards of a fixed size (DECKSIZE), that optimizes the number of combos that can be played using the chosen cards (the number of combos that include only the chosen cards is maximized).

cards = [BoolVar("card1"), BoolVar("card2"), BoolVar("card3"), BoolVar("card4")]

combos = [
    [cards[0], cards[1]],
    [cards[0], cards[2]],
    [cards[1], cards[3]],
    [cards[0], cards[2], cards[3]]
]

DECKSIZE = 3
solver.Add(sum(cards)==DECKSIZE)

num_combos = sum([And(combo) for combo in combos])

solver.Maximize(num_combos)

print("chosen cards:", [card for card in cards if card.solution_value()])

Is there a way to express this maximization problem with ortools? I managed to do this with z3py but perhaps ortools is faster.

Solution

for each combination, add a BoolVar equal to the and (or product) of bool vars.

See: https://github.com/google/or-tools/blob/stable/ortools/sat/docs/boolean_logic.md#product-of-two-boolean-variables

Note that this can easily be extended to any number of variables.

Then maximize the sum of the new variables:

from ortools.sat.python import cp_model

model = cp_model.CpModel()
cards: list[cp_model.IntVar] = [
    model.new_bool_var("card1"),
    model.new_bool_var("card2"),
    model.new_bool_var("card3"),
    model.new_bool_var("card4"),
]

combos: list[list[cp_model.IntVar]] = [
    [cards[0], cards[1]],
    [cards[0], cards[2]],
    [cards[1], cards[3]],
    [cards[0], cards[2], cards[3]],
]

DECKSIZE: int = 3
model.add(sum(cards) == DECKSIZE)

valid_combos: list[cp_model.IntVar] = []
for combination in combos:
    is_valid = model.new_bool_var("")

    # All true implies is_valid.
    model.add_bool_and(is_valid).only_enforce_if(combination)

    # is_valid implies all true.
    for literal in combination:
        model.add_implication(is_valid, literal)
    valid_combos.append(is_valid)

model.maximize(sum(valid_combos))

solver = cp_model.CpSolver()
solver.parameters.log_search_progress = True
status = solver.solve(model)

if status == cp_model.OPTIMAL:
    print("chosen cards:", [card.name for card in cards if solver.boolean_value(card)])