always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix UMR in assumptions

Browse Source
This commit is contained in:
Laurent Perron
2020-08-18 17:21:51 +02:00
parent b7a370c4fd
commit 95035186c3
1 changed files with 9 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
ortools/sat/sat_solver.cc
View File

@@ -534,8 +534,15 @@ bool SatSolver::ResetToLevelZero() {
bool SatSolver::ResetWithGivenAssumptions(
const std::vector<Literal>& assumptions) {
if (!ResetToLevelZero()) return false;
assumption_level_ = assumptions.size();
for (int i = 0; i < assumptions.size(); ++i) {
// Assuming there is no duplicate in assumptions, but they can be a literal
// and its negation (weird corner case), there will always be a conflict if we
// enqueue stricly more assumptions than the number of variables, so there is
// no point considering the end of the list. Note that there is no overflow
// since decisions_.size() == num_variables_ + 1;
assumption_level_ =
std::min<int>(assumptions.size(), num_variables_.value() + 1);
for (int i = 0; i < assumption_level_; ++i) {
decisions_[i].literal = assumptions[i];
}
return ReapplyAssumptionsIfNeeded();