348 lines
12 KiB
C#
348 lines
12 KiB
C#
using System;
|
|
using System.Collections.Generic;
|
|
using Xunit;
|
|
using Google.OrTools.Sat;
|
|
|
|
namespace Google.OrTools.Tests {
|
|
public class SatSolverTest {
|
|
static IntegerVariableProto NewIntegerVariable(long lb, long ub) {
|
|
IntegerVariableProto var = new IntegerVariableProto();
|
|
var.Domain.Add(lb);
|
|
var.Domain.Add(ub);
|
|
return var;
|
|
}
|
|
|
|
static ConstraintProto NewLinear2(int v1, int v2, long c1, long c2, long lb, long ub) {
|
|
LinearConstraintProto linear = new LinearConstraintProto();
|
|
linear.Vars.Add(v1);
|
|
linear.Vars.Add(v2);
|
|
linear.Coeffs.Add(c1);
|
|
linear.Coeffs.Add(c2);
|
|
linear.Domain.Add(lb);
|
|
linear.Domain.Add(ub);
|
|
ConstraintProto ct = new ConstraintProto();
|
|
ct.Linear = linear;
|
|
return ct;
|
|
}
|
|
|
|
static ConstraintProto NewLinear3(int v1, int v2, int v3, long c1, long c2, long c3, long lb,
|
|
long ub) {
|
|
LinearConstraintProto linear = new LinearConstraintProto();
|
|
linear.Vars.Add(v1);
|
|
linear.Vars.Add(v2);
|
|
linear.Vars.Add(v3);
|
|
linear.Coeffs.Add(c1);
|
|
linear.Coeffs.Add(c2);
|
|
linear.Coeffs.Add(c3);
|
|
linear.Domain.Add(lb);
|
|
linear.Domain.Add(ub);
|
|
ConstraintProto ct = new ConstraintProto();
|
|
ct.Linear = linear;
|
|
return ct;
|
|
}
|
|
|
|
static CpObjectiveProto NewMinimize1(int v1, long c1) {
|
|
CpObjectiveProto obj = new CpObjectiveProto();
|
|
obj.Vars.Add(v1);
|
|
obj.Coeffs.Add(c1);
|
|
return obj;
|
|
}
|
|
|
|
static CpObjectiveProto NewMaximize1(int v1, long c1) {
|
|
CpObjectiveProto obj = new CpObjectiveProto();
|
|
obj.Vars.Add(-v1 - 1);
|
|
obj.Coeffs.Add(c1);
|
|
obj.ScalingFactor = -1;
|
|
return obj;
|
|
}
|
|
|
|
static CpObjectiveProto NewMaximize2(int v1, int v2, long c1, long c2) {
|
|
CpObjectiveProto obj = new CpObjectiveProto();
|
|
obj.Vars.Add(-v1 - 1);
|
|
obj.Vars.Add(-v2 - 1);
|
|
obj.Coeffs.Add(c1);
|
|
obj.Coeffs.Add(c2);
|
|
obj.ScalingFactor = -1;
|
|
return obj;
|
|
}
|
|
|
|
// CpModelProto
|
|
[Fact]
|
|
public void SimpleLinearModelProto() {
|
|
CpModelProto model = new CpModelProto();
|
|
model.Variables.Add(NewIntegerVariable(-10, 10));
|
|
model.Variables.Add(NewIntegerVariable(-10, 10));
|
|
model.Variables.Add(NewIntegerVariable(-1000000, 1000000));
|
|
model.Constraints.Add(NewLinear2(0, 1, 1, 1, -1000000, 100000));
|
|
model.Constraints.Add(NewLinear3(0, 1, 2, 1, 2, -1, 0, 100000));
|
|
model.Objective = NewMaximize1(2, 1);
|
|
// Console.WriteLine("model = " + model.ToString());
|
|
|
|
CpSolverResponse response = SatHelper.Solve(model);
|
|
Assert.Equal(CpSolverStatus.Optimal, response.Status);
|
|
Assert.Equal(30, response.ObjectiveValue);
|
|
Assert.Equal(new long[] { 10, 10, 30 }, response.Solution);
|
|
// Console.WriteLine("response = " + response.ToString());
|
|
}
|
|
|
|
[Fact]
|
|
public void SimpleLinearModelProto2() {
|
|
CpModelProto model = new CpModelProto();
|
|
model.Variables.Add(NewIntegerVariable(-10, 10));
|
|
model.Variables.Add(NewIntegerVariable(-10, 10));
|
|
model.Constraints.Add(NewLinear2(0, 1, 1, 1, -1000000, 100000));
|
|
model.Objective = NewMaximize2(0, 1, 1, -2);
|
|
// Console.WriteLine("model = " + model.ToString());
|
|
|
|
CpSolverResponse response = SatHelper.Solve(model);
|
|
Assert.Equal(CpSolverStatus.Optimal, response.Status);
|
|
Assert.Equal(30, response.ObjectiveValue);
|
|
Assert.Equal(new long[] { 10, -10 }, response.Solution);
|
|
// Console.WriteLine("response = " + response.ToString());
|
|
}
|
|
|
|
// CpModel
|
|
[Fact]
|
|
public void SimpleLinearModel() {
|
|
CpModel model = new CpModel();
|
|
IntVar v1 = model.NewIntVar(-10, 10, "v1");
|
|
IntVar v2 = model.NewIntVar(-10, 10, "v2");
|
|
IntVar v3 = model.NewIntVar(-100000, 100000, "v3");
|
|
model.AddLinearConstraint(v1 + v2, -1000000, 100000);
|
|
model.AddLinearConstraint(v1 + 2 * v2 - v3, 0, 100000);
|
|
model.Maximize(v3);
|
|
Assert.Equal(v1.Domain.FlattenedIntervals(), new long[] { -10, 10 });
|
|
// Console.WriteLine("model = " + model.Model.ToString());
|
|
|
|
CpSolver solver = new CpSolver();
|
|
CpSolverStatus status = solver.Solve(model);
|
|
Assert.Equal(CpSolverStatus.Optimal, status);
|
|
|
|
CpSolverResponse response = solver.Response;
|
|
Assert.Equal(30, response.ObjectiveValue);
|
|
Assert.Equal(new long[] { 10, 10, 30 }, response.Solution);
|
|
// Console.WriteLine("response = " + reponse.ToString());
|
|
}
|
|
|
|
[Fact]
|
|
public void SimpleLinearModel2() {
|
|
CpModel model = new CpModel();
|
|
IntVar v1 = model.NewIntVar(-10, 10, "v1");
|
|
IntVar v2 = model.NewIntVar(-10, 10, "v2");
|
|
model.AddLinearConstraint(v1 + v2, -1000000, 100000);
|
|
model.Maximize(v1 - 2 * v2);
|
|
// Console.WriteLine("model = " + model.Model.ToString());
|
|
|
|
CpSolver solver = new CpSolver();
|
|
CpSolverStatus status = solver.Solve(model);
|
|
Assert.Equal(CpSolverStatus.Optimal, status);
|
|
|
|
CpSolverResponse response = solver.Response;
|
|
Assert.Equal(30, response.ObjectiveValue);
|
|
Assert.Equal(new long[] { 10, -10 }, response.Solution);
|
|
// Console.WriteLine("response = " + reponse.ToString());
|
|
}
|
|
|
|
[Fact]
|
|
public void SimpleLinearModel3() {
|
|
CpModel model = new CpModel();
|
|
IntVar v1 = model.NewIntVar(-10, 10, "v1");
|
|
IntVar v2 = model.NewIntVar(-10, 10, "v2");
|
|
model.Add(-100000 <= v1 + 2 * v2 <= 100000);
|
|
model.Minimize(v1 - 2 * v2);
|
|
// Console.WriteLine("model = " + model.Model.ToString());
|
|
|
|
CpSolver solver = new CpSolver();
|
|
CpSolverStatus status = solver.Solve(model);
|
|
Assert.Equal(CpSolverStatus.Optimal, status);
|
|
|
|
CpSolverResponse response = solver.Response;
|
|
Assert.Equal(-10, solver.Value(v1));
|
|
Assert.Equal(10, solver.Value(v2));
|
|
Assert.Equal(new long[] { -10, 10 }, response.Solution);
|
|
Assert.Equal(-30, solver.Value(v1 - 2 * v2));
|
|
Assert.Equal(-30, response.ObjectiveValue);
|
|
// Console.WriteLine("response = " + reponse.ToString());
|
|
}
|
|
|
|
[Fact]
|
|
public void NegativeIntVar() {
|
|
CpModel model = new CpModel();
|
|
IntVar boolvar = model.NewBoolVar("boolvar");
|
|
IntVar x = model.NewIntVar(0, 10, "x");
|
|
IntVar delta = model.NewIntVar(-5, 5, "delta");
|
|
IntVar squaredDelta = model.NewIntVar(0, 25, "squaredDelta");
|
|
model.Add(x == boolvar * 4);
|
|
model.Add(delta == x - 5);
|
|
model.AddProdEquality(squaredDelta, new IntVar[] { delta, delta });
|
|
model.Minimize(squaredDelta);
|
|
// Console.WriteLine("model = " + model.Model.ToString());
|
|
|
|
CpSolver solver = new CpSolver();
|
|
CpSolverStatus status = solver.Solve(model);
|
|
CpSolverResponse response = solver.Response;
|
|
Console.WriteLine("response = " + response.ToString());
|
|
|
|
Assert.Equal(CpSolverStatus.Optimal, status);
|
|
|
|
Assert.Equal(1, solver.Value(boolvar));
|
|
Assert.Equal(4, solver.Value(x));
|
|
Assert.Equal(-1, solver.Value(delta));
|
|
Assert.Equal(1, solver.Value(squaredDelta));
|
|
Assert.Equal(new long[] { 1, 4, -1, 1 }, response.Solution);
|
|
Assert.Equal(1.0, response.ObjectiveValue, 5);
|
|
}
|
|
|
|
[Fact]
|
|
public void NegativeSquareVar() {
|
|
CpModel model = new CpModel();
|
|
IntVar boolvar = model.NewBoolVar("boolvar");
|
|
IntVar x = model.NewIntVar(0, 10, "x");
|
|
IntVar delta = model.NewIntVar(-5, 5, "delta");
|
|
IntVar squaredDelta = model.NewIntVar(0, 25, "squaredDelta");
|
|
model.Add(x == 4).OnlyEnforceIf(boolvar);
|
|
model.Add(x == 0).OnlyEnforceIf(boolvar.Not());
|
|
model.Add(delta == x - 5);
|
|
long[,] tuples = { { -5, 25 }, { -4, 16 }, { -3, 9 }, { -2, 4 }, { -1, 1 }, { 0, 0 },
|
|
{ 1, 1 }, { 2, 4 }, { 3, 9 }, { 4, 16 }, { 5, 25 } };
|
|
model.AddAllowedAssignments(new IntVar[] { delta, squaredDelta }, tuples);
|
|
model.Minimize(squaredDelta);
|
|
|
|
CpSolver solver = new CpSolver();
|
|
CpSolverStatus status = solver.Solve(model);
|
|
|
|
CpSolverResponse response = solver.Response;
|
|
Assert.Equal(1, solver.Value(boolvar));
|
|
Assert.Equal(4, solver.Value(x));
|
|
Assert.Equal(-1, solver.Value(delta));
|
|
Assert.Equal(1, solver.Value(squaredDelta));
|
|
Assert.Equal(new long[] { 1, 4, -1, 1 }, response.Solution);
|
|
Assert.Equal(1.0, response.ObjectiveValue, 6);
|
|
}
|
|
|
|
[Fact]
|
|
public void Division() {
|
|
CpModel model = new CpModel();
|
|
IntVar v1 = model.NewIntVar(0, 10, "v1");
|
|
IntVar v2 = model.NewIntVar(1, 10, "v2");
|
|
model.AddDivisionEquality(3, v1, v2);
|
|
// Console.WriteLine(model.Model);
|
|
|
|
CpSolver solver = new CpSolver();
|
|
CpSolverStatus status = solver.Solve(model);
|
|
Assert.Equal(CpSolverStatus.Optimal, status);
|
|
|
|
CpSolverResponse response = solver.Response;
|
|
Assert.Equal(3, solver.Value(v1));
|
|
Assert.Equal(1, solver.Value(v2));
|
|
Assert.Equal(new long[] { 3, 1, 3 }, response.Solution);
|
|
Assert.Equal(0, response.ObjectiveValue);
|
|
// Console.WriteLine("response = " + reponse.ToString());
|
|
}
|
|
|
|
[Fact]
|
|
public void Modulo() {
|
|
CpModel model = new CpModel();
|
|
IntVar v1 = model.NewIntVar(1, 10, "v1");
|
|
IntVar v2 = model.NewIntVar(1, 10, "v2");
|
|
model.AddModuloEquality(3, v1, v2);
|
|
// Console.WriteLine(model.Model);
|
|
|
|
CpSolver solver = new CpSolver();
|
|
CpSolverStatus status = solver.Solve(model);
|
|
Assert.Equal(CpSolverStatus.Optimal, status);
|
|
|
|
CpSolverResponse response = solver.Response;
|
|
Assert.Equal(3, solver.Value(v1));
|
|
Assert.Equal(4, solver.Value(v2));
|
|
Assert.Equal(new long[] { 3, 4, 3 }, response.Solution);
|
|
Assert.Equal(0, response.ObjectiveValue);
|
|
// Console.WriteLine("response = " + reponse.ToString());
|
|
}
|
|
|
|
[Fact]
|
|
public void LargeScalProdLong() {
|
|
CpModel model = new CpModel();
|
|
List<IntVar> vars = new List<IntVar>();
|
|
List<long> coeffs = new List<long>();
|
|
|
|
for (int i = 0; i < 100000; ++i) {
|
|
vars.Add(model.NewBoolVar(""));
|
|
coeffs.Add(i + 1);
|
|
}
|
|
|
|
var watch = System.Diagnostics.Stopwatch.StartNew();
|
|
model.Minimize(LinearExpr.ScalProd(vars, coeffs));
|
|
watch.Stop();
|
|
var elapsedMs = watch.ElapsedMilliseconds;
|
|
Console.WriteLine($"Long: Elapsed time {elapsedMs}");
|
|
}
|
|
|
|
[Fact]
|
|
public void LargeScalProdInt() {
|
|
CpModel model = new CpModel();
|
|
List<IntVar> vars = new List<IntVar>();
|
|
List<int> coeffs = new List<int>();
|
|
|
|
for (int i = 0; i < 100000; ++i) {
|
|
vars.Add(model.NewBoolVar(""));
|
|
coeffs.Add(i);
|
|
}
|
|
|
|
var watch = System.Diagnostics.Stopwatch.StartNew();
|
|
model.Minimize(LinearExpr.ScalProd(vars, coeffs));
|
|
watch.Stop();
|
|
var elapsedMs = watch.ElapsedMilliseconds;
|
|
Console.WriteLine($"Int: Elapsed time {elapsedMs}");
|
|
}
|
|
|
|
[Fact]
|
|
public void LargeScalProdExpr() {
|
|
CpModel model = new CpModel();
|
|
List<LinearExpr> exprs = new List<LinearExpr>();
|
|
|
|
for (int i = 0; i < 100000; ++i) {
|
|
exprs.Add(model.NewBoolVar("") * i);
|
|
}
|
|
|
|
var watch = System.Diagnostics.Stopwatch.StartNew();
|
|
model.Minimize(LinearExpr.Sum(exprs));
|
|
watch.Stop();
|
|
var elapsedMs = watch.ElapsedMilliseconds;
|
|
Console.WriteLine($"Exprs: Elapsed time {elapsedMs}");
|
|
}
|
|
|
|
[Fact]
|
|
public void LargeScalProdProto() {
|
|
CpModel model = new CpModel();
|
|
List<IntVar> vars = new List<IntVar>();
|
|
List<long> coeffs = new List<long>();
|
|
|
|
for (int i = 0; i < 100000; ++i) {
|
|
vars.Add(model.NewBoolVar(""));
|
|
coeffs.Add(i + 1);
|
|
}
|
|
|
|
var watch = System.Diagnostics.Stopwatch.StartNew();
|
|
model.Minimize();
|
|
for (int i = 0; i < 100000; ++i) {
|
|
model.AddTermToObjective(vars[i], coeffs[i]);
|
|
}
|
|
watch.Stop();
|
|
var elapsedMs = watch.ElapsedMilliseconds;
|
|
Console.WriteLine($"Proto: Elapsed time {elapsedMs}");
|
|
}
|
|
|
|
[Fact]
|
|
public void ExportModel() {
|
|
CpModel model = new CpModel();
|
|
IntVar v1 = model.NewIntVar(-10, 10, "v1");
|
|
IntVar v2 = model.NewIntVar(-10, 10, "v2");
|
|
model.Add(-100000 <= v1 + 2 * v2 <= 100000);
|
|
model.Minimize(v1 - 2 * v2);
|
|
Assert.True(model.ExportToFile("test_model_dotnet.pbtxt"));
|
|
Console.WriteLine("Model written to file");
|
|
}
|
|
}
|
|
} // namespace Google.OrTools.Tests
|