Google OR-Tools v9.12
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
SatSolverTests.cs
Go to the documentation of this file.
1// Copyright 2010-2025 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14using System;
15using System.Collections.Generic;
16using System.Text;
17using Xunit;
18using Google.OrTools.Sat;
19using Xunit.Abstractions;
20
21public class SolutionCounter : CpSolverSolutionCallback
22{
23 public SolutionCounter()
24 {
25 // Console.WriteLine("SolutionCounter Ctor");
26 solution_count_ = 0;
27 }
28
29 public override void OnSolutionCallback()
30 {
31 solution_count_ += 1;
32 }
33
34 public int SolutionCount
35 {
36 get {
37 return solution_count_;
38 }
39 set {
40 solution_count_ = value;
41 }
42 }
43 private int solution_count_;
44}
45
46public class SolutionDivisionCounter : SolutionCounter
47{
48 public SolutionDivisionCounter(int result, IntVar a, IntVar b, ITestOutputHelper output)
49 {
50 result_ = result;
51 a_ = a;
52 b_ = b;
53 output_ = output;
54 }
55
56 public override void OnSolutionCallback()
57 {
58 base.OnSolutionCallback();
59
60 var solutionVariablesReport = new StringBuilder();
61 foreach (IntVar v in new IntVar[] { a_, b_ })
62 {
63 solutionVariablesReport.Append($"{v}={Value(v)} ");
64 }
65 solutionVariablesReport.AppendLine();
66 output_.WriteLine(solutionVariablesReport.ToString());
67 Assert.Equal(result_, Value(a_) / Value(b_));
68 }
69
70 private readonly int result_;
71 private readonly IntVar a_;
72 private readonly IntVar b_;
73 private readonly ITestOutputHelper output_;
74}
75
76public class SolutionModuloCounter : SolutionCounter
77{
78 public SolutionModuloCounter(int result, IntVar a, IntVar b, ITestOutputHelper output)
79 {
80 result_ = result;
81 a_ = a;
82 b_ = b;
83 output_ = output;
84 }
85
86 public override void OnSolutionCallback()
87 {
88 base.OnSolutionCallback();
89
90 var solutionVariablesReport = new StringBuilder();
91 foreach (IntVar v in new IntVar[] { a_, b_ })
92 {
93 solutionVariablesReport.Append($"{v}={Value(v)} ");
94 }
95 solutionVariablesReport.AppendLine();
96 output_.WriteLine(solutionVariablesReport.ToString());
97 Assert.Equal(result_, Value(a_) % Value(b_));
98 }
99
100 private readonly int result_;
101 private readonly IntVar a_;
102 private readonly IntVar b_;
103 private readonly ITestOutputHelper output_;
104}
105
106namespace Google.OrTools.Tests
107{
108public class SatSolverTest
109{
110 private readonly ITestOutputHelper output_;
111
112 public SatSolverTest(ITestOutputHelper output)
113 {
114 this.output_ = output;
115 }
116
117 static IntegerVariableProto NewIntegerVariable(long lb, long ub)
118 {
119 IntegerVariableProto var = new IntegerVariableProto();
120 var.Domain.Add(lb);
121 var.Domain.Add(ub);
122 return var;
123 }
124
125 static ConstraintProto NewLinear2(int v1, int v2, long c1, long c2, long lb, long ub)
126 {
127 LinearConstraintProto linear = new LinearConstraintProto();
128 linear.Vars.Add(v1);
129 linear.Vars.Add(v2);
130 linear.Coeffs.Add(c1);
131 linear.Coeffs.Add(c2);
132 linear.Domain.Add(lb);
133 linear.Domain.Add(ub);
134 ConstraintProto ct = new ConstraintProto();
135 ct.Linear = linear;
136 return ct;
137 }
138
139 static ConstraintProto NewLinear3(int v1, int v2, int v3, long c1, long c2, long c3, long lb, long ub)
140 {
141 LinearConstraintProto linear = new LinearConstraintProto();
142 linear.Vars.Add(v1);
143 linear.Vars.Add(v2);
144 linear.Vars.Add(v3);
145 linear.Coeffs.Add(c1);
146 linear.Coeffs.Add(c2);
147 linear.Coeffs.Add(c3);
148 linear.Domain.Add(lb);
149 linear.Domain.Add(ub);
150 ConstraintProto ct = new ConstraintProto();
151 ct.Linear = linear;
152 return ct;
153 }
154
155 static CpObjectiveProto NewMinimize1(int v1, long c1)
156 {
157 CpObjectiveProto obj = new CpObjectiveProto();
158 obj.Vars.Add(v1);
159 obj.Coeffs.Add(c1);
160 return obj;
161 }
162
163 static CpObjectiveProto NewMaximize1(int v1, long c1)
164 {
165 CpObjectiveProto obj = new CpObjectiveProto();
166 obj.Vars.Add(-v1 - 1);
167 obj.Coeffs.Add(c1);
168 obj.ScalingFactor = -1;
169 return obj;
170 }
171
172 static CpObjectiveProto NewMaximize2(int v1, int v2, long c1, long c2)
173 {
174 CpObjectiveProto obj = new CpObjectiveProto();
175 obj.Vars.Add(-v1 - 1);
176 obj.Vars.Add(-v2 - 1);
177 obj.Coeffs.Add(c1);
178 obj.Coeffs.Add(c2);
179 obj.ScalingFactor = -1;
180 return obj;
181 }
182
183 // CpModelProto
184 [Fact]
185 public void SimpleLinearModelProto()
186 {
187 CpModelProto model = new CpModelProto();
188 model.Variables.Add(NewIntegerVariable(-10, 10));
189 model.Variables.Add(NewIntegerVariable(-10, 10));
190 model.Variables.Add(NewIntegerVariable(-1000000, 1000000));
191 model.Constraints.Add(NewLinear2(0, 1, 1, 1, -1000000, 100000));
192 model.Constraints.Add(NewLinear3(0, 1, 2, 1, 2, -1, 0, 100000));
193 model.Objective = NewMaximize1(2, 1);
194 // Console.WriteLine("model = " + model.ToString());
195 SolveWrapper solve_wrapper = new SolveWrapper();
196 CpSolverResponse response = solve_wrapper.Solve(model);
197 Assert.Equal(CpSolverStatus.Optimal, response.Status);
198 Assert.Equal(30, response.ObjectiveValue);
199 Assert.Equal(new long[] { 10, 10, 30 }, response.Solution);
200 // Console.WriteLine("response = " + response.ToString());
201 }
202
203 [Fact]
204 public void SimpleLinearModelProto2()
205 {
206 CpModelProto model = new CpModelProto();
207 model.Variables.Add(NewIntegerVariable(-10, 10));
208 model.Variables.Add(NewIntegerVariable(-10, 10));
209 model.Constraints.Add(NewLinear2(0, 1, 1, 1, -1000000, 100000));
210 model.Objective = NewMaximize2(0, 1, 1, -2);
211 // Console.WriteLine("model = " + model.ToString());
212
213 SolveWrapper solve_wrapper = new SolveWrapper();
214 CpSolverResponse response = solve_wrapper.Solve(model);
215 Assert.Equal(CpSolverStatus.Optimal, response.Status);
216 Assert.Equal(30, response.ObjectiveValue);
217 Assert.Equal(new long[] { 10, -10 }, response.Solution);
218 // Console.WriteLine("response = " + response.ToString());
219 }
220
221 // CpModel
222 [Fact]
223 public void SimpleLinearModel()
224 {
225 CpModel model = new CpModel();
226 IntVar v1 = model.NewIntVar(-10, 10, "v1");
227 IntVar v2 = model.NewIntVar(-10, 10, "v2");
228 IntVar v3 = model.NewIntVar(-100000, 100000, "v3");
229 model.AddLinearConstraint(v1 + v2, -1000000, 100000);
230 model.AddLinearConstraint(v1 + 2 * v2 - v3, 0, 100000);
231 model.Maximize(v3);
232 Assert.Equal(v1.Domain.FlattenedIntervals(), new long[] { -10, 10 });
233 // Console.WriteLine("model = " + model.Model.ToString());
234
235 CpSolver solver = new CpSolver();
236 CpSolverStatus status = solver.Solve(model);
237 Assert.Equal(CpSolverStatus.Optimal, status);
238
239 CpSolverResponse response = solver.Response;
240 Assert.Equal(30, response.ObjectiveValue);
241 Assert.Equal(new long[] { 10, 10, 30 }, response.Solution);
242 // Console.WriteLine("response = " + response.ToString());
243 }
244
245 [Fact]
246 public void SimpleLinearModel2()
247 {
248 CpModel model = new CpModel();
249 IntVar v1 = model.NewIntVar(-10, 10, "v1");
250 IntVar v2 = model.NewIntVar(-10, 10, "v2");
251 model.AddLinearConstraint(v1 + v2, -1000000, 100000);
252 model.Maximize(v1 - 2 * v2);
253 // Console.WriteLine("model = " + model.Model.ToString());
254
255 CpSolver solver = new CpSolver();
256 CpSolverStatus status = solver.Solve(model);
257 Assert.Equal(CpSolverStatus.Optimal, status);
258
259 CpSolverResponse response = solver.Response;
260 Assert.Equal(30, response.ObjectiveValue);
261 Assert.Equal(new long[] { 10, -10 }, response.Solution);
262 // Console.WriteLine("response = " + response.ToString());
263 }
264
265 [Fact]
266 public void SimpleLinearModel3()
267 {
268 CpModel model = new CpModel();
269 IntVar v1 = model.NewIntVar(-10, 10, "v1");
270 IntVar v2 = model.NewIntVar(-10, 10, "v2");
271 model.Add(-100000 <= v1 + 2 * v2 <= 100000);
272 model.Minimize(v1 - 2 * v2);
273 // Console.WriteLine("model = " + model.Model.ToString());
274
275 CpSolver solver = new CpSolver();
276 CpSolverStatus status = solver.Solve(model);
277 Assert.Equal(CpSolverStatus.Optimal, status);
278
279 CpSolverResponse response = solver.Response;
280 Assert.Equal(-10, solver.Value(v1));
281 Assert.Equal(10, solver.Value(v2));
282 Assert.Equal(new long[] { -10, 10 }, response.Solution);
283 Assert.Equal(-30, solver.Value(v1 - 2 * v2));
284 Assert.Equal(-30, response.ObjectiveValue);
285 // Console.WriteLine("response = " + response.ToString());
286 }
287
288 [Fact]
289 public void NegativeIntVar()
290 {
291 CpModel model = new CpModel();
292 IntVar boolvar = model.NewBoolVar("boolvar");
293 IntVar x = model.NewIntVar(0, 10, "x");
294 IntVar delta = model.NewIntVar(-5, 5, "delta");
295 IntVar squaredDelta = model.NewIntVar(0, 25, "squaredDelta");
296 model.Add(x == boolvar * 4);
297 model.Add(delta == x - 5);
298 model.AddMultiplicationEquality(squaredDelta, new IntVar[] { delta, delta });
299 model.Minimize(squaredDelta);
300 // output_.WriteLine("model = " + model.Model);
301
302 CpSolver solver = new CpSolver();
303 CpSolverStatus status = solver.Solve(model);
304 CpSolverResponse response = solver.Response;
305 output_.WriteLine($"response = {response}");
306
307 Assert.Equal(CpSolverStatus.Optimal, status);
308
309 Assert.Equal(1, solver.Value(boolvar));
310 Assert.Equal(4, solver.Value(x));
311 Assert.Equal(-1, solver.Value(delta));
312 Assert.Equal(1, solver.Value(squaredDelta));
313 Assert.Equal(new long[] { 1, 4, -1, 1 }, response.Solution);
314 Assert.Equal(1.0, response.ObjectiveValue, 5);
315 }
316
317 [Fact]
318 public void NegativeSquareVar()
319 {
320 CpModel model = new CpModel();
321 BoolVar boolvar = model.NewBoolVar("boolvar");
322 IntVar x = model.NewIntVar(0, 10, "x");
323 IntVar delta = model.NewIntVar(-5, 5, "delta");
324 IntVar squaredDelta = model.NewIntVar(0, 25, "squaredDelta");
325 model.Add(x == 4).OnlyEnforceIf(boolvar);
326 model.Add(x == 0).OnlyEnforceIf(boolvar.Not());
327 model.Add(delta == x - 5);
328 long[,] tuples = { { -5, 25 }, { -4, 16 }, { -3, 9 }, { -2, 4 }, { -1, 1 }, { 0, 0 },
329 { 1, 1 }, { 2, 4 }, { 3, 9 }, { 4, 16 }, { 5, 25 } };
330 model.AddAllowedAssignments(new IntVar[] { delta, squaredDelta }).AddTuples(tuples);
331 model.Minimize(squaredDelta);
332
333 CpSolver solver = new CpSolver();
334 CpSolverStatus status = solver.Solve(model);
335
336 CpSolverResponse response = solver.Response;
337 Assert.Equal(1, solver.Value(boolvar));
338 Assert.Equal(4, solver.Value(x));
339 Assert.Equal(-1, solver.Value(delta));
340 Assert.Equal(1, solver.Value(squaredDelta));
341 Assert.Equal(new long[] { 1, 4, -1, 1 }, response.Solution);
342 Assert.Equal(1.0, response.ObjectiveValue, 6);
343 }
344
345 [Fact]
346 public void Division()
347 {
348 CpModel model = new CpModel();
349 IntVar v1 = model.NewIntVar(0, 10, "v1");
350 IntVar v2 = model.NewIntVar(1, 10, "v2");
351 model.AddDivisionEquality(3, v1, v2);
352 // Console.WriteLine(model.Model);
353
354 SolutionDivisionCounter solution_callback = new SolutionDivisionCounter(3, v1, v2, output_);
355
356 CpSolver solver = new CpSolver();
357 // Tell the solver to search for all solutions.
358 solver.StringParameters = "enumerate_all_solutions:true";
359 CpSolverStatus status = solver.Solve(model, solution_callback);
360
361 Assert.Equal(CpSolverStatus.Optimal, status);
362 Assert.Equal(0, solver.ObjectiveValue);
363
364 Assert.Equal(5, solution_callback.SolutionCount);
365
366 CpSolverResponse response = solver.Response;
367 // Console.WriteLine("response = " + response.ToString());
368 }
369
370 [Fact]
371 public void Modulo()
372 {
373 CpModel model = new CpModel();
374 IntVar v1 = model.NewIntVar(1, 10, "v1");
375 IntVar v2 = model.NewIntVar(1, 10, "v2");
376 model.AddModuloEquality(3, v1, v2);
377 // Console.WriteLine(model.Model);
378
379 SolutionModuloCounter solution_callback = new SolutionModuloCounter(3, v1, v2, output_);
380
381 CpSolver solver = new CpSolver();
382 // Tell the solver to search for all solutions.
383 solver.StringParameters = "enumerate_all_solutions:true";
384 CpSolverStatus status = solver.Solve(model, solution_callback);
385
386 Assert.Equal(CpSolverStatus.Optimal, status);
387 Assert.Equal(0, solver.ObjectiveValue);
388
389 Assert.Equal(11, solution_callback.SolutionCount);
390
391 CpSolverResponse response = solver.Response;
392 // Console.WriteLine("response = " + response.ToString());
393 }
394
395 [Fact]
396 public void ValueElement()
397 {
398 CpModel model = new CpModel();
399 IntVar v1 = model.NewIntVar(1, 10, "v1");
400 IntVar v2 = model.NewIntVar(1, 10, "v2");
401 model.AddElement(v1 + 2, new int[] { 1, 3, 5 }, 5 - v2);
402 Assert.Equal(3, model.Model.Constraints[0].Element.Exprs.Count);
403 }
404
405 public void ExprElement()
406 {
407 CpModel model = new CpModel();
408 IntVar v1 = model.NewIntVar(1, 10, "v1");
409 IntVar v2 = model.NewIntVar(1, 10, "v2");
410 IntVar x = model.NewIntVar(0, 5, "x");
411 IntVar y = model.NewIntVar(0, 5, "y");
412 IntVar z = model.NewIntVar(0, 5, "z");
413 model.AddElement(v1, new LinearExpr[] { x + 2, -y, LinearExpr.Constant(5), 2 * z }, 5 - v2);
414 Assert.Equal(4, model.Model.Constraints[0].Element.Exprs.Count);
415 }
416
417 [Fact]
418 public void LargeWeightedSumLong()
419 {
420 CpModel model = new CpModel();
421 List<IntVar> vars = new List<IntVar>();
422 List<long> coeffs = new List<long>();
423
424 for (int i = 0; i < 100000; ++i)
425 {
426 vars.Add(model.NewBoolVar(""));
427 coeffs.Add(i + 1);
428 }
429
430 var watch = System.Diagnostics.Stopwatch.StartNew();
431 model.Minimize(LinearExpr.WeightedSum(vars, coeffs));
432 watch.Stop();
433 var elapsedMs = watch.ElapsedMilliseconds;
434 output_.WriteLine($"Long: Elapsed time {elapsedMs}");
435 }
436
437 [Fact]
438 public void LargeWeightedSumInt()
439 {
440 CpModel model = new CpModel();
441 List<IntVar> vars = new List<IntVar>();
442 List<int> coeffs = new List<int>();
443
444 for (int i = 0; i < 100000; ++i)
445 {
446 vars.Add(model.NewBoolVar(""));
447 coeffs.Add(i);
448 }
449
450 var watch = System.Diagnostics.Stopwatch.StartNew();
451 model.Minimize(LinearExpr.WeightedSum(vars, coeffs));
452 watch.Stop();
453 var elapsedMs = watch.ElapsedMilliseconds;
454 output_.WriteLine($"Int: Elapsed time {elapsedMs}");
455 }
456
457 [Fact]
458 public void LargeWeightedSumExpr()
459 {
460 CpModel model = new CpModel();
461 List<LinearExpr> exprs = new List<LinearExpr>();
462
463 for (int i = 0; i < 100000; ++i)
464 {
465 exprs.Add(model.NewBoolVar("") * i);
466 }
467
468 var watch = System.Diagnostics.Stopwatch.StartNew();
469 model.Minimize(LinearExpr.Sum(exprs));
470 watch.Stop();
471 var elapsedMs = watch.ElapsedMilliseconds;
472 output_.WriteLine($"Exprs: Elapsed time {elapsedMs}");
473 }
474
475 [Fact]
476 public void LargeWeightedSumBuilder()
477 {
478 CpModel model = new CpModel();
479 List<IntVar> vars = new List<IntVar>();
480 List<long> coeffs = new List<long>();
481
482 for (int i = 0; i < 100000; ++i)
483 {
484 vars.Add(model.NewBoolVar(""));
485 coeffs.Add(i + 1);
486 }
487
488 var watch = System.Diagnostics.Stopwatch.StartNew();
489 LinearExprBuilder obj = LinearExpr.NewBuilder();
490 for (int i = 0; i < 100000; ++i)
491 {
492 obj.AddTerm(vars[i], coeffs[i]);
493 }
494 model.Minimize(obj);
495 watch.Stop();
496 var elapsedMs = watch.ElapsedMilliseconds;
497 output_.WriteLine($"Proto: Elapsed time {elapsedMs}");
498 }
499
500 [Fact]
501 public void LinearExprStaticCompileTest()
502 {
503 output_.WriteLine("LinearExprStaticCompileTest");
504 CpModel model = new CpModel();
505 IntVar v1 = model.NewIntVar(-10, 10, "v1");
506 IntVar v2 = model.NewIntVar(-10, 10, "v2");
507 BoolVar b1 = model.NewBoolVar("b1");
508 BoolVar b2 = model.NewBoolVar("b2");
509 long[] c1 = new long[] { 2L, 4L };
510 int[] c2 = new int[] { 2, 4 };
511 LinearExpr e1 = LinearExpr.Sum(new IntVar[] { v1, v2 });
512 output_.WriteLine(e1.ToString());
513 LinearExpr e2 = LinearExpr.Sum(new ILiteral[] { b1, b2 });
514 output_.WriteLine(e2.ToString());
515 LinearExpr e3 = LinearExpr.Sum(new BoolVar[] { b1, b2 });
516 output_.WriteLine(e3.ToString());
517 LinearExpr e4 = LinearExpr.WeightedSum(new IntVar[] { v1, v2 }, c1);
518 output_.WriteLine(e4.ToString());
519 LinearExpr e5 = LinearExpr.WeightedSum(new ILiteral[] { b1, b2 }, c1);
520 output_.WriteLine(e5.ToString());
521 LinearExpr e6 = LinearExpr.WeightedSum(new BoolVar[] { b1, b2 }, c1);
522 output_.WriteLine(e6.ToString());
523 LinearExpr e7 = LinearExpr.WeightedSum(new IntVar[] { v1, v2 }, c2);
524 output_.WriteLine(e7.ToString());
525 LinearExpr e8 = LinearExpr.WeightedSum(new ILiteral[] { b1, b2 }, c2);
526 output_.WriteLine(e8.ToString());
527 LinearExpr e9 = LinearExpr.WeightedSum(new BoolVar[] { b1, b2 }, c2);
528 output_.WriteLine(e9.ToString());
529 }
530
531 [Fact]
532 public void LinearExprBuilderCompileTest()
533 {
534 output_.WriteLine("LinearExprBuilderCompileTest");
535 CpModel model = new CpModel();
536 IntVar v1 = model.NewIntVar(-10, 10, "v1");
537 IntVar v2 = model.NewIntVar(-10, 10, "v2");
538 BoolVar b1 = model.NewBoolVar("b1");
539 BoolVar b2 = model.NewBoolVar("b2");
540 long[] c1 = new long[] { 2L, 4L };
541 int[] c2 = new int[] { 2, 4 };
542 LinearExpr e1 = LinearExpr.NewBuilder().AddSum(new IntVar[] { v1, v2 });
543 output_.WriteLine(e1.ToString());
544 LinearExpr e2 = LinearExpr.NewBuilder().AddSum(new ILiteral[] { b1, b2 });
545 output_.WriteLine(e2.ToString());
546 LinearExpr e3 = LinearExpr.NewBuilder().AddSum(new BoolVar[] { b1, b2 });
547 output_.WriteLine(e3.ToString());
548 LinearExpr e4 = LinearExpr.NewBuilder().AddWeightedSum(new IntVar[] { v1, v2 }, c1);
549 output_.WriteLine(e4.ToString());
550 LinearExpr e5 = LinearExpr.NewBuilder().AddWeightedSum(new ILiteral[] { b1, b2 }, c1);
551 output_.WriteLine(e5.ToString());
552 LinearExpr e6 = LinearExpr.NewBuilder().AddWeightedSum(new BoolVar[] { b1, b2 }, c1);
553 output_.WriteLine(e6.ToString());
554 LinearExpr e7 = LinearExpr.NewBuilder().AddWeightedSum(new IntVar[] { v1, v2 }, c2);
555 output_.WriteLine(e7.ToString());
556 LinearExpr e8 = LinearExpr.NewBuilder().AddWeightedSum(new ILiteral[] { b1, b2 }, c2);
557 output_.WriteLine(e8.ToString());
558 LinearExpr e9 = LinearExpr.NewBuilder().AddWeightedSum(new BoolVar[] { b1, b2 }, c2);
559 output_.WriteLine(e9.ToString());
560 LinearExpr e10 = LinearExpr.NewBuilder().Add(v1);
561 output_.WriteLine(e10.ToString());
562 LinearExpr e11 = LinearExpr.NewBuilder().Add(b1);
563 output_.WriteLine(e11.ToString());
564 LinearExpr e12 = LinearExpr.NewBuilder().Add(b1.Not());
565 output_.WriteLine(e12.ToString());
566 LinearExpr e13 = LinearExpr.NewBuilder().AddTerm(v1, -1);
567 output_.WriteLine(e13.ToString());
568 LinearExpr e14 = LinearExpr.NewBuilder().AddTerm(b1, -1);
569 output_.WriteLine(e14.ToString());
570 LinearExpr e15 = LinearExpr.NewBuilder().AddTerm(b1.Not(), -2);
571 output_.WriteLine(e15.ToString());
572 }
573
574 [Fact]
575 public void LinearExprIntVarOperatorTest()
576 {
577 output_.WriteLine("LinearExprIntVarOperatorTest");
578 CpModel model = new CpModel();
579 IntVar v = model.NewIntVar(-10, 10, "v");
580 LinearExpr e = v * 2;
581 output_.WriteLine(e.ToString());
582 e = 2 * v;
583 output_.WriteLine(e.ToString());
584 e = v + 2;
585 output_.WriteLine(e.ToString());
586 e = 2 + v;
587 output_.WriteLine(e.ToString());
588 e = v;
589 output_.WriteLine(e.ToString());
590 e = -v;
591 output_.WriteLine(e.ToString());
592 e = 1 - v;
593 output_.WriteLine(e.ToString());
594 e = v - 1;
595 output_.WriteLine(e.ToString());
596 }
597
598 [Fact]
599 public void LinearExprBoolVarOperatorTest()
600 {
601 output_.WriteLine("LinearExprBoolVarOperatorTest");
602 CpModel model = new CpModel();
603 BoolVar v = model.NewBoolVar("v");
604 LinearExpr e = v * 2;
605 output_.WriteLine(e.ToString());
606 e = 2 * v;
607 output_.WriteLine(e.ToString());
608 e = v + 2;
609 output_.WriteLine(e.ToString());
610 e = 2 + v;
611 output_.WriteLine(e.ToString());
612 e = v;
613 output_.WriteLine(e.ToString());
614 e = -v;
615 output_.WriteLine(e.ToString());
616 e = 1 - v;
617 output_.WriteLine(e.ToString());
618 e = v - 1;
619 output_.WriteLine(e.ToString());
620 }
621
622 [Fact]
623 public void TrueLiteralAsExpressionTest()
624 {
625 output_.WriteLine("TrueLiteralAsExpressionTest");
626 CpModel model = new CpModel();
627 ILiteral v = model.TrueLiteral();
628 LinearExpr e = v.AsExpr() * 2;
629 output_.WriteLine(e.ToString());
630 e = 2 * v.AsExpr();
631 output_.WriteLine(e.ToString());
632 e = v.AsExpr() + 2;
633 output_.WriteLine(e.ToString());
634 e = 2 + v.AsExpr();
635 output_.WriteLine(e.ToString());
636 e = v.AsExpr();
637 output_.WriteLine(e.ToString());
638 e = -v.AsExpr();
639 output_.WriteLine(e.ToString());
640 e = 1 - v.AsExpr();
641 output_.WriteLine(e.ToString());
642 e = v.AsExpr() - 1;
643 output_.WriteLine(e.ToString());
644 }
645
646 [Fact]
647 public void FalseLiteralAsExpressionTest()
648 {
649 output_.WriteLine("FalseLiteralAsExpressionTest");
650 CpModel model = new CpModel();
651 ILiteral v = model.FalseLiteral();
652 LinearExpr e = v.AsExpr() * 2;
653 output_.WriteLine(e.ToString());
654 e = 2 * v.AsExpr();
655 output_.WriteLine(e.ToString());
656 e = v.AsExpr() + 2;
657 output_.WriteLine(e.ToString());
658 e = 2 + v.AsExpr();
659 output_.WriteLine(e.ToString());
660 e = v.AsExpr();
661 output_.WriteLine(e.ToString());
662 e = -v.AsExpr();
663 output_.WriteLine(e.ToString());
664 e = 1 - v.AsExpr();
665 output_.WriteLine(e.ToString());
666 e = v.AsExpr() - 1;
667 output_.WriteLine(e.ToString());
668 }
669
670 [Fact]
671 public void LinearExprNotBoolVarOperatorTest()
672 {
673 output_.WriteLine("LinearExprBoolVarNotOperatorTest");
674 CpModel model = new CpModel();
675 ILiteral v = model.NewBoolVar("v");
676 LinearExpr e = v.NotAsExpr() * 2;
677 output_.WriteLine(e.ToString());
678 e = 2 * v.NotAsExpr();
679 output_.WriteLine(e.ToString());
680 e = v.NotAsExpr() + 2;
681 output_.WriteLine(e.ToString());
682 e = 2 + v.NotAsExpr();
683 output_.WriteLine(e.ToString());
684 e = v.NotAsExpr();
685 output_.WriteLine(e.ToString());
686 e = -v.NotAsExpr();
687 output_.WriteLine(e.ToString());
688 e = 1 - v.NotAsExpr();
689 output_.WriteLine(e.ToString());
690 e = v.NotAsExpr() - 1;
691 output_.WriteLine(e.ToString());
692 }
693 [Fact]
694 public void ExportModel()
695 {
696 CpModel model = new CpModel();
697 IntVar v1 = model.NewIntVar(-10, 10, "v1");
698 IntVar v2 = model.NewIntVar(-10, 10, "v2");
699 model.Add(-100000 <= v1 + 2 * v2 <= 100000);
700 model.Minimize(v1 - 2 * v2);
701 Assert.True(model.ExportToFile("test_model_dotnet.pbtxt"));
702 output_.WriteLine("Model written to file");
703 }
704
705 [Fact]
706 public void SolveFromString()
707 {
708 string model_str = @"
709 {
710 ""variables"": [
711 { ""name"": ""C"", ""domain"": [ ""1"", ""9"" ] },
712 { ""name"": ""P"", ""domain"": [ ""0"", ""9"" ] },
713 { ""name"": ""I"", ""domain"": [ ""1"", ""9"" ] },
714 { ""name"": ""S"", ""domain"": [ ""0"", ""9"" ] },
715 { ""name"": ""F"", ""domain"": [ ""1"", ""9"" ] },
716 { ""name"": ""U"", ""domain"": [ ""0"", ""9"" ] },
717 { ""name"": ""N"", ""domain"": [ ""0"", ""9"" ] },
718 { ""name"": ""T"", ""domain"": [ ""1"", ""9"" ] },
719 { ""name"": ""R"", ""domain"": [ ""0"", ""9"" ] },
720 { ""name"": ""E"", ""domain"": [ ""0"", ""9"" ] }
721 ],
722 ""constraints"": [
723 { ""allDiff"": { ""exprs"": [
724 { ""vars"": [""0""], ""coeffs"": [""1""] },
725 { ""vars"": [""1""], ""coeffs"": [""1""] },
726 { ""vars"": [""2""], ""coeffs"": [""1""] },
727 { ""vars"": [""3""], ""coeffs"": [""1""] },
728 { ""vars"": [""4""], ""coeffs"": [""1""] },
729 { ""vars"": [""5""], ""coeffs"": [""1""] },
730 { ""vars"": [""6""], ""coeffs"": [""1""] },
731 { ""vars"": [""7""], ""coeffs"": [""1""] },
732 { ""vars"": [""8""], ""coeffs"": [""1""] },
733 { ""vars"": [""9""], ""coeffs"": [""1""] } ] } },
734 { ""linear"": { ""vars"": [ 6, 5, 9, 4, 3, 7, 8, 2, 0, 1 ], ""coeffs"": [ ""1"", ""0"", ""-1"", ""100"", ""1"", ""-1000"", ""-100"", ""10"", ""10"", ""1"" ], ""domain"": [ ""0"", ""0"" ] } }
735 ]
736 }";
737 CpModelProto model = Google.Protobuf.JsonParser.Default.Parse<CpModelProto>(model_str);
738 SolveWrapper solve_wrapper = new SolveWrapper();
739 CpSolverResponse response = solve_wrapper.Solve(model);
740 output_.WriteLine(response.ToString());
741 }
742
743 [Fact]
744 public void CaptureLog()
745 {
746 output_.WriteLine("CaptureLog test");
747 CpModel model = new CpModel();
748 IntVar v1 = model.NewIntVar(-10, 10, "v1");
749 IntVar v2 = model.NewIntVar(-10, 10, "v2");
750 IntVar v3 = model.NewIntVar(-100000, 100000, "v3");
751 model.AddLinearConstraint(v1 + v2, -1000000, 100000);
752 model.AddLinearConstraint(v1 + 2 * v2 - v3, 0, 100000);
753 model.Maximize(v3);
754 Assert.Equal(v1.Domain.FlattenedIntervals(), new long[] { -10, 10 });
755 // Console.WriteLine("model = " + model.Model.ToString());
756
757 CpSolver solver = new CpSolver();
758 solver.StringParameters = "log_search_progress:true log_to_stdout:false";
759 string log = "";
760 solver.SetLogCallback(message => log += $"{message}\n");
761 solver.Solve(model);
762 Assert.NotEmpty(log);
763 Assert.Contains("OPTIMAL", log);
764 }
765
766 [Fact]
767 public void TestInterval()
768 {
769 output_.WriteLine("TestInterval test");
770 CpModel model = new CpModel();
771 IntVar v = model.NewIntVar(-10, 10, "v");
772 IntervalVar i = model.NewFixedSizeIntervalVar(v, 3, "i");
773 Assert.Equal("v", i.StartExpr().ToString());
774 Assert.Equal("3", i.SizeExpr().ToString());
775 Assert.Equal("(v + 3)", i.EndExpr().ToString());
776 }
777
778 [Fact]
779 public void TestHint()
780 {
781 output_.WriteLine("TestHint test");
782 CpModel model = new CpModel();
783 IntVar v = model.NewIntVar(-10, 10, "v");
784 BoolVar b = model.NewBoolVar("b");
785 BoolVar c = model.NewBoolVar("c");
786 model.AddHint(v, 3);
787 model.AddHint(b, false);
788 model.AddHint(c.Not(), false);
789 Assert.Equal(3, model.Model.SolutionHint.Vars.Count);
790 Assert.Equal(0, model.Model.SolutionHint.Vars[0]);
791 Assert.Equal(3, model.Model.SolutionHint.Values[0]);
792 Assert.Equal(1, model.Model.SolutionHint.Vars[1]);
793 Assert.Equal(0, model.Model.SolutionHint.Values[1]);
794 Assert.Equal(2, model.Model.SolutionHint.Vars[2]);
795 Assert.Equal(1, model.Model.SolutionHint.Values[2]);
796 }
797}
798} // namespace Google.OrTools.Tests
Google.OrTools.Sat.BoolVar
Holds a Boolean variable.
Definition IntegerExpressions.cs:804
Google.OrTools.Sat.BoolVar.Not
ILiteral Not()
Returns the Boolean negation of that variable.
Definition IntegerExpressions.cs:815
Google.OrTools.Sat.Constraint.OnlyEnforceIf
void OnlyEnforceIf(ILiteral lit)
Adds a literal to the constraint.
Definition Constraints.cs:38
Google.OrTools.Sat.CpModelProto
A constraint programming problem.
Definition CpModel.pb.cs:8880
Google.OrTools.Sat.CpModelProto.Variables
pbc::RepeatedField< global::Google.OrTools.Sat.IntegerVariableProto > Variables
The associated Protos should be referred by their index in these fields.
Definition CpModel.pb.cs:8953
Google.OrTools.Sat.CpModelProto.SolutionHint
global::Google.OrTools.Sat.PartialVariableAssignment SolutionHint
Solution hint.
Definition CpModel.pb.cs:9055
Google.OrTools.Sat.CpModelProto.Constraints
pbc::RepeatedField< global::Google.OrTools.Sat.ConstraintProto > Constraints
Definition CpModel.pb.cs:8964
Google.OrTools.Sat.CpModel
Wrapper class around the cp_model proto.
Definition CpModel.cs:24
Google.OrTools.Sat.CpModel.FalseLiteral
ILiteral FalseLiteral()
Returns a constant false literal.
Definition CpModel.cs:118
Google.OrTools.Sat.CpModel.Model
CpModelProto Model
Getters.
Definition CpModel.cs:41
Google.OrTools.Sat.CpModel.NewIntVar
IntVar NewIntVar(long lb, long ub, string name)
Integer variables and constraints.
Definition CpModel.cs:64
Google.OrTools.Sat.CpModel.AddElement
Constraint AddElement(LinearExpr index, IEnumerable< LinearExpr > exprs, LinearExpr target)
Adds the element constraint: exprs[index] == target.
Definition CpModel.cs:239
Google.OrTools.Sat.CpModel.NewBoolVar
BoolVar NewBoolVar(string name)
Creates a Boolean variable with given domain.
Definition CpModel.cs:98
Google.OrTools.Sat.CpModel.AddAllowedAssignments
TableConstraint AddAllowedAssignments(IEnumerable< LinearExpr > exprs)
Adds AllowedAssignments(expressions).
Definition CpModel.cs:348
Google.OrTools.Sat.CpModel.AddMultiplicationEquality
Constraint AddMultiplicationEquality(LinearExpr target, IEnumerable< LinearExpr > exprs)
Adds target == ∏(exprs).
Definition CpModel.cs:773
Google.OrTools.Sat.CpModel.TrueLiteral
ILiteral TrueLiteral()
Returns a constant true literal.
Definition CpModel.cs:108
Google.OrTools.Sat.CpModel.AddHint
void AddHint(IntVar var, long value)
Adds variable hinting to the model.
Definition CpModel.cs:1046
Google.OrTools.Sat.CpModel.Minimize
void Minimize(LinearExpr obj)
Objective.
Definition CpModel.cs:1001
Google.OrTools.Sat.CpModel.AddLinearConstraint
Constraint AddLinearConstraint(LinearExpr expr, long lb, long ub)
Adds lb ≤ expr ≤ ub.
Definition CpModel.cs:141
Google.OrTools.Sat.CpModel.ExportToFile
Boolean ExportToFile(String file)
Write the model as a protocol buffer to file.
Definition CpModel.cs:1169
Google.OrTools.Sat.CpModel.Maximize
void Maximize(LinearExpr obj)
Adds a maximization objective of a linear expression.
Definition CpModel.cs:1007
Google.OrTools.Sat.CpModel.Add
Constraint Add(BoundedLinearExpression lin)
Adds a linear constraint to the model.
Definition CpModel.cs:192
Google.OrTools.Sat.CpObjectiveProto.Vars
pbc::RepeatedField< int > Vars
The linear terms of the objective to minimize. For a maximization problem, one can negate all coeffic...
Definition CpModel.pb.cs:6821
Google.OrTools.Sat.CpObjectiveProto.Coeffs
pbc::RepeatedField< long > Coeffs
Definition CpModel.pb.cs:6832
Google.OrTools.Sat.CpSolverResponse
The response returned by a solver trying to solve a CpModelProto.
Definition CpModel.pb.cs:9645
Google.OrTools.Sat.CpSolverResponse.ObjectiveValue
double ObjectiveValue
Only make sense for an optimization problem. The objective value of the returned solution if it is no...
Definition CpModel.pb.cs:9751
Google.OrTools.Sat.CpSolverResponse.Solution
pbc::RepeatedField< long > Solution
A feasible solution to the given problem. Depending on the returned status it may be optimal or just ...
Definition CpModel.pb.cs:9736
Google.OrTools.Sat.CpSolverResponse.Status
global::Google.OrTools.Sat.CpSolverStatus Status
The status of the solve.
Definition CpModel.pb.cs:9716
Google.OrTools.Sat.CpSolverSolutionCallback
Parent class to create a callback called at each solution.
Definition SearchHelpers.cs:26
Google.OrTools.Sat.CpSolverSolutionCallback.Value
long Value(LinearExpr e)
Returns the value of a linear expression in the current solution.
Definition SearchHelpers.cs:32
Google.OrTools.Sat.CpSolver
Wrapper around the SAT solver.
Definition CpSolver.cs:30
Google.OrTools.Sat.CpSolver.ObjectiveValue
double ObjectiveValue
The best objective value found during search.
Definition CpSolver.cs:114
Google.OrTools.Sat.CpSolver.Value
long Value(IntVar intVar)
Returns the value of an integer variable in the last solution found.
Definition CpSolver.cs:175
Google.OrTools.Sat.CpSolver.Solve
CpSolverStatus Solve(CpModel model, SolutionCallback cb=null)
Solves the given model, and returns the solve status.
Definition CpSolver.cs:32
Google.OrTools.Sat.CpSolver.Response
CpSolverResponse Response
Definition CpSolver.cs:164
Google.OrTools.Sat.CpSolver.SetLogCallback
void SetLogCallback(StringToVoidDelegate del)
Definition CpSolver.cs:143
Google.OrTools.Sat.IntVar
Holds a integer variable with a discrete domain.
Definition IntegerExpressions.cs:720
Google.OrTools.Sat.IntegerVariableProto.Domain
pbc::RepeatedField< long > Domain
The variable domain given as a sorted list of n disjoint intervals [min, max] and encoded as [min_0,...
Definition CpModel.pb.cs:372
Google.OrTools.Sat.IntervalVar.EndExpr
LinearExpr EndExpr()
The end expression of the interval.
Definition IntervalVariables.cs:78
Google.OrTools.Sat.IntervalVar.SizeExpr
LinearExpr SizeExpr()
The size expression of the interval.
Definition IntervalVariables.cs:72
Google.OrTools.Sat.IntervalVar.StartExpr
LinearExpr StartExpr()
The start expression of the interval.
Definition IntervalVariables.cs:66
Google.OrTools.Sat.LinearConstraintProto
The linear sum vars[i] * coeffs[i] must fall in the given domain. The domain has the same format as t...
Definition CpModel.pb.cs:1421
Google.OrTools.Sat.LinearConstraintProto.Coeffs
pbc::RepeatedField< long > Coeffs
Same size as vars.
Definition CpModel.pb.cs:1484
Google.OrTools.Sat.LinearConstraintProto.Domain
pbc::RepeatedField< long > Domain
Definition CpModel.pb.cs:1495
Google.OrTools.Sat.LinearExprBuilder
A builder class for linear expressions.
Definition IntegerExpressions.cs:445
Google.OrTools.Sat.LinearExprBuilder.AddWeightedSum
LinearExprBuilder AddWeightedSum(IEnumerable< LinearExpr > exprs, IEnumerable< long > coefficients)
Adds sum(exprs[i] * coeffs[i]) to the builder.
Definition IntegerExpressions.cs:540
Google.OrTools.Sat.LinearExprBuilder.AddSum
LinearExprBuilder AddSum(IEnumerable< LinearExpr > exprs)
Adds sum(exprs) to the builder.
Definition IntegerExpressions.cs:507
Google.OrTools.Sat.LinearExprBuilder.Add
LinearExprBuilder Add(LinearExpr expr)
Adds expr to the builder.
Definition IntegerExpressions.cs:453
Google.OrTools.Sat.LinearExprBuilder.AddTerm
LinearExprBuilder AddTerm(LinearExpr expr, long coefficient)
Adds expr * coefficient to the builder.
Definition IntegerExpressions.cs:478
Google.OrTools.Sat.LinearExpr
Holds a linear expression: sum (ai * xi) + b.
Definition IntegerExpressions.cs:110
Google.OrTools.Sat.LinearExpr.Constant
static LinearExpr Constant(long value)
Creates a constant expression.
Definition IntegerExpressions.cs:213
Google.OrTools.Sat.LinearExpr.WeightedSum
static LinearExpr WeightedSum(IEnumerable< LinearExpr > exprs, IEnumerable< int > coeffs)
Creates Sum(exprs[i] * coeffs[i]).
Definition IntegerExpressions.cs:130
Google.OrTools.Sat.LinearExpr.NewBuilder
static LinearExprBuilder NewBuilder(int sizeHint=2)
Creates a builder class for linear expression.
Definition IntegerExpressions.cs:219
Google.OrTools.Sat.LinearExpr.Sum
static LinearExpr Sum(IEnumerable< LinearExpr > exprs)
Creates Sum(exprs).
Definition IntegerExpressions.cs:112
Google.OrTools.Sat.SolveWrapper.Solve
Google.OrTools.Sat.CpSolverResponse Solve(Google.OrTools.Sat.CpModelProto model_proto)
Definition SolveWrapper.cs:90
Google.OrTools.Tests.SatSolverTest.SatSolverTest
SatSolverTest(ITestOutputHelper output)
Definition SatSolverTests.cs:112
Google.OrTools.Tests.SatSolverTest.SimpleLinearModelProto
void SimpleLinearModelProto()
CpModelProto.
Definition SatSolverTests.cs:185
Google.OrTools.Util.Domain.FlattenedIntervals
long[] FlattenedIntervals()
Definition Domain.cs:99
SolutionCounter.OnSolutionCallback
override void OnSolutionCallback()
Definition SatSolverTests.cs:29
SolutionDivisionCounter.OnSolutionCallback
override void OnSolutionCallback()
Definition SatSolverTests.cs:56
SolutionDivisionCounter.SolutionDivisionCounter
SolutionDivisionCounter(int result, IntVar a, IntVar b, ITestOutputHelper output)
Definition SatSolverTests.cs:48
SolutionModuloCounter.OnSolutionCallback
override void OnSolutionCallback()
Definition SatSolverTests.cs:86
SolutionModuloCounter.SolutionModuloCounter
SolutionModuloCounter(int result, IntVar a, IntVar b, ITestOutputHelper output)
Definition SatSolverTests.cs:78
Google.OrTools.Sat.ILiteral
Holds a Boolean variable or its negation.
Definition IntegerExpressions.cs:26
Google.OrTools.Sat.ILiteral.NotAsExpr
LinearExpr NotAsExpr()
Returns the Boolean negation of the literal as a linear expression.
Google.OrTools.Sat.ILiteral.AsExpr
LinearExpr AsExpr()
Returns the literal as a linear expression.
Google.OrTools.Sat.CpSolverStatus
CpSolverStatus
The status returned by a solver trying to solve a CpModelProto.
Definition CpModel.pb.cs:219