diff --git a/examples/python/balance_group_sat.py b/examples/python/balance_group_sat.py index 752da1b827..86e4bf35b1 100644 --- a/examples/python/balance_group_sat.py +++ b/examples/python/balance_group_sat.py @@ -10,7 +10,6 @@ # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. # See the License for the specific language governing permissions and # limitations under the License. - """We are trying to group items in equal sized groups. Each item has a color and a value. We want the sum of values of each group to diff --git a/ortools/sat/csharp/CpSolver.cs b/ortools/sat/csharp/CpSolver.cs index 1a4746721a..7b3fc16b2d 100644 --- a/ortools/sat/csharp/CpSolver.cs +++ b/ortools/sat/csharp/CpSolver.cs @@ -11,254 +11,256 @@ // See the License for the specific language governing permissions and // limitations under the License. -namespace Google.OrTools.Sat -{ using System; using System.Collections.Generic; -public class CpSolverSolutionCallback : SolutionCallback -{ - public long Value(IntegerExpression e) - { - List exprs = new List(); - List coeffs = new List(); - exprs.Add(e); - coeffs.Add(1L); - long constant = 0; - - while (exprs.Count > 0) - { - IntegerExpression expr = exprs[0]; - exprs.RemoveAt(0); - long coeff = coeffs[0]; - coeffs.RemoveAt(0); - if (coeff == 0) continue; - - if (expr is ProductCst) - { - ProductCst p = (ProductCst)expr; - if (p.Coeff != 0) - { - exprs.Add(p.Expr); - coeffs.Add(p.Coeff * coeff); - } - } - else if (expr is SumArray) - { - SumArray a = (SumArray)expr; - constant += coeff * a.Constant; - foreach (IntegerExpression sub in a.Expressions) - { - exprs.Add(sub); - coeffs.Add(coeff); - } - } - else if (expr is IntVar) - { - int index = expr.Index; - long value = SolutionIntegerValue(index); - constant += coeff * value; - } - else if (expr is NotBooleanVariable) - { - throw new ArgumentException( - "Cannot evaluate a literal in an integer expression."); - } - else - { - throw new ArgumentException("Cannot evaluate '" + expr.ToString() + - "' in an integer expression"); - } - } - return constant; - } - - public Boolean BooleanValue(ILiteral literal) - { - if (literal is IntVar || literal is NotBooleanVariable) - { - int index = literal.GetIndex(); - return SolutionBooleanValue(index); - } - else - { - throw new ArgumentException("Cannot evaluate '" + literal.ToString() + - "' as a boolean literal"); - } - } -} - -public class CpSolver +namespace Google.OrTools.Sat { - public CpSolverStatus Solve(CpModel model) + public class CpSolverSolutionCallback : SolutionCallback { - if (string_parameters_ != null) + public long Value(IntegerExpression e) { - response_ = SatHelper.SolveWithStringParameters(model.Model, - string_parameters_); - } - else - { - response_ = SatHelper.Solve(model.Model); - } - return response_.Status; - } + List exprs = new List(); + List coeffs = new List(); + exprs.Add(e); + coeffs.Add(1L); + long constant = 0; - public CpSolverStatus SolveWithSolutionCallback(CpModel model, - SolutionCallback cb) - { - if (string_parameters_ != null) - { - response_ = SatHelper.SolveWithStringParametersAndSolutionCallback( - model.Model, string_parameters_, cb); - } - else - { - response_ = SatHelper.Solve(model.Model); - } - return response_.Status; - } - - public CpSolverStatus SearchAllSolutions(CpModel model, SolutionCallback cb) - { - if (string_parameters_ != null) - { - string extra_parameters = " enumerate_all_solutions:true"; - response_ = - SatHelper.SolveWithStringParametersAndSolutionCallback( - model.Model, string_parameters_ + extra_parameters, cb); - } - else - { - string parameters = "enumerate_all_solutions:true"; - response_ = SatHelper.SolveWithStringParametersAndSolutionCallback( - model.Model, parameters, cb); - } - return response_.Status; - } - - public String ResponseStats() { - return SatHelper.SolverResponseStats(response_); - } - - public double ObjectiveValue - { - get { return response_.ObjectiveValue; } - } - - public double BestObjectiveBound - { - get { return response_.BestObjectiveBound; } - } - - public string StringParameters - { - get { return string_parameters_; } - set { string_parameters_ = value; } - } - - public CpSolverResponse Response - { - get { return response_; } - } - - public long Value(IntegerExpression e) - { - List exprs = new List(); - List coeffs = new List(); - exprs.Add(e); - coeffs.Add(1L); - long constant = 0; - - while (exprs.Count > 0) - { - IntegerExpression expr = exprs[0]; - exprs.RemoveAt(0); - long coeff = coeffs[0]; - coeffs.RemoveAt(0); - if (coeff == 0) continue; - - if (expr is ProductCst) + while (exprs.Count > 0) { - ProductCst p = (ProductCst)expr; - if (p.Coeff != 0) + IntegerExpression expr = exprs[0]; + exprs.RemoveAt(0); + long coeff = coeffs[0]; + coeffs.RemoveAt(0); + if (coeff == 0) continue; + + if (expr is ProductCst) { - exprs.Add(p.Expr); - coeffs.Add(p.Coeff * coeff); + ProductCst p = (ProductCst)expr; + if (p.Coeff != 0) + { + exprs.Add(p.Expr); + coeffs.Add(p.Coeff * coeff); + } + } + else if (expr is SumArray) + { + SumArray a = (SumArray)expr; + constant += coeff * a.Constant; + foreach (IntegerExpression sub in a.Expressions) + { + exprs.Add(sub); + coeffs.Add(coeff); + } + } + else if (expr is IntVar) + { + int index = expr.Index; + long value = SolutionIntegerValue(index); + constant += coeff * value; + } + else if (expr is NotBooleanVariable) + { + throw new ArgumentException( + "Cannot evaluate a literal in an integer expression."); + } + else + { + throw new ArgumentException("Cannot evaluate '" + expr.ToString() + + "' in an integer expression"); } } - else if (expr is SumArray) + return constant; + } + + public Boolean BooleanValue(ILiteral literal) + { + if (literal is IntVar || literal is NotBooleanVariable) { - SumArray a = (SumArray)expr; - constant += coeff * a.Constant; - foreach (IntegerExpression sub in a.Expressions) - { - exprs.Add(sub); - coeffs.Add(coeff); - } - } - else if (expr is IntVar) - { - int index = expr.Index; - long value = index >= 0 ? response_.Solution[index] - : -response_.Solution[-index - 1]; - constant += coeff * value; - } - else if (expr is NotBooleanVariable) - { - throw new ArgumentException( - "Cannot evaluate a literal in an integer expression."); + int index = literal.GetIndex(); + return SolutionBooleanValue(index); } else { - throw new ArgumentException("Cannot evaluate '" + expr.ToString() + - "' in an integer expression"); + throw new ArgumentException("Cannot evaluate '" + literal.ToString() + + "' as a boolean literal"); } } - return constant; } - public Boolean BooleanValue(ILiteral literal) + public class CpSolver { - if (literal is IntVar || literal is NotBooleanVariable) + + public CpSolverStatus Solve(CpModel model) { - int index = literal.GetIndex(); - if (index >= 0) + if (string_parameters_ != null) { - return response_.Solution[index] != 0; + response_ = SatHelper.SolveWithStringParameters(model.Model, + string_parameters_); } else { - return response_.Solution[index] == 0; + response_ = SatHelper.Solve(model.Model); + } + return response_.Status; + } + + public CpSolverStatus SolveWithSolutionCallback(CpModel model, + SolutionCallback cb) + { + if (string_parameters_ != null) + { + response_ = SatHelper.SolveWithStringParametersAndSolutionCallback( + model.Model, string_parameters_, cb); + } + else + { + response_ = SatHelper.Solve(model.Model); + } + return response_.Status; + } + + public CpSolverStatus SearchAllSolutions(CpModel model, SolutionCallback cb) + { + if (string_parameters_ != null) + { + string extra_parameters = " enumerate_all_solutions:true"; + response_ = + SatHelper.SolveWithStringParametersAndSolutionCallback( + model.Model, string_parameters_ + extra_parameters, cb); + } + else + { + string parameters = "enumerate_all_solutions:true"; + response_ = SatHelper.SolveWithStringParametersAndSolutionCallback( + model.Model, parameters, cb); + } + return response_.Status; + } + + public String ResponseStats() + { + return SatHelper.SolverResponseStats(response_); + } + + public double ObjectiveValue + { + get { return response_.ObjectiveValue; } + } + + public double BestObjectiveBound + { + get { return response_.BestObjectiveBound; } + } + + public string StringParameters + { + get { return string_parameters_; } + set { string_parameters_ = value; } + } + + public CpSolverResponse Response + { + get { return response_; } + } + + public long Value(IntegerExpression e) + { + List exprs = new List(); + List coeffs = new List(); + exprs.Add(e); + coeffs.Add(1L); + long constant = 0; + + while (exprs.Count > 0) + { + IntegerExpression expr = exprs[0]; + exprs.RemoveAt(0); + long coeff = coeffs[0]; + coeffs.RemoveAt(0); + if (coeff == 0) continue; + + if (expr is ProductCst) + { + ProductCst p = (ProductCst)expr; + if (p.Coeff != 0) + { + exprs.Add(p.Expr); + coeffs.Add(p.Coeff * coeff); + } + } + else if (expr is SumArray) + { + SumArray a = (SumArray)expr; + constant += coeff * a.Constant; + foreach (IntegerExpression sub in a.Expressions) + { + exprs.Add(sub); + coeffs.Add(coeff); + } + } + else if (expr is IntVar) + { + int index = expr.Index; + long value = index >= 0 ? response_.Solution[index] + : -response_.Solution[-index - 1]; + constant += coeff * value; + } + else if (expr is NotBooleanVariable) + { + throw new ArgumentException( + "Cannot evaluate a literal in an integer expression."); + } + else + { + throw new ArgumentException("Cannot evaluate '" + expr.ToString() + + "' in an integer expression"); + } + } + return constant; + } + + public Boolean BooleanValue(ILiteral literal) + { + if (literal is IntVar || literal is NotBooleanVariable) + { + int index = literal.GetIndex(); + if (index >= 0) + { + return response_.Solution[index] != 0; + } + else + { + return response_.Solution[index] == 0; + } + } + else + { + throw new ArgumentException("Cannot evaluate '" + literal.ToString() + + "' as a boolean literal"); } } - else + + public long NumBranches() { - throw new ArgumentException("Cannot evaluate '" + literal.ToString() + - "' as a boolean literal"); + return response_.NumBranches; } + + public long NumConflicts() + { + return response_.NumConflicts; + } + + public double WallTime() + { + return response_.WallTime; + } + + + private CpModelProto model_; + private CpSolverResponse response_; + string string_parameters_; } - public long NumBranches() - { - return response_.NumBranches; - } - - public long NumConflicts() - { - return response_.NumConflicts; - } - - public double WallTime() - { - return response_.WallTime; - } - - - private CpModelProto model_; - private CpSolverResponse response_; - string string_parameters_; -} - } // namespace Google.OrTools.Sat diff --git a/ortools/sat/doc/boolean_logic.md b/ortools/sat/doc/boolean_logic.md index 47c52724e7..320d3f37e6 100644 --- a/ortools/sat/doc/boolean_logic.md +++ b/ortools/sat/doc/boolean_logic.md @@ -229,11 +229,12 @@ public class CodeSamplesSat { CpModel model = new CpModel(); IntVar x = model.NewBoolVar("x"); - IntVar y = model.newBoolVar("y"); - model.AddBoolOr(new ILiteral[] {x, y.Not()}); + IntVar y = model.NewBoolVar("y"); + model.AddBoolOr(new ILiteral[] { x, y.Not() }); } - static void Main() { + static void Main() + { BoolOrSample(); } } diff --git a/ortools/sat/doc/channeling.md b/ortools/sat/doc/channeling.md index 2e8d09cec2..cd91da97fc 100644 --- a/ortools/sat/doc/channeling.md +++ b/ortools/sat/doc/channeling.md @@ -672,7 +672,7 @@ public class CodeSamplesSat int slack_capacity = 20; int num_bins = 10; - int[,] items = new int[,] { {20, 12}, {15, 12}, {30, 8}, {45, 5} }; + int[,] items = new int[,] { { 20, 12 }, { 15, 12 }, { 30, 8 }, { 45, 5 } }; int num_items = items.GetLength(0); // Model. @@ -705,7 +705,8 @@ public class CodeSamplesSat // Links load and x. int[] sizes = new int[num_items]; - for (int i = 0; i < num_items; ++i) { + for (int i = 0; i < num_items; ++i) + { sizes[i] = items[i, 0]; } for (int b = 0; b < num_bins; ++b) @@ -766,6 +767,7 @@ public class CodeSamplesSat Console.WriteLine(String.Format(" - branches : {0}", solver.NumBranches())); Console.WriteLine(String.Format(" - wall time : {0} s", + solver.WallTime())); } static void Main() diff --git a/ortools/sat/doc/solver.md b/ortools/sat/doc/solver.md index ab28dd5a6c..3bddc8ac47 100644 --- a/ortools/sat/doc/solver.md +++ b/ortools/sat/doc/solver.md @@ -351,7 +351,7 @@ public class CodeSamplesSat CpSolver solver = new CpSolver(); // Adds a time limit. Parameters are stored as strings in the solver. - solver.StringParameters = "max_time_in_seconds:10.0" ; + solver.StringParameters = "max_time_in_seconds:10.0"; CpSolverStatus status = solver.Solve(model); @@ -592,18 +592,16 @@ public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback public override void OnSolutionCallback() { + Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", + solution_count_, WallTime())); + Console.WriteLine( + String.Format(" objective value = {0}", ObjectiveValue())); + foreach (IntVar v in variables_) { - Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", - solution_count_, WallTime())); Console.WriteLine( - String.Format(" objective value = {0}", ObjectiveValue())); - foreach (IntVar v in variables_) - { - Console.WriteLine( - String.Format(" {0} = {1}", v.ShortString(), Value(v))); - } - solution_count_++; + String.Format(" {0} = {1}", v.ShortString(), Value(v))); } + solution_count_++; } public int SolutionCount() @@ -624,9 +622,9 @@ public class CodeSamplesSat // Creates the variables. int num_vals = 3; - IntVar x = model.NewIntVar(0, num_vals - 1, 'x'); - IntVar y = model.NewIntVar(0, num_vals - 1, 'y'); - IntVar z = model.NewIntVar(0, num_vals - 1, 'z'); + IntVar x = model.NewIntVar(0, num_vals - 1, "x"); + IntVar y = model.NewIntVar(0, num_vals - 1, "y"); + IntVar z = model.NewIntVar(0, num_vals - 1, "z"); // Adds a different constraint. model.Add(x != y); @@ -637,10 +635,10 @@ public class CodeSamplesSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithObjective cb = - new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z}); + new VarArraySolutionPrinterWithObjective(new IntVar[] { x, y, z }); solver.SolveWithSolutionCallback(model, cb); - Console.WriteLine(String.Format('Number of solutions found: {0}', - cb.SolutionCount())); + Console.WriteLine(String.Format("Number of solutions found: {0}", + cb.SolutionCount())); } static void Main() @@ -689,7 +687,7 @@ class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback): return self.__solution_count -def MinimalSatSearchForAllSolutions(): +def SolveAllSolutions(): """Showcases calling the solver to search for all solutions.""" # Creates the model. model = cp_model.CpModel() @@ -709,7 +707,7 @@ def MinimalSatSearchForAllSolutions(): print('Number of solutions found: %i' % solution_printer.SolutionCount()) -MinimalSatSearchForAllSolutions() +SolveAllSolutions() ``` ### C++ code @@ -901,7 +899,7 @@ public class CodeSamplesSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = - new VarArraySolutionPrinter(new IntVar[] {x, y, z}); + new VarArraySolutionPrinter(new IntVar[] { x, y, z }); solver.SearchAllSolutions(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); @@ -1130,22 +1128,27 @@ CpSolverSolutionCallback.OnSolutionCallback(). using System; using Google.OrTools.Sat; -public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback { +public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback +{ public VarArraySolutionPrinterWithLimit(IntVar[] variables, - int solution_limit) { + int solution_limit) + { variables_ = variables; solution_limit_ = solution_limit; } - public override void OnSolutionCallback() { + public override void OnSolutionCallback() + { Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime())); - foreach (IntVar v in variables_) { + foreach (IntVar v in variables_) + { Console.WriteLine( String.Format(" {0} = {1}", v.ShortString(), Value(v))); } solution_count_++; - if (solution_count_ >= solution_limit_) { + if (solution_count_ >= solution_limit_) + { Console.WriteLine( String.Format("Stopping search after {0} solutions", solution_limit_)); @@ -1153,7 +1156,8 @@ public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback { } } - public int SolutionCount() { + public int SolutionCount() + { return solution_count_; } @@ -1162,8 +1166,10 @@ public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback { private int solution_limit_; } -public class CodeSamplesSat { - static void StopAfterNSolutions() { +public class CodeSamplesSat +{ + static void StopAfterNSolutions() + { // Creates the model. CpModel model = new CpModel(); // Creates the variables. @@ -1176,13 +1182,14 @@ public class CodeSamplesSat { // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithLimit cb = - new VarArraySolutionPrinterWithLimit(new IntVar[] {x, y, z}, 5); + new VarArraySolutionPrinterWithLimit(new IntVar[] { x, y, z }, 5); solver.SearchAllSolutions(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); } - static void Main() { + static void Main() + { StopAfterNSolutions(); } } diff --git a/ortools/sat/samples/binpacking_problem.cs b/ortools/sat/samples/binpacking_problem.cs index dbf881b411..75dbab49d8 100644 --- a/ortools/sat/samples/binpacking_problem.cs +++ b/ortools/sat/samples/binpacking_problem.cs @@ -14,14 +14,16 @@ using System; using Google.OrTools.Sat; -public class CodeSamplesSat { - static void BinpackingProblem() { +public class CodeSamplesSat +{ + static void BinpackingProblem() + { // Data. int bin_capacity = 100; int slack_capacity = 20; int num_bins = 10; - int[,] items = new int[,] { {20, 12}, {15, 12}, {30, 8}, {45, 5} }; + int[,] items = new int[,] { { 20, 12 }, { 15, 12 }, { 30, 8 }, { 45, 5 } }; int num_items = items.GetLength(0); // Model. @@ -29,42 +31,51 @@ public class CodeSamplesSat { // Main variables. IntVar[,] x = new IntVar[num_items, num_bins]; - for (int i = 0; i < num_items; ++i) { + for (int i = 0; i < num_items; ++i) + { int num_copies = items[i, 1]; - for (int b = 0; b < num_bins; ++b) { + for (int b = 0; b < num_bins; ++b) + { x[i, b] = model.NewIntVar(0, num_copies, String.Format("x_{0}_{1}", i, b)); } } // Load variables. IntVar[] load = new IntVar[num_bins]; - for (int b = 0; b < num_bins; ++b) { + for (int b = 0; b < num_bins; ++b) + { load[b] = model.NewIntVar(0, bin_capacity, String.Format("load_{0}", b)); } // Slack variables. IntVar[] slacks = new IntVar[num_bins]; - for (int b = 0; b < num_bins; ++b) { + for (int b = 0; b < num_bins; ++b) + { slacks[b] = model.NewBoolVar(String.Format("slack_{0}", b)); } // Links load and x. int[] sizes = new int[num_items]; - for (int i = 0; i < num_items; ++i) { + for (int i = 0; i < num_items; ++i) + { sizes[i] = items[i, 0]; } - for (int b = 0; b < num_bins; ++b) { + for (int b = 0; b < num_bins; ++b) + { IntVar[] tmp = new IntVar[num_items]; - for (int i = 0; i < num_items; ++i) { + for (int i = 0; i < num_items; ++i) + { tmp[i] = x[i, b]; } model.Add(load[b] == tmp.ScalProd(sizes)); } // Place all items. - for (int i = 0; i < num_items; ++i) { + for (int i = 0; i < num_items; ++i) + { IntVar[] tmp = new IntVar[num_bins]; - for (int b = 0; b < num_bins; ++b) { + for (int b = 0; b < num_bins; ++b) + { tmp[b] = x[i, b]; } model.Add(tmp.Sum() == items[i, 1]); @@ -72,7 +83,8 @@ public class CodeSamplesSat { // Links load and slack. int safe_capacity = bin_capacity - slack_capacity; - for (int b = 0; b < num_bins; ++b) { + for (int b = 0; b < num_bins; ++b) + { // slack[b] => load[b] <= safe_capacity. model.Add(load[b] <= safe_capacity).OnlyEnforceIf(slacks[b]); // not(slack[b]) => load[b] > safe_capacity. @@ -88,26 +100,29 @@ public class CodeSamplesSat { Console.WriteLine(String.Format("Solve status: {0}", status)); if (status == CpSolverStatus.Optimal) { Console.WriteLine(String.Format("Optimal objective value: {0}", - solver.ObjectiveValue)); - for (int b = 0; b < num_bins; ++b) { + solver.ObjectiveValue)); + for (int b = 0; b < num_bins; ++b) + { Console.WriteLine(String.Format("load_{0} = {1}", - b, solver.Value(load[b]))); - for (int i = 0; i < num_items; ++i) { + b, solver.Value(load[b]))); + for (int i = 0; i < num_items; ++i) + { Console.WriteLine(string.Format(" item_{0}_{1} = {2}", - i, b, solver.Value(x[i, b]))); + i, b, solver.Value(x[i, b]))); } } } Console.WriteLine("Statistics"); Console.WriteLine(String.Format(" - conflicts : {0}", - solver.NumConflicts())); + solver.NumConflicts())); Console.WriteLine(String.Format(" - branches : {0}", - solver.NumBranches())); + solver.NumBranches())); Console.WriteLine(String.Format(" - wall time : {0} s", - solver.WallTime())); + solver.WallTime())); } - static void Main() { + static void Main() + { BinpackingProblem(); } } diff --git a/ortools/sat/samples/bool_or_sample.cs b/ortools/sat/samples/bool_or_sample.cs index f29098cfaa..4c4d7c42a2 100644 --- a/ortools/sat/samples/bool_or_sample.cs +++ b/ortools/sat/samples/bool_or_sample.cs @@ -14,15 +14,18 @@ using System; using Google.OrTools.Sat; -public class CodeSamplesSat { - static void BoolOrSample() { +public class CodeSamplesSat +{ + static void BoolOrSample() + { CpModel model = new CpModel(); IntVar x = model.NewBoolVar("x"); IntVar y = model.NewBoolVar("y"); - model.AddBoolOr(new ILiteral[] {x, y.Not()}); + model.AddBoolOr(new ILiteral[] { x, y.Not() }); } - static void Main() { + static void Main() + { BoolOrSample(); } } diff --git a/ortools/sat/samples/solve_all_solutions.cs b/ortools/sat/samples/solve_all_solutions.cs index 8e988739ed..970a8800b1 100644 --- a/ortools/sat/samples/solve_all_solutions.cs +++ b/ortools/sat/samples/solve_all_solutions.cs @@ -64,7 +64,7 @@ public class CodeSamplesSat // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = - new VarArraySolutionPrinter(new IntVar[] {x, y, z}); + new VarArraySolutionPrinter(new IntVar[] { x, y, z }); solver.SearchAllSolutions(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); diff --git a/ortools/sat/samples/solve_with_intermediate_solutions.cs b/ortools/sat/samples/solve_with_intermediate_solutions.cs index 6b16eca88d..2ffa9059d1 100644 --- a/ortools/sat/samples/solve_with_intermediate_solutions.cs +++ b/ortools/sat/samples/solve_with_intermediate_solutions.cs @@ -14,24 +14,29 @@ using System; using Google.OrTools.Sat; -public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback { - public VarArraySolutionPrinterWithObjective(IntVar[] variables) { +public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback +{ + public VarArraySolutionPrinterWithObjective(IntVar[] variables) + { variables_ = variables; } - public override void OnSolutionCallback() { + public override void OnSolutionCallback() + { Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime())); Console.WriteLine( String.Format(" objective value = {0}", ObjectiveValue())); - foreach (IntVar v in variables_) { + foreach (IntVar v in variables_) + { Console.WriteLine( String.Format(" {0} = {1}", v.ShortString(), Value(v))); } solution_count_++; } - public int SolutionCount() { + public int SolutionCount() + { return solution_count_; } @@ -39,8 +44,10 @@ public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback { private IntVar[] variables_; } -public class CodeSamplesSat { - static void MinimalCpSatPrintIntermediateSolutions() { +public class CodeSamplesSat +{ + static void MinimalCpSatPrintIntermediateSolutions() + { // Creates the model. CpModel model = new CpModel(); // Creates the variables. @@ -59,13 +66,14 @@ public class CodeSamplesSat { // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithObjective cb = - new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z}); + new VarArraySolutionPrinterWithObjective(new IntVar[] { x, y, z }); solver.SolveWithSolutionCallback(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); } - static void Main() { + static void Main() + { MinimalCpSatPrintIntermediateSolutions(); } } diff --git a/ortools/sat/samples/solve_with_time_limit.cs b/ortools/sat/samples/solve_with_time_limit.cs index e7b7c99a99..8e603c8f64 100644 --- a/ortools/sat/samples/solve_with_time_limit.cs +++ b/ortools/sat/samples/solve_with_time_limit.cs @@ -33,7 +33,7 @@ public class CodeSamplesSat CpSolver solver = new CpSolver(); // Adds a time limit. Parameters are stored as strings in the solver. - solver.StringParameters = "max_time_in_seconds:10.0" ; + solver.StringParameters = "max_time_in_seconds:10.0"; CpSolverStatus status = solver.Solve(model); diff --git a/ortools/sat/samples/stop_after_n_solutions.cs b/ortools/sat/samples/stop_after_n_solutions.cs index b71e41ebc8..5bae38fe90 100644 --- a/ortools/sat/samples/stop_after_n_solutions.cs +++ b/ortools/sat/samples/stop_after_n_solutions.cs @@ -15,22 +15,27 @@ using System; using Google.OrTools.Sat; -public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback { +public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback +{ public VarArraySolutionPrinterWithLimit(IntVar[] variables, - int solution_limit) { + int solution_limit) + { variables_ = variables; solution_limit_ = solution_limit; } - public override void OnSolutionCallback() { + public override void OnSolutionCallback() + { Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime())); - foreach (IntVar v in variables_) { + foreach (IntVar v in variables_) + { Console.WriteLine( String.Format(" {0} = {1}", v.ShortString(), Value(v))); } solution_count_++; - if (solution_count_ >= solution_limit_) { + if (solution_count_ >= solution_limit_) + { Console.WriteLine( String.Format("Stopping search after {0} solutions", solution_limit_)); @@ -38,7 +43,8 @@ public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback { } } - public int SolutionCount() { + public int SolutionCount() + { return solution_count_; } @@ -47,8 +53,10 @@ public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback { private int solution_limit_; } -public class CodeSamplesSat { - static void StopAfterNSolutions() { +public class CodeSamplesSat +{ + static void StopAfterNSolutions() + { // Creates the model. CpModel model = new CpModel(); // Creates the variables. @@ -61,13 +69,14 @@ public class CodeSamplesSat { // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinterWithLimit cb = - new VarArraySolutionPrinterWithLimit(new IntVar[] {x, y, z}, 5); + new VarArraySolutionPrinterWithLimit(new IntVar[] { x, y, z }, 5); solver.SearchAllSolutions(model, cb); Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount())); } - static void Main() { + static void Main() + { StopAfterNSolutions(); } }