Skip to content

Commit 800e1f6

Browse files
lperronlperron
committed
[CP-SAT] fix scheduling bugs: wrong explanations; unsafe heuristics; more work on lrat; switch max_hs to use CP-SAT as MIP solver; other bugfixes
1 parent 3d301d9 commit 800e1f6

4 files changed

Lines changed: 558 additions & 0 deletions

File tree

‎ortools/sat/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ list(REMOVE_ITEM _SRCS
1818
${CMAKE_CURRENT_SOURCE_DIR}/opb_reader.h
1919
${CMAKE_CURRENT_SOURCE_DIR}/sat_cnf_reader.h
2020
${CMAKE_CURRENT_SOURCE_DIR}/sat_runner.cc
21+
${CMAKE_CURRENT_SOURCE_DIR}/lrat_checker_main.cc
2122
)
2223
set(NAME ${PROJECT_NAME}_sat)
2324

‎ortools/sat/debug_solution.cc‎

Lines changed: 229 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,229 @@
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+
14+
#include "ortools/sat/debug_solution.h"
15+
16+
#include <tuple>
17+
#include <vector>
18+
19+
#include "absl/algorithm/container.h"
20+
#include "absl/log/check.h"
21+
#include "absl/log/log.h"
22+
#include "absl/numeric/int128.h"
23+
#include "absl/types/span.h"
24+
#include "ortools/sat/cp_model_checker.h"
25+
#include "ortools/sat/integer_base.h"
26+
#include "ortools/sat/linear_constraint.h"
27+
#include "ortools/sat/sat_base.h"
28+
#include "ortools/util/logging.h"
29+
30+
namespace operations_research {
31+
namespace sat {
32+
33+
void DebugSolution::SynchronizeWithShared(const CpModelProto& model_proto) {
34+
if (shared_response_->DebugSolution().empty()) return;
35+
36+
if (!SolutionIsFeasible(model_proto, shared_response_->DebugSolution())) {
37+
// TODO(user): we should probably CHECK-fail.
38+
SOLVER_LOG(logger_, "Debug solution is not feasible.");
39+
return;
40+
}
41+
SOLVER_LOG(logger_, "Debug solution is feasible.");
42+
43+
// Copy the proto values.
44+
proto_values_ = shared_response_->DebugSolution();
45+
46+
// Fill the values by integer variable.
47+
const int num_integers = integer_trail_->NumIntegerVariables().value();
48+
ivar_has_value_.assign(num_integers, false);
49+
ivar_values_.assign(num_integers, 0);
50+
boolean_solution_.clear();
51+
52+
for (int i = 0; i < proto_values_.size(); ++i) {
53+
if (mapping_->IsBoolean(i)) {
54+
Literal l = mapping_->Literal(i);
55+
if (proto_values_[i] == 0) {
56+
l = l.Negated();
57+
}
58+
boolean_solution_.push_back(l);
59+
}
60+
61+
if (!mapping_->IsInteger(i)) continue;
62+
const IntegerVariable var = mapping_->Integer(i);
63+
ivar_has_value_[var] = true;
64+
ivar_has_value_[NegationOf(var)] = true;
65+
ivar_values_[var] = proto_values_[i];
66+
ivar_values_[NegationOf(var)] = -proto_values_[i];
67+
}
68+
69+
// Also add the trivial literal that is sometimes created by the loader
70+
if (trivial_literals_->TrueLiteral().Variable().value() ==
71+
proto_values_.size()) {
72+
boolean_solution_.push_back(trivial_literals_->TrueLiteral());
73+
}
74+
75+
// The objective variable is usually not part of the proto, but it is still
76+
// nice to have it, so we recompute it here.
77+
if (objective_def_ != nullptr &&
78+
objective_def_->objective_var != kNoIntegerVariable) {
79+
if (absl::c_all_of(objective_def_->vars, [this](IntegerVariable var) {
80+
return var < ivar_has_value_.end_index() && ivar_has_value_[var];
81+
})) {
82+
const IntegerVariable objective_var = objective_def_->objective_var;
83+
if (objective_var + 1 >= ivar_has_value_.size()) {
84+
ivar_has_value_.resize(objective_var + 2, false);
85+
ivar_values_.resize(objective_var + 2, 0);
86+
}
87+
IntegerValue objective_value = 0;
88+
for (int i = 0; i < objective_def_->vars.size(); ++i) {
89+
objective_value +=
90+
objective_def_->coeffs[i] * ivar_values_[objective_def_->vars[i]];
91+
}
92+
SOLVER_LOG(
93+
logger_,
94+
absl::StrCat("Debug solution objective value: ",
95+
objective_def_->ScaleIntegerObjective(objective_value)));
96+
ivar_has_value_[objective_var] = true;
97+
ivar_has_value_[NegationOf(objective_var)] = true;
98+
ivar_values_[objective_var] = objective_value;
99+
ivar_values_[NegationOf(objective_var)] = -objective_value;
100+
inner_objective_value_ = objective_value;
101+
}
102+
}
103+
}
104+
105+
bool DebugSolution::CheckClause(
106+
absl::Span<const Literal> clause,
107+
absl::Span<const IntegerLiteral> integers) const {
108+
if (IsLookingForSolutionBetterThanDebugSolution()) return true;
109+
if (proto_values_.empty()) return true;
110+
111+
bool is_satisfied = false;
112+
std::vector<std::tuple<Literal, IntegerLiteral, IntegerValue>> to_print;
113+
for (const Literal l : clause) {
114+
// First case, this Boolean is mapped.
115+
{
116+
const int proto_var =
117+
mapping_->GetProtoVariableFromBooleanVariable(l.Variable());
118+
if (proto_var != -1) {
119+
CHECK_LT(proto_var, proto_values_.size());
120+
to_print.push_back({l, IntegerLiteral(), proto_values_[proto_var]});
121+
if (proto_values_[proto_var] == (l.IsPositive() ? 1 : 0)) {
122+
is_satisfied = true;
123+
break;
124+
}
125+
continue;
126+
}
127+
}
128+
129+
// Second case, it is associated to IntVar >= value.
130+
// We can use any of them, so if one is false, we use this one.
131+
bool all_true = true;
132+
for (const IntegerLiteral associated : encoder_->GetIntegerLiterals(l)) {
133+
if (associated.var >= ivar_has_value_.end_index() ||
134+
!ivar_has_value_[associated.var]) {
135+
continue;
136+
}
137+
const IntegerValue value = ivar_values_[associated.var];
138+
to_print.push_back({l, associated, value});
139+
140+
if (value < associated.bound) {
141+
all_true = false;
142+
break;
143+
}
144+
}
145+
if (all_true) {
146+
is_satisfied = true;
147+
break;
148+
}
149+
}
150+
for (const IntegerLiteral i_lit : integers) {
151+
DCHECK(!i_lit.IsAlwaysFalse());
152+
if (i_lit.IsAlwaysTrue()) continue;
153+
if (i_lit.var >= ivar_has_value_.end_index() ||
154+
!ivar_has_value_[i_lit.var]) {
155+
is_satisfied = true;
156+
break;
157+
}
158+
159+
const IntegerValue value = ivar_values_[i_lit.var];
160+
to_print.push_back({Literal(kNoLiteralIndex), i_lit, value});
161+
162+
// This is a bit confusing, but since the i_lit in the reason are
163+
// not "negated", we need at least one to be FALSE, for the reason to
164+
// be valid.
165+
if (value < i_lit.bound) {
166+
is_satisfied = true;
167+
break;
168+
}
169+
}
170+
if (!is_satisfied) {
171+
LOG(INFO) << "Reason clause is not satisfied by loaded solution:";
172+
LOG(INFO) << "Worker '" << name_
173+
<< "', level=" << sat_solver_->CurrentDecisionLevel();
174+
LOG(INFO) << "literals (neg): " << clause;
175+
LOG(INFO) << "integer literals: " << integers;
176+
for (const auto [l, i_lit, solution_value] : to_print) {
177+
if (i_lit.IsAlwaysTrue()) {
178+
const int proto_var =
179+
mapping_->GetProtoVariableFromBooleanVariable(l.Variable());
180+
LOG(INFO) << l << " (bool in model) proto_var=" << proto_var
181+
<< " value_in_sol=" << solution_value;
182+
} else {
183+
const int proto_var = mapping_->GetProtoVariableFromIntegerVariable(
184+
PositiveVariable(i_lit.var));
185+
LOG(INFO) << l << " " << i_lit << " proto_var="
186+
<< (proto_var == -1 ? "none" : absl::StrCat(proto_var))
187+
<< " value_in_sol="
188+
<< (VariableIsPositive(i_lit.var) ? solution_value
189+
: -solution_value);
190+
}
191+
}
192+
}
193+
return is_satisfied;
194+
}
195+
196+
bool DebugSolution::CheckCut(const LinearConstraint& cut,
197+
bool only_check_ub) const {
198+
if (IsLookingForSolutionBetterThanDebugSolution()) return true;
199+
if (proto_values_.empty()) return true;
200+
absl::int128 activity(0);
201+
for (int i = 0; i < cut.num_terms; ++i) {
202+
const IntegerVariable var = cut.vars[i];
203+
const IntegerValue coeff = cut.coeffs[i];
204+
if (var >= ivar_has_value_.size() || !ivar_has_value_[var]) {
205+
return true;
206+
}
207+
activity += absl::int128(coeff.value()) * ivar_values_[var].value();
208+
}
209+
if (only_check_ub) {
210+
if (activity > cut.ub.value()) {
211+
LOG(INFO) << cut.DebugString();
212+
LOG(INFO) << "activity " << activity << " > " << cut.ub;
213+
LOG(INFO) << "Cut is not satisfied by loaded solution.";
214+
return false;
215+
}
216+
} else {
217+
if (activity > cut.ub.value() || activity < cut.lb.value()) {
218+
LOG(INFO) << cut.DebugString();
219+
LOG(INFO) << "activity " << activity << " not in [" << cut.lb << ","
220+
<< cut.ub << "]";
221+
LOG(INFO) << "Cut is not satisfied by loaded solution.";
222+
return false;
223+
}
224+
}
225+
return true;
226+
}
227+
228+
} // namespace sat
229+
} // namespace operations_research

