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

small changes in SAT internals

Browse Source
This commit is contained in:
Laurent Perron
2018-04-17 13:00:25 +02:00
parent b878cad661
commit ebee158577
3 changed files with 44 additions and 27 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
ortools/sat/precedences.cc
View File

@@ -725,6 +725,7 @@ void PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(
const int old_level = solver->CurrentDecisionLevel();
solver->EnqueueDecisionAndBacktrackOnConflict(literal.Negated());
if (solver->IsModelUnsat()) return;
const int new_level = solver->CurrentDecisionLevel();
if (new_level <= old_level) {
clause = solver->GetLastIncompatibleDecisions();
@@ -756,7 +757,7 @@ void PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(
selectors.push_back(Literal(arcs_[a].presence_literals.front()));
}
model->Add(GreaterThanAtLeastOneOf(target, vars, offsets, selectors));
solver->Propagate();
if (!solver->FinishPropagation()) return;
}
}

62
ortools/sat/sat_solver.cc
View File

@@ -1005,7 +1005,14 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
moved_last.insert(candidate.back().Index());
}
// Returns if we don't have any minimization.
Backtrack(0);
if (candidate.size() == clause->Size()) return;
// Write the new clause to the proof before the deletion of the old one
// happens (when we will detach it).
if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate);
if (candidate.size() == 1) {
if (!Assignment().VariableIsAssigned(candidate[0].Variable())) {
counters_.minimization_num_removed_literals += clause->Size();
@@ -1018,21 +1025,17 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
counters_.minimization_num_removed_literals += clause->Size() - 2;
AddBinaryClauseInternal(candidate[0], candidate[1]);
clauses_propagator_.Detach(clause);
if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate);
return;
}
if (candidate.size() < clause->Size()) {
counters_.minimization_num_removed_literals +=
clause->Size() - candidate.size();
counters_.minimization_num_removed_literals +=
clause->Size() - candidate.size();
// TODO(user): If the watched literal didn't change, we could just rewrite
// the clause while keeping the two watched literals at the beginning.
clauses_propagator_.Detach(clause);
clause->Rewrite(candidate);
clauses_propagator_.Attach(clause, trail_);
if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate);
}
// TODO(user): If the watched literal didn't change, we could just rewrite
// the clause while keeping the two watched literals at the beginning.
clauses_propagator_.Detach(clause);
clause->Rewrite(candidate);
clauses_propagator_.Attach(clause, trail_);
}
SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) {
@@ -1471,6 +1474,17 @@ void SatSolver::ProcessNewlyFixedVariables() {
int num_detached_clauses = 0;
int num_binary = 0;
if (drat_writer_ != nullptr) {
// We need to output the literals that are fixed so we can remove all
// clauses that contains them. Note that this doesn't seems to be needed
// for drat-trim.
Literal temp;
for (int i = num_processed_fixed_variables_; i < trail_->Index(); ++i) {
temp = (*trail_)[i];
drat_writer_->AddClause({&temp, 1});
}
}
// We remove the clauses that are always true and the fixed literals from the
// others. Note that none of the clause should be all false because we should
// have detected a conflict before this is called.
@@ -1483,26 +1497,26 @@ void SatSolver::ProcessNewlyFixedVariables() {
clauses_propagator_.LazyDetach(clause);
++num_detached_clauses;
continue;
} else if (clause->Size() != old_size) {
if (clause->Size() == 2 &&
parameters_->treat_binary_clauses_separately()) {
// This clause is now a binary clause, treat it separately. Note that
// it is safe to do that because this clause can't be used as a reason
// since we are at level zero and the clause is not satisfied.
AddBinaryClauseInternal(clause->FirstLiteral(),
clause->SecondLiteral());
clauses_propagator_.LazyDetach(clause);
++num_binary;
continue;
}
}
const size_t new_size = clause->Size();
if (new_size != old_size && drat_writer_ != nullptr) {
if (new_size == old_size) continue;
if (drat_writer_ != nullptr) {
CHECK_GT(new_size, 0);
drat_writer_->AddClause({clause->begin(), new_size});
drat_writer_->DeleteClause({clause->begin(), old_size});
}
if (new_size == 2 && parameters_->treat_binary_clauses_separately()) {
// This clause is now a binary clause, treat it separately. Note that
// it is safe to do that because this clause can't be used as a reason
// since we are at level zero and the clause is not satisfied.
AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral());
clauses_propagator_.LazyDetach(clause);
++num_binary;
continue;
}
}
// Note that we will only delete the clauses during the next database cleanup.

6
ortools/sat/simplification.cc
View File

@@ -161,13 +161,15 @@ void SatPresolver::AddClause(absl::Span<Literal> clause) {
in_clause_to_process_.push_back(true);
clause_to_process_.push_back(ci);
bool changed = false;
std::vector<Literal>& clause_ref = clauses_.back();
if (!equiv_mapping_.empty()) {
for (int i = 0; i < clause_ref.size(); ++i) {
const Literal old_literal = clause_ref[i];
clause_ref[i] = Literal(equiv_mapping_[clause_ref[i].Index()]);
if (old_literal != clause_ref[i]) changed = true;
}
}
const int old_size = clause_ref.size();
std::sort(clause_ref.begin(), clause_ref.end());
clause_ref.erase(std::unique(clause_ref.begin(), clause_ref.end()),
clause_ref.end());
@@ -184,7 +186,7 @@ void SatPresolver::AddClause(absl::Span<Literal> clause) {
}
}
if (drat_writer_ != nullptr && clause_ref.size() < old_size) {
if (drat_writer_ != nullptr && changed) {
drat_writer_->AddClause(clause_ref);
drat_writer_->DeleteClause(clause);
}