Search code examples
performancesolveror-toolscp-sat

How to achieve a speed up by adding unit clauses to solve a sequence of CP-SAT problems incrementally?

I am solving a sequence of SAT problems, where the next SAT problem can be always built incrementally by adding some unit clauses to the model of the previous SAT problem. Can we speed up CP-SAT by not only reusing the constraints and variables in the previous SAT problem, but also reusing the intermediate results by solving previous SAT problem?

Does the following code work:

    solver = cp_model.CpSolver()

    x = model.NewBoolVar('x')
    y = model.NewBoolVar('y')

    model.AddBoolOr([x, y.Not()])

    # retrieve the results for the first problem
    status = solver.Solve(model)

    ....
    # add a new unit clause
    model.AddBoolOr([x.Not()])
    # retrieve the results for the second problem
    status = solver.Solve(model)
Solution

  • This is called solution hinting.

    See this example