Google or-tools库中约束的布尔运算

问题描述 投票：0回答：4

我是约束编程的初学者，我在我的 c# 程序中使用 Google 或工具库。

我想在我的求解器中添加以下约束：

((t1 >= 12 && t1 <= 15) || (t2 >= 16 && t2 <= 18)) && ( t1 + t2 ) < 30

所以我用 C# 编写了以下代码：

var solver = new Solver("My_CP_Colver");
var t1 = solver.MakeIntVar(12, 20,"t1");
var t2 = solver.MakeIntVar(12, 20,"t2");

solver.Add(???)//<-((t1 >= 12 && t1 <= 15)||(t2 >= 16 && t2 <= 18)) && ( t1 + t2 ) < 30

对上述约束有什么帮助吗？

c# or-tools constraint-programming boolean-operations cp-sat-solver
4个回答
6
投票

我的语言是 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
3
投票

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

目前在谷歌或工具中制定逻辑约束的方式是将它们转换为线性约束。最好先检查 this 以了解转换的概念，然后看看 Who killed Agatha 来自 HakanK 的例子。这里实现的一部分与逻辑约束有关：

//   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);
    }
  }
}

您也可以查看这篇文章.

3
投票

您可以使用

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
值）

-2
投票

首先，必须为域定义变量（例如正整数）。 然后，在 

Solver
被要求解决之前定义约束和目标函数。

您可以轻松地将以下

C#
代码示例翻译成您的问题：

    string solverType = "GLPK_MIXED_INTEGER_PROGRAMMING";
    Solver solver = Solver.CreateSolver("IntegerProgramming", solverType);
    if (solver == null)
    {
      Console.WriteLine("Could not create solver " + solverType);
      return;
    }
    // x1 and x2 are integer non-negative variables.
    Variable x1 = solver.MakeIntVar(0.0, double.PositiveInfinity, "x1");
    Variable x2 = solver.MakeIntVar(0.0, double.PositiveInfinity, "x2");

    // Minimize x1 + 2 * x2.
    Objective objective = solver.Objective();
    objective.SetMinimization();
    objective.SetCoefficient(x1, 1);
    objective.SetCoefficient(x2, 2);

    // 2 * x2 + 3 * x1 >= 17.
    Constraint ct = solver.MakeConstraint(17, double.PositiveInfinity);
    ct.SetCoefficient(x1, 3);
    ct.SetCoefficient(x2, 2);

    int resultStatus = solver.Solve();

    // Check that the problem has an optimal solution.
    if (resultStatus != Solver.OPTIMAL)
    {
      Console.WriteLine("The problem does not have an optimal solution!");
      return;
    }

    Console.WriteLine("Problem solved in " + solver.WallTime() +
                      " milliseconds");

    // The objective value of the solution.
    Console.WriteLine("Optimal objective value = " + objective.Value());

    // The value of each variable in the solution.
    Console.WriteLine("x1 = " + x1.SolutionValue());
    Console.WriteLine("x2 = " + x2.SolutionValue());

    Console.WriteLine("Advanced usage:");
    Console.WriteLine("Problem solved in " + solver.Nodes() +
                      " branch-and-bound nodes");

从这里复制.

另一个简单的exampleHåkan Kjellerstrand：

Solver solver = new Solver("Volsay", Solver.CLP_LINEAR_PROGRAMMING);

//
// Variables
//

Variable Gas = solver.MakeNumVar(0, 100000, "Gas");
Variable Chloride = solver.MakeNumVar(0, 100000, "Cloride");

Constraint c1 = solver.Add(Gas + Chloride <= 50);
Constraint c2 = solver.Add(3 * Gas + 4 * Chloride <= 180);

solver.Maximize(40 * Gas + 50 * Chloride);

int resultStatus = solver.Solve();

if (resultStatus != Solver.OPTIMAL) {
  Console.WriteLine("The problem don't have an optimal solution.");
  return;
}

Console.WriteLine("Objective: {0}", solver.ObjectiveValue());

Console.WriteLine("Gas      : {0} ReducedCost: {1}",
                  Gas.SolutionValue(),
                  Gas.ReducedCost());

Console.WriteLine("Chloride : {0} ReducedCost: {1}",
                  Chloride.SolutionValue(),
                  Chloride.ReducedCost());

我不知道如何在 Google OR 工具中定义析取约束。

使用 

Microsoft Z3 Solver
的 C# API，可以按如下方式完成：

    Context ctx = new Context();

    IntExpr t1 = ctx.MkIntConst("t1");
    IntExpr t2 = ctx.MkIntConst("t2");
    IntNum c12 = ctx.MkInt(12);
    IntNum c15 = ctx.MkInt(15);
    IntNum c16 = ctx.MkInt(16);
    IntNum c18 = ctx.MkInt(18);
    IntNum c30 = ctx.MkInt(30);

    Solver solver = ctx.MkSolver();

    BoolExpr constraintInterval12_15 = 
        ctx.MkAnd(ctx.MkLe(c12, t1), ctx.MkLe(t1, c15));
    BoolExpr constraintInterval16_18 = 
        ctx.MkAnd(ctx.MkLe(c16, t2), ctx.MkLe(t2, c18));
    BoolExpr constraintLe20 = 
        ctx.MkLt(ctx.MkAdd(t1, t2), c30);

    solver.Assert(constraintLe20);
    solver.Assert(ctx.MkOr(constraintInterval12_15, constraintInterval16_18));

    if (solver.Check() == Status.SATISFIABLE)
    {
        Model m = solver.Model;

        Console.WriteLine("t1 = " + m.Evaluate(t1));
        Console.WriteLine("t2 = " + m.Evaluate(t2));
    }
最新问题
© www.soinside.com 2019 - 2024. All rights reserved.