Google OR-Tools v9.11
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-2024 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 LargeWeightedSumLong()
397 {
398 CpModel model = new CpModel();
399 List<IntVar> vars = new List<IntVar>();
400 List<long> coeffs = new List<long>();
401
402 for (int i = 0; i < 100000; ++i)
403 {
404 vars.Add(model.NewBoolVar(""));
405 coeffs.Add(i + 1);
406 }
407
408 var watch = System.Diagnostics.Stopwatch.StartNew();
409 model.Minimize(LinearExpr.WeightedSum(vars, coeffs));
410 watch.Stop();
411 var elapsedMs = watch.ElapsedMilliseconds;
412 output_.WriteLine($"Long: Elapsed time {elapsedMs}");
413 }
414
415 [Fact]
416 public void LargeWeightedSumInt()
417 {
418 CpModel model = new CpModel();
419 List<IntVar> vars = new List<IntVar>();
420 List<int> coeffs = new List<int>();
421
422 for (int i = 0; i < 100000; ++i)
423 {
424 vars.Add(model.NewBoolVar(""));
425 coeffs.Add(i);
426 }
427
428 var watch = System.Diagnostics.Stopwatch.StartNew();
429 model.Minimize(LinearExpr.WeightedSum(vars, coeffs));
430 watch.Stop();
431 var elapsedMs = watch.ElapsedMilliseconds;
432 output_.WriteLine($"Int: Elapsed time {elapsedMs}");
433 }
434
435 [Fact]
436 public void LargeWeightedSumExpr()
437 {
438 CpModel model = new CpModel();
439 List<LinearExpr> exprs = new List<LinearExpr>();
440
441 for (int i = 0; i < 100000; ++i)
442 {
443 exprs.Add(model.NewBoolVar("") * i);
444 }
445
446 var watch = System.Diagnostics.Stopwatch.StartNew();
447 model.Minimize(LinearExpr.Sum(exprs));
448 watch.Stop();
449 var elapsedMs = watch.ElapsedMilliseconds;
450 output_.WriteLine($"Exprs: Elapsed time {elapsedMs}");
451 }
452
453 [Fact]
454 public void LargeWeightedSumBuilder()
455 {
456 CpModel model = new CpModel();
457 List<IntVar> vars = new List<IntVar>();
458 List<long> coeffs = new List<long>();
459
460 for (int i = 0; i < 100000; ++i)
461 {
462 vars.Add(model.NewBoolVar(""));
463 coeffs.Add(i + 1);
464 }
465
466 var watch = System.Diagnostics.Stopwatch.StartNew();
467 LinearExprBuilder obj = LinearExpr.NewBuilder();
468 for (int i = 0; i < 100000; ++i)
469 {
470 obj.AddTerm(vars[i], coeffs[i]);
471 }
472 model.Minimize(obj);
473 watch.Stop();
474 var elapsedMs = watch.ElapsedMilliseconds;
475 output_.WriteLine($"Proto: Elapsed time {elapsedMs}");
476 }
477
478 [Fact]
479 public void LinearExprStaticCompileTest()
480 {
481 output_.WriteLine("LinearExprStaticCompileTest");
482 CpModel model = new CpModel();
483 IntVar v1 = model.NewIntVar(-10, 10, "v1");
484 IntVar v2 = model.NewIntVar(-10, 10, "v2");
485 BoolVar b1 = model.NewBoolVar("b1");
486 BoolVar b2 = model.NewBoolVar("b2");
487 long[] c1 = new long[] { 2L, 4L };
488 int[] c2 = new int[] { 2, 4 };
489 LinearExpr e1 = LinearExpr.Sum(new IntVar[] { v1, v2 });
490 output_.WriteLine(e1.ToString());
491 LinearExpr e2 = LinearExpr.Sum(new ILiteral[] { b1, b2 });
492 output_.WriteLine(e2.ToString());
493 LinearExpr e3 = LinearExpr.Sum(new BoolVar[] { b1, b2 });
494 output_.WriteLine(e3.ToString());
495 LinearExpr e4 = LinearExpr.WeightedSum(new IntVar[] { v1, v2 }, c1);
496 output_.WriteLine(e4.ToString());
497 LinearExpr e5 = LinearExpr.WeightedSum(new ILiteral[] { b1, b2 }, c1);
498 output_.WriteLine(e5.ToString());
499 LinearExpr e6 = LinearExpr.WeightedSum(new BoolVar[] { b1, b2 }, c1);
500 output_.WriteLine(e6.ToString());
501 LinearExpr e7 = LinearExpr.WeightedSum(new IntVar[] { v1, v2 }, c2);
502 output_.WriteLine(e7.ToString());
503 LinearExpr e8 = LinearExpr.WeightedSum(new ILiteral[] { b1, b2 }, c2);
504 output_.WriteLine(e8.ToString());
505 LinearExpr e9 = LinearExpr.WeightedSum(new BoolVar[] { b1, b2 }, c2);
506 output_.WriteLine(e9.ToString());
507 }
508
509 [Fact]
510 public void LinearExprBuilderCompileTest()
511 {
512 output_.WriteLine("LinearExprBuilderCompileTest");
513 CpModel model = new CpModel();
514 IntVar v1 = model.NewIntVar(-10, 10, "v1");
515 IntVar v2 = model.NewIntVar(-10, 10, "v2");
516 BoolVar b1 = model.NewBoolVar("b1");
517 BoolVar b2 = model.NewBoolVar("b2");
518 long[] c1 = new long[] { 2L, 4L };
519 int[] c2 = new int[] { 2, 4 };
520 LinearExpr e1 = LinearExpr.NewBuilder().AddSum(new IntVar[] { v1, v2 });
521 output_.WriteLine(e1.ToString());
522 LinearExpr e2 = LinearExpr.NewBuilder().AddSum(new ILiteral[] { b1, b2 });
523 output_.WriteLine(e2.ToString());
524 LinearExpr e3 = LinearExpr.NewBuilder().AddSum(new BoolVar[] { b1, b2 });
525 output_.WriteLine(e3.ToString());
526 LinearExpr e4 = LinearExpr.NewBuilder().AddWeightedSum(new IntVar[] { v1, v2 }, c1);
527 output_.WriteLine(e4.ToString());
528 LinearExpr e5 = LinearExpr.NewBuilder().AddWeightedSum(new ILiteral[] { b1, b2 }, c1);
529 output_.WriteLine(e5.ToString());
530 LinearExpr e6 = LinearExpr.NewBuilder().AddWeightedSum(new BoolVar[] { b1, b2 }, c1);
531 output_.WriteLine(e6.ToString());
532 LinearExpr e7 = LinearExpr.NewBuilder().AddWeightedSum(new IntVar[] { v1, v2 }, c2);
533 output_.WriteLine(e7.ToString());
534 LinearExpr e8 = LinearExpr.NewBuilder().AddWeightedSum(new ILiteral[] { b1, b2 }, c2);
535 output_.WriteLine(e8.ToString());
536 LinearExpr e9 = LinearExpr.NewBuilder().AddWeightedSum(new BoolVar[] { b1, b2 }, c2);
537 output_.WriteLine(e9.ToString());
538 LinearExpr e10 = LinearExpr.NewBuilder().Add(v1);
539 output_.WriteLine(e10.ToString());
540 LinearExpr e11 = LinearExpr.NewBuilder().Add(b1);
541 output_.WriteLine(e11.ToString());
542 LinearExpr e12 = LinearExpr.NewBuilder().Add(b1.Not());
543 output_.WriteLine(e12.ToString());
544 LinearExpr e13 = LinearExpr.NewBuilder().AddTerm(v1, -1);
545 output_.WriteLine(e13.ToString());
546 LinearExpr e14 = LinearExpr.NewBuilder().AddTerm(b1, -1);
547 output_.WriteLine(e14.ToString());
548 LinearExpr e15 = LinearExpr.NewBuilder().AddTerm(b1.Not(), -2);
549 output_.WriteLine(e15.ToString());
550 }
551
552 [Fact]
553 public void LinearExprIntVarOperatorTest()
554 {
555 output_.WriteLine("LinearExprIntVarOperatorTest");
556 CpModel model = new CpModel();
557 IntVar v = model.NewIntVar(-10, 10, "v");
558 LinearExpr e = v * 2;
559 output_.WriteLine(e.ToString());
560 e = 2 * v;
561 output_.WriteLine(e.ToString());
562 e = v + 2;
563 output_.WriteLine(e.ToString());
564 e = 2 + v;
565 output_.WriteLine(e.ToString());
566 e = v;
567 output_.WriteLine(e.ToString());
568 e = -v;
569 output_.WriteLine(e.ToString());
570 e = 1 - v;
571 output_.WriteLine(e.ToString());
572 e = v - 1;
573 output_.WriteLine(e.ToString());
574 }
575
576 [Fact]
577 public void LinearExprBoolVarOperatorTest()
578 {
579 output_.WriteLine("LinearExprBoolVarOperatorTest");
580 CpModel model = new CpModel();
581 BoolVar v = model.NewBoolVar("v");
582 LinearExpr e = v * 2;
583 output_.WriteLine(e.ToString());
584 e = 2 * v;
585 output_.WriteLine(e.ToString());
586 e = v + 2;
587 output_.WriteLine(e.ToString());
588 e = 2 + v;
589 output_.WriteLine(e.ToString());
590 e = v;
591 output_.WriteLine(e.ToString());
592 e = -v;
593 output_.WriteLine(e.ToString());
594 e = 1 - v;
595 output_.WriteLine(e.ToString());
596 e = v - 1;
597 output_.WriteLine(e.ToString());
598 }
599
600 [Fact]
601 public void TrueLiteralAsExpressionTest()
602 {
603 output_.WriteLine("TrueLiteralAsExpressionTest");
604 CpModel model = new CpModel();
605 ILiteral v = model.TrueLiteral();
606 LinearExpr e = v.AsExpr() * 2;
607 output_.WriteLine(e.ToString());
608 e = 2 * v.AsExpr();
609 output_.WriteLine(e.ToString());
610 e = v.AsExpr() + 2;
611 output_.WriteLine(e.ToString());
612 e = 2 + v.AsExpr();
613 output_.WriteLine(e.ToString());
614 e = v.AsExpr();
615 output_.WriteLine(e.ToString());
616 e = -v.AsExpr();
617 output_.WriteLine(e.ToString());
618 e = 1 - v.AsExpr();
619 output_.WriteLine(e.ToString());
620 e = v.AsExpr() - 1;
621 output_.WriteLine(e.ToString());
622 }
623
624 [Fact]
625 public void FalseLiteralAsExpressionTest()
626 {
627 output_.WriteLine("FalseLiteralAsExpressionTest");
628 CpModel model = new CpModel();
629 ILiteral v = model.FalseLiteral();
630 LinearExpr e = v.AsExpr() * 2;
631 output_.WriteLine(e.ToString());
632 e = 2 * v.AsExpr();
633 output_.WriteLine(e.ToString());
634 e = v.AsExpr() + 2;
635 output_.WriteLine(e.ToString());
636 e = 2 + v.AsExpr();
637 output_.WriteLine(e.ToString());
638 e = v.AsExpr();
639 output_.WriteLine(e.ToString());
640 e = -v.AsExpr();
641 output_.WriteLine(e.ToString());
642 e = 1 - v.AsExpr();
643 output_.WriteLine(e.ToString());
644 e = v.AsExpr() - 1;
645 output_.WriteLine(e.ToString());
646 }
647
648 [Fact]
649 public void LinearExprNotBoolVarOperatorTest()
650 {
651 output_.WriteLine("LinearExprBoolVarNotOperatorTest");
652 CpModel model = new CpModel();
653 ILiteral v = model.NewBoolVar("v");
654 LinearExpr e = v.NotAsExpr() * 2;
655 output_.WriteLine(e.ToString());
656 e = 2 * v.NotAsExpr();
657 output_.WriteLine(e.ToString());
658 e = v.NotAsExpr() + 2;
659 output_.WriteLine(e.ToString());
660 e = 2 + v.NotAsExpr();
661 output_.WriteLine(e.ToString());
662 e = v.NotAsExpr();
663 output_.WriteLine(e.ToString());
664 e = -v.NotAsExpr();
665 output_.WriteLine(e.ToString());
666 e = 1 - v.NotAsExpr();
667 output_.WriteLine(e.ToString());
668 e = v.NotAsExpr() - 1;
669 output_.WriteLine(e.ToString());
670 }
671 [Fact]
672 public void ExportModel()
673 {
674 CpModel model = new CpModel();
675 IntVar v1 = model.NewIntVar(-10, 10, "v1");
676 IntVar v2 = model.NewIntVar(-10, 10, "v2");
677 model.Add(-100000 <= v1 + 2 * v2 <= 100000);
678 model.Minimize(v1 - 2 * v2);
679 Assert.True(model.ExportToFile("test_model_dotnet.pbtxt"));
680 output_.WriteLine("Model written to file");
681 }
682
683 [Fact]
684 public void SolveFromString()
685 {
686 string model_str = @"
687 {
688 ""variables"": [
689 { ""name"": ""C"", ""domain"": [ ""1"", ""9"" ] },
690 { ""name"": ""P"", ""domain"": [ ""0"", ""9"" ] },
691 { ""name"": ""I"", ""domain"": [ ""1"", ""9"" ] },
692 { ""name"": ""S"", ""domain"": [ ""0"", ""9"" ] },
693 { ""name"": ""F"", ""domain"": [ ""1"", ""9"" ] },
694 { ""name"": ""U"", ""domain"": [ ""0"", ""9"" ] },
695 { ""name"": ""N"", ""domain"": [ ""0"", ""9"" ] },
696 { ""name"": ""T"", ""domain"": [ ""1"", ""9"" ] },
697 { ""name"": ""R"", ""domain"": [ ""0"", ""9"" ] },
698 { ""name"": ""E"", ""domain"": [ ""0"", ""9"" ] }
699 ],
700 ""constraints"": [
701 { ""allDiff"": { ""exprs"": [
702 { ""vars"": [""0""], ""coeffs"": [""1""] },
703 { ""vars"": [""1""], ""coeffs"": [""1""] },
704 { ""vars"": [""2""], ""coeffs"": [""1""] },
705 { ""vars"": [""3""], ""coeffs"": [""1""] },
706 { ""vars"": [""4""], ""coeffs"": [""1""] },
707 { ""vars"": [""5""], ""coeffs"": [""1""] },
708 { ""vars"": [""6""], ""coeffs"": [""1""] },
709 { ""vars"": [""7""], ""coeffs"": [""1""] },
710 { ""vars"": [""8""], ""coeffs"": [""1""] },
711 { ""vars"": [""9""], ""coeffs"": [""1""] } ] } },
712 { ""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"" ] } }
713 ]
714 }";
715 CpModelProto model = Google.Protobuf.JsonParser.Default.Parse<CpModelProto>(model_str);
716 SolveWrapper solve_wrapper = new SolveWrapper();
717 CpSolverResponse response = solve_wrapper.Solve(model);
718 output_.WriteLine(response.ToString());
719 }
720
721 [Fact]
722 public void CaptureLog()
723 {
724 output_.WriteLine("CaptureLog test");
725 CpModel model = new CpModel();
726 IntVar v1 = model.NewIntVar(-10, 10, "v1");
727 IntVar v2 = model.NewIntVar(-10, 10, "v2");
728 IntVar v3 = model.NewIntVar(-100000, 100000, "v3");
729 model.AddLinearConstraint(v1 + v2, -1000000, 100000);
730 model.AddLinearConstraint(v1 + 2 * v2 - v3, 0, 100000);
731 model.Maximize(v3);
732 Assert.Equal(v1.Domain.FlattenedIntervals(), new long[] { -10, 10 });
733 // Console.WriteLine("model = " + model.Model.ToString());
734
735 CpSolver solver = new CpSolver();
736 solver.StringParameters = "log_search_progress:true log_to_stdout:false";
737 string log = "";
738 solver.SetLogCallback(message => log += $"{message}\n");
739 solver.Solve(model);
740 Assert.NotEmpty(log);
741 Assert.Contains("OPTIMAL", log);
742 }
743
744 [Fact]
745 public void TestInterval()
746 {
747 output_.WriteLine("TestInterval test");
748 CpModel model = new CpModel();
749 IntVar v = model.NewIntVar(-10, 10, "v");
750 IntervalVar i = model.NewFixedSizeIntervalVar(v, 3, "i");
751 Assert.Equal("v", i.StartExpr().ToString());
752 Assert.Equal("3", i.SizeExpr().ToString());
753 Assert.Equal("(v + 3)", i.EndExpr().ToString());
754 }
755
756 [Fact]
757 public void TestHint()
758 {
759 output_.WriteLine("TestHint test");
760 CpModel model = new CpModel();
761 IntVar v = model.NewIntVar(-10, 10, "v");
762 BoolVar b = model.NewBoolVar("b");
763 BoolVar c = model.NewBoolVar("c");
764 model.AddHint(v, 3);
765 model.AddHint(b, false);
766 model.AddHint(c.Not(), false);
767 Assert.Equal(3, model.Model.SolutionHint.Vars.Count);
768 Assert.Equal(0, model.Model.SolutionHint.Vars[0]);
769 Assert.Equal(3, model.Model.SolutionHint.Values[0]);
770 Assert.Equal(1, model.Model.SolutionHint.Vars[1]);
771 Assert.Equal(0, model.Model.SolutionHint.Values[1]);
772 Assert.Equal(2, model.Model.SolutionHint.Vars[2]);
773 Assert.Equal(1, model.Model.SolutionHint.Values[2]);
774 }
775}
776} // 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:8463
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:8536
Google.OrTools.Sat.CpModelProto.SolutionHint
global::Google.OrTools.Sat.PartialVariableAssignment SolutionHint
Solution hint.
Definition CpModel.pb.cs:8638
Google.OrTools.Sat.CpModelProto.Constraints
pbc::RepeatedField< global::Google.OrTools.Sat.ConstraintProto > Constraints
Definition CpModel.pb.cs:8547
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.NewBoolVar
BoolVar NewBoolVar(string name)
Creates a Boolean variable with given domain.
Definition CpModel.cs:98
Google.OrTools.Sat.CpModel.AddMultiplicationEquality
Constraint AddMultiplicationEquality(LinearExpr target, IEnumerable< LinearExpr > exprs)
Adds target == ∏(exprs).
Definition CpModel.cs:770
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:1043
Google.OrTools.Sat.CpModel.Minimize
void Minimize(LinearExpr obj)
Objective.
Definition CpModel.cs:998
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:1166
Google.OrTools.Sat.CpModel.Maximize
void Maximize(LinearExpr obj)
Adds a maximization objective of a linear expression.
Definition CpModel.cs:1004
Google.OrTools.Sat.CpModel.Add
Constraint Add(BoundedLinearExpression lin)
Adds a linear constraint to the model.
Definition CpModel.cs:192
Google.OrTools.Sat.CpModel.AddAllowedAssignments
TableConstraint AddAllowedAssignments(IEnumerable< IntVar > vars)
Adds AllowedAssignments(variables).
Definition CpModel.cs:347
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:6461
Google.OrTools.Sat.CpObjectiveProto.Coeffs
pbc::RepeatedField< long > Coeffs
Definition CpModel.pb.cs:6472
Google.OrTools.Sat.CpSolverResponse
The response returned by a solver trying to solve a CpModelProto.
Definition CpModel.pb.cs:9212
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:9317
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:9302
Google.OrTools.Sat.CpSolverResponse.Status
global::Google.OrTools.Sat.CpSolverStatus Status
The status of the solve.
Definition CpModel.pb.cs:9282
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:362
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:1371
Google.OrTools.Sat.LinearConstraintProto.Coeffs
pbc::RepeatedField< long > Coeffs
Same size as vars.
Definition CpModel.pb.cs:1434
Google.OrTools.Sat.LinearConstraintProto.Domain
pbc::RepeatedField< long > Domain
Definition CpModel.pb.cs:1445
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.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:209