对 Google 或工具库中约束的布尔运算

我的语言是python，我认为它应该很容易将pytho代码翻译成C#。

model = cp_model.CpModel()
t1 = model.NewIntVar(12, 20, "t1")
t1_bool_ge = model.NewBoolVar("t1_bool_ge")
t1_bool_le = model.NewBoolVar("t1_bool_le")
t1_bool_and =  model.NewBoolVar("t1_bool_and")
tmp_t1 = []
tmp_t1.append(t1_bool_ge)
tmp_t1.append(t1_bool_le)
model.Add(t1 >= 12).OnlyEnforceIf(t1_bool_ge) # t1 >=12
model.Add(t1 <= 15).OnlyEnforceIf(t1_bool_le) # t1 <= 15
model.Add(t1_bool_and==1).OnlyEnforceIf(tmp_t1) # (t1 >=12)&&(t1 <= 15)
t2 = model.NewIntVar(12, 20, "t2")
t2_bool_ge = model.NewBoolVar("t2_bool_ge")
t2_bool_le = model.NewBoolVar("t2_bool_le")
t2_bool_and =  model.NewBoolVar("t2_bool_and")
tmp_t2 = []
tmp_t2.append(t2_bool_ge)
tmp_t2.append(t2_bool_le)
model.Add(t2 >= 16).OnlyEnforceIf(t2_bool_ge) # t2 >=16
model.Add(t2 <= 18).OnlyEnforceIf(t2_bool_le) # t2 <= 18
model.Add(t2_bool_and==1).OnlyEnforceIf(tmp_t2) #(t2 >=16) && (t2 <=18)
tmp_t1_t2 = []
tmp_t1_t2.append(t2_bool_and)
tmp_t1_t2.append(t1_bool_and)
model.Add(sum(tmp_t1_t2)==1) #((t1 >=12)&&(t1 <= 15))||((t2 >=16) && (t2 <=18))
model.Add(t1 + t2 < 30) # ( t1 + t2 ) < 30

不幸的是，Google or-tools 库没有提供丰富的逻辑约束。如果你可以用Java开发你的实现，我建议你使用Choco Solver，它包含一个具有大量SAT约束的SAT求解器。

目前在Google或工具中制定逻辑约束的方法是将它们转换为线性约束。最好先检查一下以了解转换的概念，然后，看看哈坎克的谁杀死了阿加莎的例子。这里这个实现的一部分与逻辑约束有关：

//   if (i != j) =>
//       ((richer[i,j] = 1) <=> (richer[j,i] = 0))
for(int i = 0; i < n; i++) {
  for(int j = 0; j < n; j++) {
    if (i != j) {
      solver.Add((richer[i, j]==1) - (richer[j, i]==0) == 0);
    }
  }
}

你也可以查看这篇文章。

您可以使用 MakeMin 和 MakeMax 分别对连词和析取进行编码。对每个部分执行此操作，您最终会得到如下所示的内容：

var solver = new Solver("MY_CP_Solver");
var t1 = solver.MakeIntVar(12, 20, "t1");
var t1ge = solver.MakeGreaterOrEqual(t1, 12);
var t1le = solver.MakeLessOrEqual(t1, 15);
var t1both = solver.MakeMin(t1ge, t1le);
var t2 = solver.MakeIntVar(12, 20, "t2");
var t2ge = solver.MakeGreaterOrEqual(t2, 16);
var t2le = solver.MakeLessOrEqual(t2, 18);
var t2both = solver.MakeMin(t2ge, t2le);
var or = solver.MakeMax(t1both, t2both);
solver.Add(or == 1);
solver.Add(t1 + t2 < 30);
var db = solver.MakePhase(new[] {t1, t2}, Solver.CHOOSE_FIRST_UNBOUND, Solver.ASSIGN_MIN_VALUE);
solver.Solve(db);
while (solver.NextSolution())
    Console.WriteLine($"t1: {t1.Value()}, t2: {t2.Value()}");

输出：

t1: 12, t2: 12
t1: 12, t2: 13
t1: 12, t2: 14
t1: 12, t2: 15
t1: 12, t2: 16
t1: 12, t2: 17
t1: 13, t2: 12
t1: 13, t2: 13
t1: 13, t2: 14
t1: 13, t2: 15
t1: 13, t2: 16
t1: 14, t2: 12
t1: 14, t2: 13
t1: 14, t2: 14
t1: 14, t2: 15
t1: 15, t2: 12
t1: 15, t2: 13
t1: 15, t2: 14

特别是，析取中的第一个约束始终处于活动状态。

使用较新的Google.OrTools.Sat.CpSolver，您可以执行以下操作，其中我们引入了一个辅助布尔b，它具有确保满足析取中至少一个子句的特性：

var model = new CpModel();
var t1 = model.NewIntVar(12, 20, "t1");
var t2 = model.NewIntVar(12, 20, "t2");
var b = model.NewBoolVar("First constraint active");
model.Add(t1 >= 12).OnlyEnforceIf(b);
model.Add(t1 <= 15).OnlyEnforceIf(b);
model.Add(t2 >= 16).OnlyEnforceIf(b.Not());
model.Add(t2 <= 18).OnlyEnforceIf(b.Not());
model.Add(t1 + t2 < 30);
var solver = new CpSolver();
var cb = new SolutionPrinter(new [] { t1, t2 });
solver.SearchAllSolutions(model, cb);

在这里，打印机定义如下：

public class SolutionPrinter : CpSolverSolutionCallback
{
    public VarArraySolutionPrinter(IntVar[] v) => this.v = v;
    public override void OnSolutionCallback() => Console.WriteLine($"t1: {Value(v[0])}, t2: {Value(v[1])}");
    private readonly IntVar[] v;
}

请注意，这将多次找到相同的(t1, t2)对（但具有不同的b值）