DotNet Reference

.Net Reference

CpSolver.cs
Go to the documentation of this file.
1 // Copyright 2010-2018 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 
14 using System;
15 using System.Collections.Generic;
16 
17 namespace Google.OrTools.Sat
18 {
19  public class CpSolver
20  {
21  public CpSolverStatus Solve(CpModel model)
22  {
23  if (string_parameters_ != null)
24  {
25  response_ = SatHelper.SolveWithStringParameters(model.Model, string_parameters_);
26  }
27  else
28  {
29  response_ = SatHelper.Solve(model.Model);
30  }
31  return response_.Status;
32  }
33 
34  public CpSolverStatus SolveWithSolutionCallback(CpModel model, SolutionCallback cb)
35  {
36  if (string_parameters_ != null)
37  {
38  response_ = SatHelper.SolveWithStringParametersAndSolutionCallback(model.Model, string_parameters_, cb);
39  }
40  else
41  {
42  response_ = SatHelper.SolveWithStringParametersAndSolutionCallback(model.Model, "", cb);
43  }
44  return response_.Status;
45  }
46 
47  public CpSolverStatus SearchAllSolutions(CpModel model, SolutionCallback cb)
48  {
49  if (string_parameters_ != null)
50  {
51  string extra_parameters = " enumerate_all_solutions:true";
52  response_ = SatHelper.SolveWithStringParametersAndSolutionCallback(
53  model.Model, string_parameters_ + extra_parameters, cb);
54  }
55  else
56  {
57  string parameters = "enumerate_all_solutions:true";
58  response_ = SatHelper.SolveWithStringParametersAndSolutionCallback(model.Model, parameters, cb);
59  }
60  return response_.Status;
61  }
62 
63  public String ResponseStats()
64  {
65  return SatHelper.SolverResponseStats(response_);
66  }
67 
68  public double ObjectiveValue
69  {
70  get {
71  return response_.ObjectiveValue;
72  }
73  }
74 
75  public double BestObjectiveBound
76  {
77  get {
78  return response_.BestObjectiveBound;
79  }
80  }
81 
82  public string StringParameters
83  {
84  get {
85  return string_parameters_;
86  }
87  set {
88  string_parameters_ = value;
89  }
90  }
91 
92  public CpSolverResponse Response
93  {
94  get {
95  return response_;
96  }
97  }
98 
99  public long Value(LinearExpr e)
100  {
101  List<LinearExpr> exprs = new List<LinearExpr>();
102  List<long> coeffs = new List<long>();
103  exprs.Add(e);
104  coeffs.Add(1L);
105  long constant = 0;
106 
107  while (exprs.Count > 0)
108  {
109  LinearExpr expr = exprs[0];
110  exprs.RemoveAt(0);
111  long coeff = coeffs[0];
112  coeffs.RemoveAt(0);
113  if (coeff == 0)
114  continue;
115 
116  if (expr is ProductCst)
117  {
118  ProductCst p = (ProductCst)expr;
119  if (p.Coeff != 0)
120  {
121  exprs.Add(p.Expr);
122  coeffs.Add(p.Coeff * coeff);
123  }
124  }
125  else if (expr is SumArray)
126  {
127  SumArray a = (SumArray)expr;
128  constant += coeff * a.Constant;
129  foreach (LinearExpr sub in a.Expressions)
130  {
131  exprs.Add(sub);
132  coeffs.Add(coeff);
133  }
134  }
135  else if (expr is IntVar)
136  {
137  int index = expr.Index;
138  long value = index >= 0 ? response_.Solution[index] : -response_.Solution[-index - 1];
139  constant += coeff * value;
140  }
141  else if (expr is NotBooleanVariable)
142  {
143  throw new ArgumentException("Cannot evaluate a literal in an integer expression.");
144  }
145  else
146  {
147  throw new ArgumentException("Cannot evaluate '" + expr.ToString() + "' in an integer expression");
148  }
149  }
150  return constant;
151  }
152 
153  public Boolean BooleanValue(ILiteral literal)
154  {
155  if (literal is IntVar || literal is NotBooleanVariable)
156  {
157  int index = literal.GetIndex();
158  if (index >= 0)
159  {
160  return response_.Solution[index] != 0;
161  }
162  else
163  {
164  return response_.Solution[-index - 1] == 0;
165  }
166  }
167  else
168  {
169  throw new ArgumentException("Cannot evaluate '" + literal.ToString() + "' as a boolean literal");
170  }
171  }
172 
173  public long NumBranches()
174  {
175  return response_.NumBranches;
176  }
177 
178  public long NumConflicts()
179  {
180  return response_.NumConflicts;
181  }
182 
183  public double WallTime()
184  {
185  return response_.WallTime;
186  }
187 
189  {
190  return response_.SufficientAssumptionsForInfeasibility;
191  }
192 
193  private CpModelProto model_;
194  private CpSolverResponse response_;
195  string string_parameters_;
196  }
197 
198 } // namespace Google.OrTools.Sat
using System
Definition: Program.cs:14
Wrapper class around the cp_model proto.
Definition: CpModel.cs:24
CpModelProto Model
Definition: CpModel.cs:34
IList< int > SufficientAssumptionsForInfeasibility()
Definition: CpSolver.cs:188
CpSolverStatus SolveWithSolutionCallback(CpModel model, SolutionCallback cb)
Definition: CpSolver.cs:34
long Value(LinearExpr e)
Definition: CpSolver.cs:99
CpSolverStatus SearchAllSolutions(CpModel model, SolutionCallback cb)
Definition: CpSolver.cs:47
CpSolverStatus Solve(CpModel model)
Definition: CpSolver.cs:21
CpSolverResponse Response
Definition: CpSolver.cs:93
Boolean BooleanValue(ILiteral literal)
Definition: CpSolver.cs:153