‎ortools/sat/debug_solution.h‎

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
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+
14+
#ifndef ORTOOLS_SAT_DEBUG_SOLUTION_H_
15+
#define ORTOOLS_SAT_DEBUG_SOLUTION_H_
16+
17+
#include <cstdint>
18+
#include <string>
19+
#include <vector>
20+
21+
#include "absl/types/span.h"
22+
#include "ortools/base/strong_vector.h"
23+
#include "ortools/sat/cp_model_mapping.h"
24+
#include "ortools/sat/integer.h"
25+
#include "ortools/sat/integer_base.h"
26+
#include "ortools/sat/linear_constraint.h"
27+
#include "ortools/sat/model.h"
28+
#include "ortools/sat/sat_base.h"
29+
#include "ortools/sat/sat_solver.h"
30+
#include "ortools/sat/synchronization.h"
31+
#include "ortools/util/logging.h"
32+
33+
namespace operations_research {
34+
namespace sat {
35+
36+
// A model singleton used for debugging. If this is set in the model, then we
37+
// can check that various derived constraint do not exclude this solution (if
38+
// it is a known optimal solution for instance).
39+
class DebugSolution {
40+
public:
41+
explicit DebugSolution(Model* model)
42+
: shared_response_(model->GetOrCreate<SharedResponseManager>()),
43+
logger_(model->GetOrCreate<SolverLogger>()),
44+
integer_trail_(model->GetOrCreate<IntegerTrail>()),
45+
mapping_(model->GetOrCreate<CpModelMapping>()),
46+
trivial_literals_(model->GetOrCreate<TrivialLiterals>()),
47+
sat_solver_(model->GetOrCreate<SatSolver>()),
48+
objective_def_(model->GetOrCreate<ObjectiveDefinition>()),
49+
encoder_(model->GetOrCreate<IntegerEncoder>()),
50+
name_(model->Name()) {}
51+
52+
void SynchronizeWithShared(const CpModelProto& model_proto);
53+
54+
const std::vector<Literal>& boolean_solution() const {
55+
return boolean_solution_;
56+
}
57+
58+
bool IsBooleanSolution() const {
59+
if (boolean_solution_.empty()) return false;
60+
if (inner_objective_value_ != kMinIntegerValue) {
61+
return false;
62+
}
63+
return boolean_solution_.size() == proto_values_.size();
64+
}
65+
66+
bool CheckClause(absl::Span<const Literal> clause,
67+
absl::Span<const IntegerLiteral> integers) const;
68+
69+
bool CheckCut(const LinearConstraint& cut, bool only_check_ub) const;
70+
71+
const util_intops::StrongVector<IntegerVariable, IntegerValue>&
72+
IntegerVariableValues() const {
73+
return ivar_values_;
74+
}
75+
76+
private:
77+
SharedResponseManager* shared_response_;
78+
SolverLogger* logger_;
79+
IntegerTrail* integer_trail_;
80+
CpModelMapping* mapping_;
81+
TrivialLiterals* trivial_literals_;
82+
SatSolver* sat_solver_;
83+
ObjectiveDefinition* objective_def_;
84+
IntegerEncoder* encoder_;
85+
std::string name_;
86+
87+
bool IsLookingForSolutionBetterThanDebugSolution() const {
88+
if (inner_objective_value_ == kMinIntegerValue) return false;
89+
if (shared_response_->BestSolutionInnerObjectiveValue() <=
90+
inner_objective_value_) {
91+
return true;
92+
}
93+
return false;
94+
}
95+
96+
// This is filled from proto_values at load-time, and using the
97+
// cp_model_mapping, we cache the solution of the integer variables that are
98+
// mapped. Note that it is possible that not all integer variable are
99+
// mapped.
100+
//
101+
// TODO(user): When this happen we should be able to infer the value of
102+
// these derived variable in the solution. For now, we only do that for the
103+
// objective variable.
104+
util_intops::StrongVector<IntegerVariable, bool> ivar_has_value_;
105+
util_intops::StrongVector<IntegerVariable, IntegerValue> ivar_values_;
106+
107+
std::vector<Literal> boolean_solution_;
108+
109+
// This is the value of all proto variables.
110+
// It should be of the same size of the PRESOLVED model and should
111+
// correspond to a solution to the presolved model.
112+
std::vector<int64_t> proto_values_;
113+
114+
IntegerValue inner_objective_value_ = kMinIntegerValue;
115+
};
116+
117+
} // namespace sat
118+
} // namespace operations_research
119+
120+
#endif // ORTOOLS_SAT_DEBUG_SOLUTION_H_

0 commit comments

Comments
 (0)