pythonoptimizationor-toolscp-sat

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)])