如何通过添加单位子句来逐步解决一系列CP-SAT问题来实现加速？

编程问答 2022-06-12

问题描述

我正在解决一系列SAT问题，可以通过在前一个SAT问题的模型中添加一些单位条款来逐步构建下一个SAT问题。我们不仅可以通过重用以前的SAT问题中的约束和变量来加速CP-SAT，还可以通过解决先前的SAT问题来重用中间结果吗？

以下代码是否起作用：

    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)

解决方法

这称为解决方案提示。

请参见this example

or-toolsperformanceperformanceperformancesolver