Search code examples
pythonor-toolsinteger-programmingcp-sat

Obtain list of SAT solutions from ortools


I'm trying to figure out how to get the complete list of possible solutions from the ortools.sat.python.cp_model. I understand I can print them, as in the example below, but it is not clear to me how to get the values, e.g. as a nested list or list of dicts. I tried writing my own callback class by modifying the VarArraySolutionPrinter and appending solutions to a list attribute, but for some reason this consistently caused the python kernel to crash. Anyway, there must be a more direct way. I don't consider parsing the printed output an option.

from ortools.sat.python import cp_model

model = cp_model.CpModel()

x00 = model.NewBoolVar('x00')
x01 = model.NewBoolVar('x01')
x02 = model.NewBoolVar('x02')

model.AddBoolOr([x00, x01, x02.Not()])
model.AddBoolOr([x00.Not(), x02.Not()])

# Create a solver and solve.
solver = cp_model.CpSolver()
solution_printer = cp_model.VarArraySolutionPrinter([x00, x01, x02])
solver.SearchForAllSolutions(model, solution_printer)

## Prints:
Solution 0, time = 0.00 s
  x00 = 0   x01 = 1   x02 = 0 
Solution 1, time = 0.01 s
  x00 = 0   x01 = 0   x02 = 0 
Solution 2, time = 0.01 s
  x00 = 0   x01 = 1   x02 = 1 
Solution 3, time = 0.01 s
  x00 = 1   x01 = 1   x02 = 0 
Solution 4, time = 0.01 s
  x00 = 1   x01 = 0   x02 = 0 

Solution

  • Turns out writing a custom callback class works after all:

    from ortools.sat.python import cp_model
    
    model = cp_model.CpModel()
    
    x00 = model.NewBoolVar('x00')
    x01 = model.NewBoolVar('x01')
    x02 = model.NewBoolVar('x02')
    
    model.AddBoolOr([x00, x01, x02.Not()])
    model.AddBoolOr([x00.Not(), x02.Not()])
    
    class VarArraySolutionCollector(cp_model.CpSolverSolutionCallback):
    
        def __init__(self, variables):
            cp_model.CpSolverSolutionCallback.__init__(self)
            self.__variables = variables
            self.solution_list = []
    
        def on_solution_callback(self):
            self.solution_list.append([self.Value(v) for v in self.__variables])
    
    # Create a solver and solve.
    solver = cp_model.CpSolver()
    solution_collector = VarArraySolutionCollector([x00, x01, x02])
    solver.SearchForAllSolutions(model, solution_collector)
    
    solution_collector.solution_list
    
    Out[33]: [[0, 1, 0], [0, 0, 0], [0, 1, 1], [1, 1, 0], [1, 0, 0]]