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

fix bug in sat with non-monotonic propagators (aka LP)

Browse Source
This commit is contained in:
Laurent Perron
2017-11-23 13:19:22 +01:00
parent a8a9536977
commit b49dc2a2ad
2 changed files with 28 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
ortools/sat/precedences.cc
View File

@@ -757,6 +757,7 @@ void PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(
selectors.push_back(Literal(arcs_[a].presence_l));
}
model->Add(GreaterThanAtLeastOneOf(target, vars, offsets, selectors));
solver->Propagate();
}
}

30
ortools/sat/sat_solver.cc
View File

@@ -789,7 +789,12 @@ SatSolver::Status SatSolver::ReapplyDecisionsUpTo(
DCHECK_GE(decision_index, current_decision_level_);
const Literal previous_decision = decisions_[decision_index].literal;
++decision_index;
if (Assignment().LiteralIsTrue(previous_decision)) continue;
if (Assignment().LiteralIsTrue(previous_decision)) {
// Note that this particular position in decisions_ will be overridden,
// but that is fine since this is a consequence of the previous decision,
// so we will never need to take it into account again.
continue;
}
if (Assignment().LiteralIsFalse(previous_decision)) {
// Update decision so that GetLastIncompatibleDecisions() works.
decisions_[current_decision_level_].literal = previous_decision;
@@ -1131,9 +1136,28 @@ SatSolver::Status SatSolver::SolveWithTimeLimit(TimeLimit* time_limit) {
std::vector<Literal> SatSolver::GetLastIncompatibleDecisions() {
SCOPED_TIME_STAT(&stats_);
std::vector<Literal> unsat_assumptions;
const Literal false_assumption = decisions_[CurrentDecisionLevel()].literal;
DCHECK(trail_->Assignment().LiteralIsFalse(false_assumption));
std::vector<Literal> unsat_assumptions;
if (!trail_->Assignment().LiteralIsFalse(false_assumption)) {
// This can only happen in some corner cases where: we enqueued
// false_assumption, it leads to a conflict, but after re-enqueing the
// decisions that were backjumped over, there is no conflict anymore. This
// can only happen in the presence of propagators that are non-monotonic
// and do not propagate the same thing when there is more literal on the
// trail.
//
// In this case, we simply return all the decisions since we know that is
// a valid conflict. Since this should be rare, it is okay to not "minimize"
// what we return like we do below.
//
// TODO(user): unit-test this case with a mock propagator.
unsat_assumptions.reserve(CurrentDecisionLevel());
for (int i = 0; i < CurrentDecisionLevel(); ++i) {
unsat_assumptions.push_back(decisions_[i].literal);
}
return unsat_assumptions;
}
unsat_assumptions.push_back(false_assumption);
// This will be used to mark all the literals inspected while we process the