Булевы операции над ограничениями в библиотеке Google or-tools
Я новичок в программировании с ограничениями, и я использую библиотеку Google or-tools в своей программе на C#.
Я хочу добавить следующее ограничение в мой решатель:
((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
Любая помощь, чтобы сделать выше ограничение, пожалуйста?
2 ответа
Мой язык - python, я думаю, он должен легко перевести следующий код Python на 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
Вы можете использовать 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)
К сожалению, библиотека Google or-tools не предоставляет богатых логических ограничений. Если вы можете разработать свою реализацию на Java, я рекомендую вам использовать Choco Solver, который включает в себя SAT-решатель с большим количеством ограничений SAT.
Текущий способ формулирования логических ограничений в Google or-tools - это преобразование их в линейные ограничения. Было бы лучше сначала проверить это, чтобы понять концепцию трансформации, а затем взглянуть на пример " Кто убил Агату" из 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);
}
}
}
Вы также можете проверить этот пост.
Во-первых, переменные должны быть определены для домена (например, натуральные числа). Затем ограничения и целевая функция определяются до 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");
Скопировано отсюда.
Еще один простой пример Хокана Кьеллерстранда:
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 Tools.
С использованием C# API Microsoft Z3 Solver, это можно сделать следующим образом:
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));
}