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

[CP-SAT] work on lrat, clause congruence, inprocess ; bug fixes

Browse Source
This commit is contained in:
Laurent Perron
2025-12-23 18:11:58 +01:00
committed by Corentin Le Molgat
parent 9190a5d819
commit 0782d13065
14 changed files with 883 additions and 231 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
ortools/sat/BUILD.bazel
View File

@@ -1638,6 +1638,7 @@ cc_library(
"//ortools/util:sorted_interval_list",
"//ortools/util:strong_integers",
"//ortools/util:time_limit",
"@abseil-cpp//absl/algorithm:container",
"@abseil-cpp//absl/cleanup",
"@abseil-cpp//absl/container:btree",
"@abseil-cpp//absl/container:flat_hash_map",

22
ortools/sat/clause.cc
View File

@@ -125,7 +125,6 @@ ClauseManager::~ClauseManager() {
}
void ClauseManager::Resize(int num_variables) {
DCHECK(is_clean_);
watchers_on_false_.resize(num_variables << 1);
reasons_.resize(num_variables);
needs_cleaning_.Resize(LiteralIndex(num_variables << 1));
@@ -980,8 +979,29 @@ bool BinaryImplicationGraph::AddBinaryClauseInternal(
trail_->ChangeReason(trail_index, propagator_id_);
}
// Deal with literal fixing and do not even add a binary clause in that case.
if (rep_a == rep_b) {
return FixLiteral(rep_a, {rep_id});
} else if (trail_->CurrentDecisionLevel() == 0) {
const auto& assignment = trail_->Assignment();
// TODO(user): just make GetUnitClauseId() work all the time? for that
// we need to make sure all level zero are pushed with kUnitReason.
if (lrat_proof_handler_ != nullptr) {
if (assignment.LiteralIsFalse(rep_a)) {
return FixLiteral(rep_b,
{rep_id, trail_->GetUnitClauseId(rep_a.Variable())});
} else if (assignment.LiteralIsFalse(rep_b)) {
return FixLiteral(rep_a,
{rep_id, trail_->GetUnitClauseId(rep_b.Variable())});
}
} else {
if (assignment.LiteralIsFalse(rep_a)) {
return FixLiteral(rep_b, {});
} else if (assignment.LiteralIsFalse(rep_b)) {
return FixLiteral(rep_a, {});
}
}
}
a = rep_a;

13
ortools/sat/cp_model_checker.cc
View File

@@ -284,15 +284,6 @@ std::string ValidateLinearExpression(const CpModelProto& model,
return "";
}
std::string ValidateConstantExpression(const CpModelProto& model,
const LinearExpressionProto& expr) {
if (!expr.vars().empty()) {
return absl::StrCat("expression must be constant: ",
ProtobufShortDebugString(expr));
}
return ValidateLinearExpression(model, expr);
}
std::string ValidateLinearConstraint(const CpModelProto& model,
const ConstraintProto& ct) {
if (!DomainInProtoIsValid(ct.linear())) {
@@ -1376,8 +1367,8 @@ class ConstraintChecker {
bool LinearConstraintIsFeasible(const ConstraintProto& ct) {
int64_t sum = 0;
const int num_variables = ct.linear().coeffs_size();
const int* const vars = ct.linear().vars().data();
const int64_t* const coeffs = ct.linear().coeffs().data();
absl::Span<const int> vars = absl::MakeSpan(ct.linear().vars());
absl::Span<const int64_t> coeffs = absl::MakeSpan(ct.linear().coeffs());
for (int i = 0; i < num_variables; ++i) {
// We know we only have positive reference now.
DCHECK(RefIsPositive(vars[i]));

6
ortools/sat/cp_model_solver.cc
View File

@@ -2529,6 +2529,12 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
}
#endif // ORTOOLS_TARGET_OS_SUPPORTS_THREADS
if (DEBUG_MODE) {
LOG(WARNING)
<< "WARNING: CP-SAT is running in debug mode. The solver will "
"be slow because we will do a lot of extra checks. Compile in "
"optimization mode to gain an order of magnitude speedup.";
}
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, "Starting ", CpSatSolverVersion());
SOLVER_LOG(logger, "Parameters: ", ProtobufShortDebugString(params));

5
ortools/sat/csharp/CpSolver.cs
View File

@@ -210,7 +210,8 @@ public class CpSolver : IDisposable
/// <summary>
/// Releases unmanaged resources and optionally releases managed resources.
/// </summary>
/// <param name="disposing">true to release both managed and unmanaged resources; false to release only unmanaged resources.</param>
/// <param name="disposing">true to release both managed and unmanaged resources; false to release only unmanaged
/// resources.</param>
protected virtual void Dispose(bool disposing)
{
if (_disposed)
@@ -270,4 +271,4 @@ class BestBoundCallbackDelegate : BestBoundCallback
public override void NewBestBound(double bound) => _delegate(bound);
}
} // namespace Google.OrTools.Sat
} // namespace Google.OrTools.Sat

22
ortools/sat/gate_utils.h
View File

@@ -98,6 +98,28 @@ inline int AddHoleAtPosition(int i, int bitset) {
return (bitset & ((1 << i) - 1)) + ((bitset >> i) << (i + 1));
}
inline int RemoveFixedInput(int i, bool at_true,
absl::Span<LiteralIndex> inputs,
int& int_function_values) {
DCHECK_LT(i, inputs.size());
const int value = at_true ? 1 : 0;
// Re-compute the bitset.
SmallBitset values = int_function_values;
SmallBitset new_truth_table = 0;
const int new_size = inputs.size() - 1;
for (int p = 0; p < (1 << new_size); ++p) {
const int extended_p = AddHoleAtPosition(i, p) | (value << i);
new_truth_table |= ((values >> extended_p) & 1) << p;
}
int_function_values = new_truth_table;
for (int j = i + 1; j < inputs.size(); ++j) {
inputs[j - 1] = inputs[j];
}
return new_size;
}
// The function is target = function_values[inputs as bit position].
//
// TODO(user): This can be optimized with more bit twiddling if needed.

41
ortools/sat/gate_utils_test.cc
View File

@@ -75,6 +75,47 @@ TEST(AddHoleAtPositionTest, BasicTest) {
EXPECT_EQ(AddHoleAtPosition(8, 0xFF), 0b011111111);
}
TEST(CanonicalizeFunctionTruthTableTest, AndGateWithXAndNotX) {
LiteralIndex output = Literal(+1).Index();
std::vector<LiteralIndex> inputs{Literal(+2).Index(), Literal(-2).Index()};
int table = 0b1000;
const int new_size =
CanonicalizeFunctionTruthTable(output, absl::MakeSpan(inputs), table);
CHECK_EQ(new_size, 0); // Fixed to zero.
}
TEST(RemoveFixedInputTest, BasicTest1) {
std::vector<LiteralIndex> inputs{Literal(+1).Index(), Literal(+2).Index(),
Literal(+3).Index()};
int table = 0b01011010;
const int new_size = RemoveFixedInput(1, true, absl::MakeSpan(inputs), table);
EXPECT_EQ(new_size, 2);
EXPECT_EQ(inputs[0], Literal(+1).Index());
EXPECT_EQ(inputs[1], Literal(+3).Index());
EXPECT_EQ(table, 0b0110) << std::bitset<4>(table);
}
TEST(RemoveFixedInputTest, BasicTest2) {
std::vector<LiteralIndex> inputs{Literal(+1).Index(), Literal(+2).Index(),
Literal(+3).Index()};
int table = 0b01011010;
const int new_size =
RemoveFixedInput(1, false, absl::MakeSpan(inputs), table);
EXPECT_EQ(new_size, 2);
EXPECT_EQ(inputs[0], Literal(+1).Index());
EXPECT_EQ(inputs[1], Literal(+3).Index());
EXPECT_EQ(table, 0b0110) << std::bitset<4>(table);
}
TEST(CanonicalizeFunctionTruthTableTest, AndGateWithXAndNotX2) {
LiteralIndex output = Literal(+1).Index();
std::vector<LiteralIndex> inputs{Literal(-2).Index(), Literal(+2).Index()};
int table = 0b1000;
const int new_size =
CanonicalizeFunctionTruthTable(output, absl::MakeSpan(inputs), table);
CHECK_EQ(new_size, 0); // Fixed to zero.
}
TEST(CanonicalizeFunctionTruthTableTest, RandomTest) {
absl::BitGen random;
const int num_vars = 8;

14
ortools/sat/lrat_proof_handler.cc
View File

@@ -802,7 +802,6 @@ ClauseId LratProofHandler::AddAndProveInferredClauseByEnumeration(
// That give us 2^(n + 1) intermediate clauses.
// Their ids will be stored in (1 << k) + binary_encoding_of_the_li.
const int n = to_dense_index.size() - new_clause.size();
CHECK_GT(n, 0); // We dealt with this above.
CHECK_EQ(n, relevant_literals.size());
const int num_intermediates = 1 << (n + 1);
std::vector<ClauseId> ids(num_intermediates, kNoClauseId);
@@ -838,11 +837,16 @@ ClauseId LratProofHandler::AddAndProveInferredClauseByEnumeration(
// The clause is the same as the one we try to prove! or smaller.
if (clauses_for_proof[i].size() == new_clause.size()) {
return ids_for_proof[i];
} else {
// TODO(user): Likely we could have simplified what we are trying to
// prove. Like I saw this happen when we prove an equivalence but we
// can actually prove that the variables are fixed.
const ClauseId new_id = id_generator_->GetNextId();
if (!AddInferredClause(new_id, new_clause, {ids_for_proof[i]})) {
return error("failed trivial inclusion proof");
}
return new_id;
}
// TODO(user): if this ever happen we can create a new id and prove it
// with clauses_for_proof[i], but for now I never saw that.
return error("Case not yet supported");
}
mask >>= new_clause.size();

381
ortools/sat/probing.cc
View File

@@ -14,11 +14,14 @@
#include "ortools/sat/probing.h"
#include <algorithm>
#include <deque>
#include <functional>
#include <optional>
#include <utility>
#include <variant>
#include <vector>
#include "absl/algorithm/container.h"
#include "absl/cleanup/cleanup.h"
#include "absl/container/btree_map.h"
#include "absl/container/btree_set.h"
@@ -51,6 +54,212 @@
namespace operations_research {
namespace sat {
// Holds a copy of the trail and of propagator reasons in order to be able to
// build LRAT proofs after the trail has been modified.
class TrailCopy {
public:
TrailCopy(const Trail& trail, const BinaryImplicationGraph& implication_graph,
const ClauseManager& clause_manager)
: trail_(trail),
implication_graph_(implication_graph),
clause_manager_(clause_manager) {}
// Updates this trail copy with the current trail state.
void CopyTrail() {
const int trail_size = trail_.Index();
trail_index_.resize(trail_.NumVariables(), -1);
trail_literals_.clear();
trail_info_.clear();
stored_reasons_.clear();
trail_literals_.reserve(trail_size);
trail_info_.reserve(trail_size);
for (int i = 0; i < trail_size; ++i) {
const Literal literal = trail_[i];
const BooleanVariable var = literal.Variable();
const AssignmentInfo& info = trail_.Info(var);
const int assignment_type = trail_.AssignmentType(var);
absl::Span<const Literal> reason;
// Get the clause ID only if it is very cheap to compute. Otherwise, delay
// its computation until it is really needed, in AppendClauseIdsFixing().
std::variant<ClauseId, const SatClause*> reason_clause = kNoClauseId;
if (assignment_type == AssignmentType::kCachedReason) {
const absl::Span<const Literal> cached_reason = trail_.Reason(var);
stored_reasons_.push_back({cached_reason.begin(), cached_reason.end()});
reason = stored_reasons_.back();
} else if (assignment_type == AssignmentType::kUnitReason) {
reason_clause = trail_.GetUnitClauseId(var);
} else if (assignment_type == implication_graph_.PropagatorId()) {
absl::Span<const Literal> original_reason = trail_.Reason(var);
DCHECK_EQ(original_reason.size(), 1);
reason = absl::MakeConstSpan(trail_literals_)
.subspan(trail_index_[original_reason[0].Variable()], 1);
DCHECK_EQ(reason[0], original_reason[0].Negated());
} else if (assignment_type == clause_manager_.PropagatorId()) {
const SatClause* sat_clause = clause_manager_.ReasonClauseOrNull(var);
if (sat_clause != nullptr) {
reason = sat_clause->AsSpan();
}
reason_clause = clause_manager_.ReasonClauseOrNull(var);
}
trail_index_[var] = i;
trail_literals_.push_back(literal);
trail_info_.emplace_back(info.level, assignment_type, reason,
reason_clause);
}
const int num_decisions = trail_.CurrentDecisionLevel();
decisions_.clear();
decisions_.reserve(num_decisions);
for (int i = 0; i < num_decisions; ++i) {
decisions_.push_back(trail_.Decisions()[i].literal);
}
}
// Same as ClauseManager::AppendClauseIdsFixing(), but adapted to work on this
// trail copy instead of on the real trail.
void AppendClauseIdsFixing(
absl::Span<const Literal> literals, std::vector<ClauseId>* clause_ids,
LiteralIndex decision,
absl::flat_hash_map<std::pair<Literal, Literal>, ClauseId>
tmp_binary_clause_ids) {
// Mark the literals whose reason must be expanded, and put them in a heap.
tmp_mark_.ClearAndResize(BooleanVariable(trail_index_.size()));
marked_trail_indices_heap_.clear();
for (const Literal lit : literals) {
tmp_mark_.Set(lit.Variable());
marked_trail_indices_heap_.push_back(trail_index_[lit.Variable()]);
}
absl::c_make_heap(marked_trail_indices_heap_);
const int current_level = decisions_.size();
// The min level of the expanded literals.
int min_level = current_level;
// Unit clauses must come first. We put them in clause_ids directly. We put
// the others in non_unit_clause_ids and append them to clause_ids at the
// end.
std::vector<ClauseId>& non_unit_clause_ids =
tmp_clause_ids_for_append_clauses_fixing_;
non_unit_clause_ids.clear();
while (!marked_trail_indices_heap_.empty()) {
absl::c_pop_heap(marked_trail_indices_heap_);
const int trail_index = marked_trail_indices_heap_.back();
marked_trail_indices_heap_.pop_back();
const Literal marked_literal = trail_literals_[trail_index];
const TrailInfo& trail_info = trail_info_[trail_index];
// Stop at decisions, at literals fixed at root, and at literals implied
// by the decision at their level.
const int level = trail_info.level;
if (level > 0) min_level = std::min(min_level, level);
if (trail_info.assignment_type == AssignmentType::kSearchDecision) {
continue;
}
if (level == 0) {
clause_ids->push_back(std::get<ClauseId>(trail_info.reason_clause));
continue;
}
const Literal level_decision = decisions_[level - 1];
ClauseId clause_id = implication_graph_.GetClauseId(
level_decision.Negated(), marked_literal);
if (clause_id == kNoClauseId) {
const auto it = tmp_binary_clause_ids.find(
std::minmax(level_decision.Negated(), marked_literal));
if (it != tmp_binary_clause_ids.end()) {
clause_id = it->second;
}
}
if (clause_id != kNoClauseId) {
non_unit_clause_ids.push_back(clause_id);
continue;
}
// Mark all the literals of its reason.
for (const Literal literal : trail_info.reason) {
const BooleanVariable var = literal.Variable();
if (!tmp_mark_[var]) {
const int trail_index = trail_index_[var];
const TrailInfo& info = trail_info_[trail_index];
tmp_mark_.Set(var);
if (info.level > 0) {
marked_trail_indices_heap_.push_back(trail_index);
absl::c_push_heap(marked_trail_indices_heap_);
} else {
clause_ids->push_back(std::get<ClauseId>(info.reason_clause));
}
}
}
non_unit_clause_ids.push_back(ReasonClauseId(trail_index));
}
// Add the implication chain from `decision` to all the decisions found
// during the expansion.
if (Literal(decision) != decisions_[current_level - 1]) {
// If `decision` is not the last decision, it must directly imply it.
clause_ids->push_back(implication_graph_.GetClauseId(
Literal(decision).Negated(), decisions_[current_level - 1]));
}
for (int level = current_level - 1; level >= min_level; --level) {
clause_ids->push_back(implication_graph_.GetClauseId(
decisions_[level].Negated(), decisions_[level - 1]));
}
clause_ids->insert(clause_ids->end(), non_unit_clause_ids.rbegin(),
non_unit_clause_ids.rend());
}
private:
// Same as ClauseManager::ReasonClauseId(), but adapted to work on this trail
// copy instead of on the real trail.
ClauseId ReasonClauseId(int trail_index) const {
const TrailInfo& trail_info = trail_info_[trail_index];
const int assignment_type = trail_info.assignment_type;
if (assignment_type == AssignmentType::kCachedReason ||
assignment_type == AssignmentType::kUnitReason) {
return std::get<ClauseId>(trail_info.reason_clause);
} else if (assignment_type == implication_graph_.PropagatorId()) {
return implication_graph_.GetClauseId(trail_literals_[trail_index],
trail_info.reason[0].Negated());
} else if (assignment_type == clause_manager_.PropagatorId()) {
const SatClause* reason =
std::get<const SatClause*>(trail_info.reason_clause);
if (reason != nullptr) {
return clause_manager_.GetClauseId(reason);
}
}
return kNoClauseId;
}
struct TrailInfo {
int level;
int assignment_type;
// For literals propagated by the BinaryImplicationGraph, the negation of
// the original reason. For literals propagated by the ClauseManager, *all*
// the literals of the SatClause (which includes the propagated variable).
// For kCachedReason, this is the stored reason. Empty for kUnitReason.
absl::Span<const Literal> reason;
// Holds a clause ID if `assignment_type` is kCachedReason or kUnitReason,
// or a SatClause* if `assignment_type` corresponds to the ClauseManager.
std::variant<ClauseId, const SatClause*> reason_clause;
};
const Trail& trail_;
const BinaryImplicationGraph& implication_graph_;
const ClauseManager& clause_manager_;
util_intops::StrongVector<BooleanVariable, int> trail_index_;
std::vector<Literal> trail_literals_;
std::vector<TrailInfo> trail_info_;
// We use a deque for pointer stability (they are kept in TrailInfo::reason).
std::deque<std::vector<Literal>> stored_reasons_;
std::vector<Literal> decisions_;
SparseBitset<BooleanVariable> tmp_mark_;
std::vector<int> marked_trail_indices_heap_;
std::vector<ClauseId> tmp_clause_ids_for_append_clauses_fixing_;
};
Prober::Prober(Model* model)
: trail_(*model->GetOrCreate<Trail>()),
assignment_(model->GetOrCreate<SatSolver>()->Assignment()),
@@ -63,11 +272,14 @@ Prober::Prober(Model* model)
clause_manager_(model->GetOrCreate<ClauseManager>()),
clause_id_generator_(model->GetOrCreate<ClauseIdGenerator>()),
lrat_proof_handler_(model->Mutable<LratProofHandler>()),
trail_copy_(new TrailCopy(trail_, *implication_graph_, *clause_manager_)),
drat_enabled_(lrat_proof_handler_ != nullptr &&
(lrat_proof_handler_->drat_check_enabled() ||
lrat_proof_handler_->drat_output_enabled())),
logger_(model->GetOrCreate<SolverLogger>()) {}
Prober::~Prober() { delete trail_copy_; }
bool Prober::ProbeBooleanVariables(const double deterministic_time_limit) {
const int num_variables = sat_solver_->NumVariables();
const VariablesAssignment& assignment = sat_solver_->Assignment();
@@ -87,6 +299,12 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
new_integer_bounds_.clear();
propagated_.ResetAllToFalse();
tmp_binary_clause_ids_.clear();
// We block clause deletion since we compute some LRAT proofs in a delayed
// way, and we need to make sure the clauses that were used are still around.
sat_solver_->BlockClauseDeletion(true);
absl::Cleanup unblock_clause_deletion = [&] {
sat_solver_->BlockClauseDeletion(false);
};
for (const Literal decision : {Literal(b, true), Literal(b, false)}) {
if (assignment_.LiteralIsAssigned(decision)) continue;
@@ -143,7 +361,7 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
}
if (lrat_proof_handler_ != nullptr) {
auto add_tmp_implication = [&](const Literal decision, const Literal l) {
for (const Literal l : new_implied_or_fixed_literals_) {
tmp_clause_ids_.clear();
clause_manager_->AppendClauseIdsFixing(
{l}, &tmp_clause_ids_, decision.Index(),
@@ -161,23 +379,21 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
tmp_binary_clause_ids_[std::minmax(decision.Negated(), l)] = clause_id;
num_lrat_clauses_++;
num_lrat_proof_clauses_ += tmp_clause_ids_.size();
};
for (const Literal l : new_implied_or_fixed_literals_) {
add_tmp_implication(decision, l);
}
if (decision.IsNegative() && !to_fix_at_true_.empty()) {
// Redo the first pass to add the LRAT clauses b => to_fix_at_true.
if (!sat_solver_->ResetToLevelZero()) return false;
if (assignment_.LiteralIsAssigned(decision)) continue;
CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
if (sat_solver_->EnqueueDecisionAndBackjumpOnConflict(
decision.Negated()) == kUnsatTrailIndex) {
return false;
}
if (sat_solver_->ModelIsUnsat()) return false;
if (sat_solver_->CurrentDecisionLevel() == 0) continue;
if (decision.IsPositive()) {
trail_copy_->CopyTrail();
} else if (!to_fix_at_true_.empty()) {
for (const Literal l : to_fix_at_true_) {
add_tmp_implication(decision.Negated(), l);
tmp_clause_ids_.clear();
trail_copy_->AppendClauseIdsFixing({l}, &tmp_clause_ids_,
decision.NegatedIndex(),
tmp_binary_clause_ids_);
const ClauseId clause_id = clause_id_generator_->GetNextId();
lrat_proof_handler_->AddInferredClause(clause_id, {decision, l},
tmp_clause_ids_);
tmp_binary_clause_ids_[std::minmax(decision, l)] = clause_id;
num_lrat_clauses_++;
num_lrat_proof_clauses_ += tmp_clause_ids_.size();
}
}
}
@@ -980,6 +1196,8 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
num_conflicts_ = 0;
num_new_binary_ = 0;
num_subsumed_ = 0;
num_lrat_clauses_ = 0;
num_lrat_proof_clauses_ = 0;
// Reset the solver in case it was already used.
if (!sat_solver_->ResetToLevelZero()) return false;
@@ -1030,12 +1248,14 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
}
binary_clause_extracted_.assign(trail_.Index(), false);
trail_implication_clauses_.assign(trail_.Index(), {kNoClauseId, false});
while (!time_limit_->LimitReached() &&
time_limit_->GetElapsedDeterministicTime() <= limit) {
// We only enqueue literal at level zero if we don't use "tree look".
if (!options.use_tree_look) {
if (!sat_solver_->BacktrackAndPropagateReimplications(0)) return false;
DeleteTemporaryLratImplicationsAfterBacktrack();
}
// Probing works by taking a series of decisions, and by analyzing what
@@ -1073,6 +1293,7 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
const int new_level = sat_solver_->CurrentDecisionLevel();
if (new_level == 0) continue;
const Literal last_decision = trail_.Decisions()[new_level - 1].literal;
binary_clauses_to_extract_.clear();
for (int i = first_new_trail_index; i < trail_.Index(); ++i) {
const Literal l = trail_[i];
if (l == last_decision) continue;
@@ -1096,7 +1317,9 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
// propagation for one literal we do finish it before calling again
// the binary propagation.
if (trail_.AssignmentType(l.Variable()) != binary_propagator_id_) {
MaybeExtractImplication(last_decision, l);
if (ShouldExtractImplication(l)) {
binary_clauses_to_extract_.push_back(l);
}
}
} else {
// If we don't extract binary, we don't need to explore any of
@@ -1104,6 +1327,9 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
processed_.Set(l.Index());
}
}
if (!binary_clauses_to_extract_.empty()) {
ExtractImplications(last_decision, binary_clauses_to_extract_);
}
if (options.subsume_with_binary_clause) {
SubsumeWithBinaryClauseUsingBlockingLiteral(last_decision);
@@ -1112,6 +1338,7 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
if (!sat_solver_->ResetToLevelZero()) return false;
if (!ProcessLiteralsToFix()) return false;
DeleteTemporaryLratImplicationsAfterBacktrack();
clause_manager_->CleanUpWatchers();
// Display stats.
@@ -1129,6 +1356,8 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
<< " explicit_fix:" << num_explicit_fix_
<< " num_conflicts:" << num_conflicts_
<< " new_binary_clauses: " << num_new_binary_
<< " num_lrat_clauses: " << num_lrat_clauses_
<< " num_lrat_proof_clauses: " << num_lrat_proof_clauses_
<< " subsumed: " << num_subsumed_ << " dtime: " << time_diff
<< " wtime: " << wall_timer.Get() << (limit_reached ? " (Aborted)" : "");
return sat_solver_->FinishPropagation();
@@ -1190,8 +1419,10 @@ bool FailedLiteralProbing::ComputeNextDecisionInOrder(
// This is a backtrack marker, go back one level.
CHECK_GT(sat_solver_->CurrentDecisionLevel(), 0);
if (!sat_solver_->BacktrackAndPropagateReimplications(
sat_solver_->CurrentDecisionLevel() - 1))
sat_solver_->CurrentDecisionLevel() - 1)) {
return false;
}
DeleteTemporaryLratImplicationsAfterBacktrack();
continue;
}
const Literal candidate(index);
@@ -1227,6 +1458,7 @@ bool FailedLiteralProbing::GetNextDecisionInNoParticularOrder(
if (!sat_solver_->BacktrackAndPropagateReimplications(level - 1)) {
return false;
}
DeleteTemporaryLratImplicationsAfterBacktrack();
}
return true;
}
@@ -1263,6 +1495,7 @@ bool FailedLiteralProbing::EnqueueDecisionAndBackjumpOnConflict(
ClauseId fixed_decision_unit_id = kNoClauseId;
auto conflict_callback = [&](ClauseId conflict_id,
absl::Span<const Literal> conflict_clause) {
DeleteTemporaryLratImplicationsAfterBacktrack();
if (fixed_decision_unit_id != kNoClauseId) return;
tmp_clause_ids_.clear();
clause_manager_->AppendClauseIdsFixing(conflict_clause, &tmp_clause_ids_,
@@ -1272,6 +1505,8 @@ bool FailedLiteralProbing::EnqueueDecisionAndBackjumpOnConflict(
lrat_proof_handler_->AddInferredClause(fixed_decision_unit_id,
{Literal(next_decision).Negated()},
tmp_clause_ids_);
num_lrat_clauses_++;
num_lrat_proof_clauses_ += tmp_clause_ids_.size();
};
first_new_trail_index = sat_solver_->EnqueueDecisionAndBackjumpOnConflict(
Literal(next_decision),
@@ -1282,6 +1517,8 @@ bool FailedLiteralProbing::EnqueueDecisionAndBackjumpOnConflict(
if (first_new_trail_index == kUnsatTrailIndex) return false;
binary_clause_extracted_.resize(first_new_trail_index);
binary_clause_extracted_.resize(trail_.Index(), false);
trail_implication_clauses_.resize(first_new_trail_index);
trail_implication_clauses_.resize(trail_.Index(), {kNoClauseId, false});
// This is tricky, depending on the parameters, and for integer problem,
// EnqueueDecisionAndBackjumpOnConflict() might create new Booleans.
@@ -1341,15 +1578,19 @@ bool FailedLiteralProbing::EnqueueDecisionAndBackjumpOnConflict(
return true;
}
void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
const Literal l) {
bool FailedLiteralProbing::ShouldExtractImplication(const Literal l) {
const auto& info = trail_.Info(l.Variable());
if (binary_clause_extracted_[info.trail_index]) return;
if (binary_clause_extracted_[info.trail_index]) return false;
binary_clause_extracted_[info.trail_index] = true;
// If the variable was true at level zero, this is not necessary.
if (info.level == 0) return;
return info.level > 0;
}
void FailedLiteralProbing::ExtractImplication(const Literal last_decision,
const Literal l, bool lrat_only) {
const auto& info = trail_.Info(l.Variable());
// TODO(user): Think about trying to extract clause that will not
// get removed by transitive reduction later. If we can both extract
@@ -1360,7 +1601,6 @@ void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
// of all literals in the reason for this propagation. And use this
// as a reason for later hyber binary resolution. Like we do when
// this clause subsumes the reason.
++num_new_binary_;
DCHECK(assignment_.LiteralIsTrue(l));
CHECK_NE(l.Variable(), last_decision.Variable());
@@ -1375,19 +1615,97 @@ void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
if (lrat_proof_handler_ != nullptr) {
clause_id = clause_id_generator_->GetNextId();
tmp_clause_ids_.clear();
clause_manager_->AppendClauseIdsFixing({l}, &tmp_clause_ids_,
last_decision);
clause_manager_->AppendClauseIdsFixing(
{l}, &tmp_clause_ids_, last_decision,
[&](int /*level*/, int trail_index) {
return trail_implication_clauses_[trail_index].first;
});
// Cache this LRAT clause so that it can be reused for later proofs. Do this
// only if `l` is propagated by the last decision, so that this cache entry
// remains valid when we backtrack later decisions.
if (info.level == sat_solver_->CurrentDecisionLevel()) {
trail_implication_clauses_[info.trail_index] = {clause_id, lrat_only};
}
lrat_proof_handler_->AddInferredClause(
clause_id, {last_decision.Negated(), l}, tmp_clause_ids_);
num_lrat_clauses_++;
num_lrat_proof_clauses_ += tmp_clause_ids_.size();
}
if (lrat_only) return;
// Each time we extract a binary clause, we change the reason in the trail.
// This is important as it will allow us to remove clauses that are now
// subsumed by this binary, even if it was a reason.
++num_new_binary_;
CHECK(implication_graph_->AddBinaryClauseAndChangeReason(
clause_id, l, last_decision.Negated()));
}
void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
const Literal l) {
if (ShouldExtractImplication(l)) {
ExtractImplication(last_decision, l);
}
}
void FailedLiteralProbing::ExtractImplications(
Literal last_decision, absl::Span<const Literal> literals) {
// 1. Find all the literals which appear in the expansion of the reasons of
// all the `literals` and collect them in reverse trail order in
// `tmp_marked_literals_`.
// 1.a Put the `literals` in a heap.
tmp_mark_.ClearAndResize(BooleanVariable(trail_.NumVariables()));
tmp_heap_.clear();
const VariablesAssignment& assignment = trail_.Assignment();
for (const Literal lit : literals) {
CHECK(assignment.LiteralIsAssigned(lit));
tmp_mark_.Set(lit.Variable());
tmp_heap_.push_back(trail_.Info(lit.Variable()).trail_index);
}
absl::c_make_heap(tmp_heap_);
// 1.b Expand the reasons of all the literals in the heap and add the reason
// literals back in the heap. Collect the literals in the order they are
// popped from the heap in `tmp_marked_literals_`.
tmp_marked_literals_.clear();
while (!tmp_heap_.empty()) {
absl::c_pop_heap(tmp_heap_);
const int trail_index = tmp_heap_.back();
tmp_heap_.pop_back();
const Literal marked_literal = trail_[trail_index];
tmp_marked_literals_.push_back(marked_literal);
DCHECK_GT(trail_.Info(marked_literal.Variable()).level, 0);
DCHECK_NE(trail_.AssignmentType(marked_literal.Variable()),
AssignmentType::kSearchDecision);
for (const Literal literal : trail_.Reason(marked_literal.Variable())) {
const BooleanVariable var = literal.Variable();
const AssignmentInfo& info = trail_.Info(var);
if (info.level > 0 && !tmp_mark_[var] &&
trail_.AssignmentType(var) != AssignmentType::kSearchDecision) {
tmp_mark_.Set(var);
tmp_heap_.push_back(info.trail_index);
absl::c_push_heap(tmp_heap_);
}
}
}
// 2. Add an LRAT implication "last_decision => l" for each literal l in
// `tmp_marked_literals_`, in increasing trail index order. Thanks to the
// cache in ExtractImplication(), the proof for each new implication has
// the same size as its reason. Also add a "real" implication in the binary
// implication graph if `l` is in `literals`.
tmp_mark_.ClearAndResize(BooleanVariable(trail_.NumVariables()));
for (const Literal lit : literals) {
tmp_mark_.Set(lit.Variable());
}
for (int i = tmp_marked_literals_.size() - 1; i >= 0; --i) {
const bool lrat_only = !tmp_mark_[tmp_marked_literals_[i].Variable()];
ExtractImplication(last_decision, tmp_marked_literals_[i], lrat_only);
}
}
// If we can extract a binary clause that subsume the reason clause, we do add
// the binary and remove the subsumed clause.
//
@@ -1479,6 +1797,8 @@ void FailedLiteralProbing::AddFailedLiteralToFix(const Literal literal) {
lrat_proof_handler_->AddInferredClause(unit_id, {literal.Negated()},
tmp_clause_ids_);
to_fix_unit_id_.push_back({unit_id});
num_lrat_clauses_++;
num_lrat_proof_clauses_ += tmp_clause_ids_.size();
}
// Fixes all the literals in to_fix_, and finish propagation.
@@ -1498,5 +1818,16 @@ bool FailedLiteralProbing::ProcessLiteralsToFix() {
return sat_solver_->FinishPropagation();
}
void FailedLiteralProbing::DeleteTemporaryLratImplicationsAfterBacktrack() {
if (lrat_proof_handler_ == nullptr) return;
for (int i = trail_.Index(); i < trail_implication_clauses_.size(); ++i) {
auto [clause_id, is_temporary] = trail_implication_clauses_[i];
if (is_temporary) {
lrat_proof_handler_->DeleteClause(clause_id, {});
}
}
trail_implication_clauses_.resize(trail_.Index(), {kNoClauseId, false});
}
} // namespace sat
} // namespace operations_research

35
ortools/sat/probing.h
View File

@@ -43,9 +43,12 @@
namespace operations_research {
namespace sat {
class TrailCopy;
class Prober {
public:
explicit Prober(Model* model);
~Prober();
// Fixes Booleans variables to true/false and see what is propagated. This
// can:
@@ -158,6 +161,7 @@ class Prober {
ClauseManager* clause_manager_;
ClauseIdGenerator* clause_id_generator_;
LratProofHandler* lrat_proof_handler_;
TrailCopy* trail_copy_;
const bool drat_enabled_;
// To detect literal x that must be true because b => x and not(b) => x.
@@ -353,9 +357,19 @@ class FailedLiteralProbing {
// do not contain last_decision.Negated().
void MaybeSubsumeWithBinaryClause(Literal last_decision, Literal l);
// If not already done, add last_decision => l to the repository.
// Functions to add "last_decision => l" to the repository if not already
// done. The Maybe() version just calls Extract() if ShouldExtract() is true.
bool ShouldExtractImplication(Literal l);
void ExtractImplication(Literal last_decision, Literal l,
bool lrat_only = false);
void MaybeExtractImplication(Literal last_decision, Literal l);
// Extracts an implication "`last_decision` => l" for each literal l in
// `literals`. This is more efficient than calling ExtractImplication() for
// each literal when LRAT is enabled.
void ExtractImplications(Literal last_decision,
absl::Span<const Literal> literals);
// Inspect the watcher list for last_decision, If we have a blocking
// literal at true (implied by last decision), then we have subsumptions.
//
@@ -375,6 +389,10 @@ class FailedLiteralProbing {
// Fixes all the literals in to_fix_, and finish propagation.
bool ProcessLiteralsToFix();
// Deletes the temporary LRAT clauses in trail_implication_clauses_ for all
// trail indices greater than the current trail index.
void DeleteTemporaryLratImplicationsAfterBacktrack();
SatSolver* sat_solver_;
BinaryImplicationGraph* implication_graph_;
TimeLimit* time_limit_;
@@ -402,13 +420,24 @@ class FailedLiteralProbing {
std::vector<Literal> to_fix_;
// For each literal in to_fix_, the ID of the corresponding LRAT unit clause.
std::vector<ClauseId> to_fix_unit_id_;
// The literals for which we want to extract "last_decision => l" clauses.
std::vector<Literal> binary_clauses_to_extract_;
// For each literal 'l' in the trail, whether a binary clause "d => l" has
// been extracted, with 'd' the decision at the same level as 'l'.
std::vector<bool> binary_clause_extracted_;
// Temporary vector used for LRAT proofs.
// For each literal on the trail, the ID of the LRAT clause stating that this
// literal is implied by the previous decisions on the trail (or kNoClauseId
// if there is no such clause), plus a Boolean indicating whether this clause
// is temporary (i.e., is not an extracted binary clause).
std::vector<std::pair<ClauseId, bool>> trail_implication_clauses_;
// Temporary data structures used for LRAT proofs.
std::vector<ClauseId> tmp_clause_ids_;
SparseBitset<BooleanVariable> tmp_mark_;
std::vector<int> tmp_heap_;
std::vector<Literal> tmp_marked_literals_;
// Stats.
int64_t num_probed_ = 0;
@@ -416,6 +445,8 @@ class FailedLiteralProbing {
int64_t num_conflicts_ = 0;
int64_t num_new_binary_ = 0;
int64_t num_subsumed_ = 0;
int64_t num_lrat_clauses_ = 0;
int64_t num_lrat_proof_clauses_ = 0;
};
} // namespace sat

8
ortools/sat/python/cp_model.py
View File

@@ -17,10 +17,10 @@
The following two sections describe the main
methods for building and solving CP-SAT models.
* [`CpModel`](#cp_model.CpModel): Methods for creating
models, including variables and constraints.
* [`CPSolver`](#cp_model.CpSolver): Methods for solving
a model and evaluating solutions.
* [`CpModel`](#cp_model.CpModel): Methods for creating models, including
variables and constraints.
* [`CpSolver`](#cp_model.CpSolver): Methods for solving a model and evaluating
solutions.
The following methods implement callbacks that the
solver calls each time it finds a new solution.

530
ortools/sat/sat_inprocessing.cc
View File

@@ -15,6 +15,7 @@
#include <algorithm>
#include <array>
#include <bitset>
#include <cmath>
#include <cstdint>
#include <deque>
@@ -91,9 +92,21 @@ bool Inprocessing::PresolveLoop(SatPresolveOptions options) {
// Mainly useful for development.
double probing_time = 0.0;
const bool log_info = VLOG_IS_ON(2);
const bool log_round_info = VLOG_IS_ON(2);
// In the presolve, we run this first as some preprocessing technique might
// change the problem clauses in such a way that make our heuristic gate
// detection miss some gates. Also, when this applies the reduction in problem
// size is huge, so it is just faster to run this early.
//
// TODO(user): If we remove fixed variables, on some problem like:
// ~/SAT24/f0426369f61595aee97055965ee7e6a3-hwmcc12miters-xits-iso-6s111.sanitized.cnf.xz
// we don't detect as much equivalences... Understand why. I suspect it is due
// to the heuristic for ITE gate that combine two clauses of size 3 to get a
// truth table on 4 variables. If one of them become of size 2, we might miss
// it. Still we should be more robust to stuff like this.
RETURN_IF_FALSE(congruence_closure_->DoOneRound(log_round_info));
// We currently do the transformations in a given order and restart each time
// we did something to make sure that the earlier step cannot strengthen more.
// This might not be the best, but it is really good during development phase
@@ -159,13 +172,6 @@ bool Inprocessing::PresolveLoop(SatPresolveOptions options) {
implication_graph_->RemoveAllRedundantVariables(&postsolve_->clauses);
}
// TODO(user): Think about the right order in this function.
if (params_.inprocessing_use_congruence_closure()) {
RETURN_IF_FALSE(RemoveFixedAndEquivalentVariables(log_round_info));
RETURN_IF_FALSE(implication_graph_->RemoveDuplicatesAndFixedVariables());
RETURN_IF_FALSE(congruence_closure_->DoOneRound(log_info));
}
// TODO(user): Combine the two? this way we don't create a full literal <->
// clause graph twice. It might make sense to reach the BCE fix point which
// is unique before each variable elimination.
@@ -1974,6 +1980,24 @@ void GateCongruenceClosure::AddToTruthTable(
}
}
namespace {
// Given a set of feasible assignment of two variables, recover the
// corresponding binary clauses.
void AppendBinaryClausesFromTruthTable(
absl::Span<const BooleanVariable> vars, SmallBitset table,
std::vector<std::pair<Literal, Literal>>* binary_used) {
DCHECK_EQ(vars.size(), 2);
for (int b = 0; b < 4; ++b) {
if (((table >> b) & 1) == 0) {
binary_used->emplace_back(Literal(vars[0], (b & 1) == 0),
Literal(vars[1], (b & 2) == 0));
}
}
}
} // namespace
// Note that this is the "hot" part of the algo, once we have the and gates,
// the congruence closure should be quite fast.
void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
@@ -1987,6 +2011,51 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
tmp_ids_.clear();
tmp_clauses_.clear();
// We deal with binary clause a bit differently.
//
// Tricky: We still include binary clause between fixed literal that haven't
// been cleaned up yet, as these are needed to really recover all gates.
//
// TODO(user): Ideally the detection code should be robust to that.
int num_fn1 = 0;
std::vector<std::pair<Literal, Literal>> binary_used;
for (LiteralIndex a(0); a < implication_graph_->literal_size(); ++a) {
if (implication_graph_->IsRedundant(Literal(a))) continue;
for (const Literal b : implication_graph_->Implications(Literal(a))) {
if (implication_graph_->IsRedundant(b)) continue;
std::array<BooleanVariable, 2> key2;
SmallBitset bitmask;
FillKeyAndBitmask({Literal(a).Negated(), b}, absl::MakeSpan(key2),
bitmask);
auto [it, inserted] = ids2_.insert({key2, bitmask});
if (!inserted) {
const SmallBitset old = it->second;
it->second &= bitmask;
if (it->second != old) {
// This is either fixing or equivalence!
//
// Doing a run of DetectEquivalences() should fix that but then
// new clause of size 3 might become binary, and the fix point might
// require a lot of step. So it is important to do it here.
const SmallBitset bitset2 = it->second;
if (lrat_proof_handler_ != nullptr) {
binary_used.clear();
AppendBinaryClausesFromTruthTable(key2, bitset2, &binary_used);
}
// If we are equivalent, we always have 2 functions.
// But if we fix a variable (like bitset2 = 0011) we just have one.
const int num_added =
ProcessTruthTable(key2, bitset2, {}, binary_used);
CHECK_GE(num_added, 1) << std::bitset<4>(bitset2);
num_fn1 += num_added;
}
}
}
}
timer.AddCounter("t2", ids2_.size());
timer.AddCounter("fn1", num_fn1);
std::vector<Literal> candidates;
for (SatClause* clause : clause_manager_->AllClausesInCreationOrder()) {
if (timer.WorkLimitIsReached()) break;
@@ -1994,6 +2063,12 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
if (clause->size() == 3) {
AddToTruthTable<3>(clause, ids3_);
// The AND gate of size 3 should be detected by the short table code, no
// need to do the algo here which should be slower.
//
// TODO(user): This seems to be less strong. I think we have some bug
// in our fixed point loop when we fix variables.
} else if (clause->size() == 4) {
AddToTruthTable<4>(clause, ids4_);
} else if (clause->size() == 5) {
@@ -2065,7 +2140,6 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
}
}
// This relies on having no duplicates.
for (const Literal target : candidates) {
if (!(*is_potential_target)[target]) continue;
@@ -2089,10 +2163,11 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
std::swap(is_potential_target, next_is_potential_target);
// Target should imply all other literal in the base clause to false.
if (count != clause_size - 1) continue;
if (count < clause_size - 1) continue;
// We have an and_gate !
// Double-check no duplicate.
// Using only the "count" require that there is no duplicates. But
// depending when this is run in the inprocessing loop, we might have
// some. Redo a pass to double check.
int second_count = 0;
for (const Literal implied : implications) {
if (implied.Variable() == target.Variable()) continue;
@@ -2101,8 +2176,14 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
marked_.Clear(implied.Negated());
}
}
CHECK_EQ(count, second_count);
// Restore is_clause_literal.
for (const Literal l : clause->AsSpan()) {
marked_.Set(l);
}
if (second_count != clause_size - 1) continue;
// We have an and_gate !
// Add the detected gate (its inputs are the negation of each clause
// literal other than the target).
gates_target_.push_back(target.Index());
@@ -2115,6 +2196,14 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
}
if (lrat_proof_handler_ != nullptr) {
gates_clauses_.Add({clause});
// Create temporary size 2 clauses for the needed binary.
for (const Literal l : clause->AsSpan()) {
if (l == target) continue;
tmp_binary_clauses_.emplace_back(
SatClause::Create({target.Negated(), l.Negated()}));
gates_clauses_.AppendToLastVector(tmp_binary_clauses_.back().get());
}
}
// Canonicalize.
@@ -2130,15 +2219,44 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
timer.AddCounter("and_gates", gates_inputs_.size());
}
int GateCongruenceClosure::CanonicalizeShortGate(GateId id) {
// Deals with fixed input variable.
absl::Span<LiteralIndex> inputs = gates_inputs_[id];
int new_size = inputs.size();
for (int i = 0; i < new_size;) {
if (assignment_.LiteralIsAssigned(Literal(inputs[i]))) {
new_size =
RemoveFixedInput(i, assignment_.LiteralIsTrue(Literal(inputs[i])),
inputs.subspan(0, new_size), gates_type_[id]);
} else {
++i;
}
}
// Now canonicalize.
new_size = CanonicalizeFunctionTruthTable(
gates_target_[id], inputs.subspan(0, new_size), gates_type_[id]);
// Resize and return.
if (new_size < gates_inputs_[id].size()) {
gates_inputs_.Shrink(id, new_size);
}
DCHECK_EQ(gates_type_[id] >> (1 << (gates_inputs_[id].size())), 0);
return new_size;
}
int GateCongruenceClosure::ProcessTruthTable(
absl::Span<const BooleanVariable> inputs, SmallBitset truth_table,
absl::Span<const TruthTableId> ids_for_proof) {
absl::Span<const TruthTableId> ids_for_proof,
absl::Span<const std::pair<Literal, Literal>> binary_used) {
int num_detected = 0;
for (int i = 0; i < inputs.size(); ++i) {
if (!IsFunction(i, inputs.size(), truth_table)) continue;
const int num_bits = inputs.size() - 1;
++num_detected;
const GateId new_id(gates_target_.size());
gates_target_.push_back(Literal(inputs[i], true));
gates_inputs_.Add({});
for (int j = 0; j < inputs.size(); ++j) {
@@ -2178,7 +2296,14 @@ int GateCongruenceClosure::ProcessTruthTable(
for (const TruthTableId id : ids_for_proof) {
gates_clauses_.AppendToLastVector(truth_tables_clauses_[id]);
}
for (const auto [a, b] : binary_used) {
tmp_binary_clauses_.emplace_back(SatClause::Create({a, b}));
gates_clauses_.AppendToLastVector(tmp_binary_clauses_.back().get());
}
}
// Canonicalize right away to deal with corner case.
CanonicalizeShortGate(new_id);
}
return num_detected;
}
@@ -2266,6 +2391,44 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
}
};
int num_merges2 = 0;
const auto merge2_into_n =
[this, &num_merges2](
absl::Span<const BooleanVariable> inputs, SmallBitset& truth_table,
std::vector<std::pair<Literal, Literal>>& binary_used) {
for (int i = 0; i < inputs.size(); ++i) {
for (int j = i + 1; j < inputs.size(); ++j) {
std::array<BooleanVariable, 2> key2 = {inputs[i], inputs[j]};
const auto it = ids2_.find(key2);
if (it == ids2_.end()) continue;
const SmallBitset bitset2 = it->second;
SmallBitset bitset = bitset2;
int new_size = 0;
std::vector<BooleanVariable> key(inputs.size());
key[new_size++] = inputs[i];
key[new_size++] = inputs[j];
for (int t = 0; t < inputs.size(); ++t) {
if (t != i && t != j) {
key[new_size] = inputs[t];
bitset |= bitset << (1 << new_size); // EXTEND
++new_size;
}
}
CanonicalizeTruthTable<BooleanVariable>(absl::MakeSpan(key),
bitset);
CHECK_EQ(inputs, absl::MakeSpan(key));
const SmallBitset old = truth_table;
truth_table &= bitset;
if (old != truth_table) {
AppendBinaryClausesFromTruthTable(key2, bitset2, &binary_used);
++num_merges2;
}
}
}
};
// Starts by processing all existing tables.
//
// TODO(user): Since we deal with and_gates differently, do we need to look at
@@ -2273,12 +2436,19 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
// kind of Boolean function on two inputs (and_gates, with any possible
// negation) and xor_gate.
std::vector<TruthTableId> ids_for_proof;
std::vector<std::pair<Literal, Literal>> binary_used;
for (TruthTableId t_id(0); t_id < truth_tables_inputs_.size(); ++t_id) {
ids_for_proof.clear();
ids_for_proof.push_back(t_id);
const absl::Span<const BooleanVariable> inputs = truth_tables_inputs_[t_id];
SmallBitset truth_table = truth_tables_bitset_[t_id];
// TODO(user): it is unlcear why this is useful. Understand a bit more the
// set of possible Boolean functions of 2 and 3 variables and their clause
// encoding.
binary_used.clear();
merge2_into_n(inputs, truth_table, binary_used);
// Merge any size-3 table included inside a size-4 gate.
// TODO(user): do it for larger gate too ?
if (inputs.size() == 4) {
@@ -2287,7 +2457,7 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
++num_tables[inputs.size()];
const int num_detected =
ProcessTruthTable(inputs, truth_table, ids_for_proof);
ProcessTruthTable(inputs, truth_table, ids_for_proof, binary_used);
num_functions[inputs.size() - 1] += num_detected;
// If this is not a function and of size 3, lets try to combine it with
@@ -2344,8 +2514,11 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
++num_combinations;
++num_tables[4];
ids_for_proof.clear();
binary_used.clear();
merge2_into_n(key, bitmask, binary_used);
merge3_into_4(key, bitmask, ids_for_proof);
num_functions[3] += ProcessTruthTable(key, bitmask, ids_for_proof);
num_functions[3] +=
ProcessTruthTable(key, bitmask, ids_for_proof, binary_used);
}
}
}
@@ -2353,12 +2526,13 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
timer.AddCounter("combine3", num_combinations);
timer.AddCounter("merges", num_merges);
timer.AddCounter("merges2", num_merges2);
// Note that we only display non-zero counters.
for (int i = 2; i < num_tables.size(); ++i) {
for (int i = 0; i < num_tables.size(); ++i) {
timer.AddCounter(absl::StrCat("t", i), num_tables[i]);
}
for (int i = 2; i < num_functions.size(); ++i) {
for (int i = 0; i < num_functions.size(); ++i) {
timer.AddCounter(absl::StrCat("fn", i), num_functions[i]);
}
}
@@ -2368,13 +2542,14 @@ namespace {
class LratGateCongruenceHelper {
public:
LratGateCongruenceHelper(
const BinaryImplicationGraph* implication_graph,
const Trail* trail, const BinaryImplicationGraph* implication_graph,
ClauseManager* clause_manager, ClauseIdGenerator* clause_id_generator,
LratProofHandler* lrat_proof_handler,
const util_intops::StrongVector<GateId, LiteralIndex>& gates_target,
const CompactVectorVector<GateId, const SatClause*>& gates_clauses,
DenseConnectedComponentsFinder& union_find)
: implication_graph_(implication_graph),
: trail_(trail),
implication_graph_(implication_graph),
clause_manager_(clause_manager),
clause_id_generator_(clause_id_generator),
lrat_proof_handler_(lrat_proof_handler),
@@ -2519,6 +2694,8 @@ class LratGateCongruenceHelper {
void AddGateClausesToTemporaryProof(GateId id) {
CHECK(lrat_proof_handler_ != nullptr);
const auto& assignment = trail_->Assignment();
std::vector<Literal> fixed;
for (const SatClause* clause : gates_clauses_[id]) {
// We rewrite each clause using new equivalences found.
marked_.ResetAllToFalse();
@@ -2528,6 +2705,9 @@ class LratGateCongruenceHelper {
bool some_change = false;
for (const Literal lit : clause->AsSpan()) {
const Literal rep = GetRepresentativeWithProofSupport(lit);
if (assignment.LiteralIsAssigned(rep)) {
fixed.push_back(rep);
}
if (rep != lit) {
some_change = true;
// We need not(rep) => not(lit). This should be equivalent to
@@ -2547,7 +2727,12 @@ class LratGateCongruenceHelper {
// If this is the case, we shouldn't need it for the proof.
if (clause_is_trivial) continue;
ClauseId new_id = clause_manager_->GetClauseId(clause);
ClauseId new_id =
clause->size() == 2
? implication_graph_->GetClauseId(clause->FirstLiteral(),
clause->SecondLiteral())
: clause_manager_->GetClauseId(clause);
CHECK_NE(new_id, kNoClauseId);
if (some_change) {
// If there is some change, we add a temporary clause id with the
// proof to go from the original clause to this one.
@@ -2563,81 +2748,32 @@ class LratGateCongruenceHelper {
tmp_proof_clauses_.Add(tmp_literals_);
}
// Hacky: If we have a single clause, then there is a chance this was
// an and_gate. We must add all the implications target => inputs[i].
// Note that the inputs are the negation of the literals in the unique
// clause, so we really have target => not(lit) for lit in clause.
// which gives (not(target), not(lit)) for the needed clause.
if (gates_clauses_[id].size() == 1) {
// Tricky: The target might have been negated ! so we recover it from
// the unique clause.
const Literal current = Literal(gates_target_[id]);
LiteralIndex real_target = kNoLiteralIndex;
for (const Literal lit : gates_clauses_[id][0]->AsSpan()) {
if (current.Variable() == lit.Variable()) {
real_target = lit.Index();
}
}
if (real_target == kNoLiteralIndex) return;
const Literal neg_target = Literal(real_target).Negated();
const Literal neg_target_rep =
GetRepresentativeWithProofSupport(neg_target);
for (const Literal lit : gates_clauses_[id][0]->AsSpan()) {
const Literal neg_lit = lit.Negated();
if (neg_lit == neg_target) continue;
// Skip trivial clause after rewrite.
const Literal neg_lit_rep = GetRepresentativeWithProofSupport(neg_lit);
if (neg_lit_rep == neg_target_rep.Negated()) continue;
ClauseId new_id = implication_graph_->GetClauseId(neg_target, neg_lit);
if (new_id == kNoClauseId) {
// We where likely not a bool_and to start with, so we shouldn't need
// these clauses.
break;
}
if (neg_lit != neg_lit_rep || neg_target != neg_target_rep) {
tmp_clause_ids_.clear();
tmp_index_to_delete_.push_back(tmp_proof_clauses_.size());
if (neg_lit != neg_lit_rep) {
tmp_clause_ids_.push_back(
GetLiteralImpliesRepresentativeClauseId(neg_lit));
}
if (neg_target != neg_target_rep) {
tmp_clause_ids_.push_back(
GetLiteralImpliesRepresentativeClauseId(neg_target));
}
tmp_clause_ids_.push_back(new_id);
new_id = clause_id_generator_->GetNextId();
lrat_proof_handler_->AddInferredClause(
new_id, {neg_target_rep, neg_lit_rep}, tmp_clause_ids_);
}
tmp_proof_clauses_id_.push_back(new_id);
CHECK_NE(neg_target_rep, neg_lit_rep);
tmp_proof_clauses_.Add({neg_target_rep, neg_lit_rep});
// Add size1 clauses.
gtl::STLSortAndRemoveDuplicates(&fixed);
for (const Literal lit : fixed) {
if (assignment.LiteralIsAssigned(lit)) {
tmp_proof_clauses_id_.push_back(
trail_->GetUnitClauseId(lit.Variable()));
tmp_proof_clauses_.Add(
{assignment.LiteralIsTrue(lit) ? lit : lit.Negated()});
}
}
}
// Same as AddAndGateTargetImplication() but with truth table based gates.
std::pair<ClauseId, ClauseId> AddShortGateTargetEquivalence(
GateId gate_a_id, GateId gate_b_id) {
std::pair<ClauseId, ClauseId> AddShortGateEquivalence(
Literal rep_a, Literal rep_b, absl::Span<const GateId> gate_ids) {
if (lrat_proof_handler_ == nullptr) return {kNoClauseId, kNoClauseId};
// Just add all clauses from both gates.
// But note that we need to remap them.
ClearTemporaryProof();
AddGateClausesToTemporaryProof(gate_a_id);
AddGateClausesToTemporaryProof(gate_b_id);
for (const GateId id : gate_ids) {
AddGateClausesToTemporaryProof(id);
}
// All clauses are now in tmp_proof_clauses_/tmp_proof_clauses_id_.
// We can add both implications with proof.
const Literal a = Literal(gates_target_[gate_a_id]);
const Literal b = Literal(gates_target_[gate_b_id]);
const Literal rep_a = GetRepresentativeWithProofSupport(a);
const Literal rep_b = GetRepresentativeWithProofSupport(b);
DCHECK(IsRepresentative(rep_a));
DCHECK(IsRepresentative(rep_b));
CHECK_NE(rep_a, rep_b);
@@ -2677,6 +2813,7 @@ class LratGateCongruenceHelper {
}
ClauseId ProofForFixingLiteral(Literal to_fix, GateId id) {
if (lrat_proof_handler_ == nullptr) return kNoClauseId;
CHECK(IsRepresentative(to_fix));
ClearTemporaryProof();
AddGateClausesToTemporaryProof(id);
@@ -2766,6 +2903,7 @@ class LratGateCongruenceHelper {
}
}
const Trail* trail_;
const BinaryImplicationGraph* implication_graph_;
ClauseManager* clause_manager_;
ClauseIdGenerator* clause_id_generator_;
@@ -2815,6 +2953,10 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
gates_type_.clear();
gates_clauses_.clear();
// Lets release the memory on exit.
CHECK(tmp_binary_clauses_.empty());
absl::Cleanup cleanup = [this] { tmp_binary_clauses_.clear(); };
ExtractAndGatesAndFillShortTruthTables(timer);
ExtractShortGates(timer);
@@ -2847,7 +2989,7 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
input_literals_to_gate.ResetFromTranspose(gates_inputs_, num_literals);
LratGateCongruenceHelper lrat_helper(
implication_graph_, clause_manager_, clause_id_generator_,
trail_, implication_graph_, clause_manager_, clause_id_generator_,
lrat_proof_handler_, gates_target_, gates_clauses_, union_find);
// Starts with all gates in the queue.
@@ -2856,10 +2998,108 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
std::vector<GateId> queue(num_gates);
for (GateId id(0); id < num_gates; ++id) queue[id.value()] = id;
// Main loop.
int num_units = 0;
int num_processed = 0;
const auto fix_literal = [&, this](Literal to_fix,
absl::Span<const ClauseId> clause_ids) {
if (assignment_.LiteralIsTrue(to_fix)) return true;
if (!clause_manager_->InprocessingFixLiteral(to_fix, clause_ids)) {
return false;
}
++num_units;
for (const GateId gate_id : input_literals_to_gate[to_fix]) {
if (in_queue[gate_id.value()]) continue;
queue.push_back(gate_id);
in_queue[gate_id.value()] = true;
}
for (const GateId gate_id : input_literals_to_gate[to_fix.Negated()]) {
if (in_queue[gate_id.value()]) continue;
queue.push_back(gate_id);
in_queue[gate_id.value()] = true;
}
return true;
};
const auto get_unit_clause = [this](Literal a) {
if (lrat_proof_handler_ == nullptr) return kNoClauseId;
return trail_->GetUnitClauseId(a.Variable());
};
int num_equivalences = 0;
const auto new_equivalence = [&, this](Literal a, Literal b,
ClauseId a_implies_b,
ClauseId b_implies_a) {
// Lets propagate fixed variable as we find new equivalences.
if (assignment_.LiteralIsAssigned(a)) {
if (assignment_.LiteralIsTrue(a)) {
return fix_literal(b, {a_implies_b, get_unit_clause(a)});
} else {
return fix_literal(b.Negated(), {b_implies_a, get_unit_clause(a)});
}
} else if (assignment_.LiteralIsAssigned(b)) {
if (assignment_.LiteralIsTrue(b)) {
return fix_literal(a, {b_implies_a, get_unit_clause(b)});
} else {
return fix_literal(a.Negated(), {a_implies_b, get_unit_clause(b)});
}
}
++num_equivalences;
DCHECK(!implication_graph_->IsRedundant(a));
DCHECK(!implication_graph_->IsRedundant(b));
if (!implication_graph_->AddBinaryClause(a_implies_b, a.Negated(), b) ||
!implication_graph_->AddBinaryClause(b_implies_a, b.Negated(), a)) {
return false;
}
for (const bool negate : {false, true}) {
const LiteralIndex x = negate ? a.NegatedIndex() : a.Index();
const LiteralIndex y = negate ? b.NegatedIndex() : b.Index();
const ClauseId x_implies_y = negate ? b_implies_a : a_implies_b;
const ClauseId y_implies_x = negate ? a_implies_b : b_implies_a;
// Because x always refer to a and y to b, this should maintain
// the invariant root(lit) = root(lit.Negated()).Negated().
// This is checked below.
union_find.AddEdge(x.value(), y.value());
const LiteralIndex rep(union_find.FindRoot(y.value()));
const LiteralIndex to_merge = rep == x ? y : x;
input_literals_to_gate.MergeInto(to_merge, rep);
if (lrat_proof_handler_ != nullptr) {
if (rep == x) {
lrat_helper.AddGateEquivalenceClauses(Literal(y), y_implies_x,
x_implies_y);
} else {
lrat_helper.AddGateEquivalenceClauses(Literal(x), x_implies_y,
y_implies_x);
}
}
// Re-add to the queue all gates with touched inputs.
//
// TODO(user): I think we could only add the gates of "to_merge"
// before we merge. This part of the code is quite quick in any
// case.
for (const GateId gate_id : input_literals_to_gate[rep]) {
if (in_queue[gate_id.value()]) continue;
queue.push_back(gate_id);
in_queue[gate_id.value()] = true;
}
}
// Invariant.
CHECK_EQ(
lrat_helper.GetRepresentativeWithProofSupport(a),
lrat_helper.GetRepresentativeWithProofSupport(a.Negated()).Negated());
CHECK_EQ(
lrat_helper.GetRepresentativeWithProofSupport(b),
lrat_helper.GetRepresentativeWithProofSupport(b.Negated()).Negated());
return true;
};
// Main loop.
int num_processed = 0;
int arity1_equivalences = 0;
while (!queue.empty()) {
++num_processed;
@@ -2912,7 +3152,6 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
const Literal rep_b = lrat_helper.GetRepresentativeWithProofSupport(b);
if (rep_a != rep_b) {
++num_equivalences;
ClauseId rep_a_implies_rep_b = kNoClauseId;
ClauseId rep_b_implies_rep_a = kNoClauseId;
if (lrat_proof_handler_ != nullptr) {
@@ -2922,71 +3161,16 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
rep_b_implies_rep_a =
lrat_helper.AddAndGateTargetImplication(other_id, id);
} else {
const auto [x, y] =
lrat_helper.AddShortGateTargetEquivalence(id, other_id);
const auto [x, y] = lrat_helper.AddShortGateEquivalence(
rep_a, rep_b, {id, other_id});
rep_a_implies_rep_b = x;
rep_b_implies_rep_a = y;
}
}
DCHECK(!implication_graph_->IsRedundant(rep_a));
DCHECK(!implication_graph_->IsRedundant(rep_b));
if (!implication_graph_->AddBinaryClause(rep_a_implies_rep_b,
rep_a.Negated(), rep_b) ||
!implication_graph_->AddBinaryClause(rep_b_implies_rep_a,
rep_b.Negated(), rep_a)) {
if (!new_equivalence(rep_a, rep_b, rep_a_implies_rep_b,
rep_b_implies_rep_a)) {
return false;
}
for (const bool negate : {false, true}) {
const LiteralIndex x =
negate ? rep_a.NegatedIndex() : rep_a.Index();
const LiteralIndex y =
negate ? rep_b.NegatedIndex() : rep_b.Index();
const ClauseId x_implies_y =
negate ? rep_b_implies_rep_a : rep_a_implies_rep_b;
const ClauseId y_implies_x =
negate ? rep_a_implies_rep_b : rep_b_implies_rep_a;
// Because x always refer to a and y to b, this should maintain
// the invariant root(lit) = root(lit.Negated()).Negated().
// This is checked below.
union_find.AddEdge(x.value(), y.value());
const LiteralIndex rep(union_find.FindRoot(y.value()));
const LiteralIndex to_merge = rep == x ? y : x;
input_literals_to_gate.MergeInto(to_merge, rep);
if (lrat_proof_handler_ != nullptr) {
if (rep == x) {
lrat_helper.AddGateEquivalenceClauses(Literal(y), y_implies_x,
x_implies_y);
} else {
lrat_helper.AddGateEquivalenceClauses(Literal(x), x_implies_y,
y_implies_x);
}
}
// Re-add to the queue all gates with touched inputs.
//
// TODO(user): I think we could only add the gates of "to_merge"
// before we merge. This part of the code is quite quick in any
// case.
for (const GateId gate_id : input_literals_to_gate[rep]) {
if (in_queue[gate_id.value()]) continue;
queue.push_back(gate_id);
in_queue[gate_id.value()] = true;
}
}
// Invariant.
CHECK_EQ(
lrat_helper.GetRepresentativeWithProofSupport(rep_a),
lrat_helper.GetRepresentativeWithProofSupport(rep_a.Negated())
.Negated());
CHECK_EQ(
lrat_helper.GetRepresentativeWithProofSupport(rep_b),
lrat_helper.GetRepresentativeWithProofSupport(rep_b.Negated())
.Negated());
}
break;
}
@@ -3016,6 +3200,8 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
// then target must be false.
if (marked_[Literal(rep).Negated()]) {
is_unit = true;
input_literals_to_gate.RemoveFromFutureOutput(id);
const Literal to_fix = Literal(gates_target_[id]).Negated();
if (!assignment_.LiteralIsTrue(to_fix)) {
absl::InlinedVector<ClauseId, 4> clause_ids;
@@ -3023,10 +3209,7 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
lrat_helper.AppendFixAndGateTargetClauses(id, Literal(rep),
clause_ids);
}
if (!clause_manager_->InprocessingFixLiteral(to_fix,
clause_ids)) {
return false;
}
if (!fix_literal(to_fix, clause_ids)) return false;
}
break;
}
@@ -3036,8 +3219,6 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
}
if (is_unit) {
++num_units;
input_literals_to_gate.RemoveFromFutureOutput(id);
break; // Abort the passes loop.
}
@@ -3077,43 +3258,36 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
.Index();
}
const int new_size = CanonicalizeFunctionTruthTable(
gates_target_[id], inputs, gates_type_[id]);
if (new_size < inputs.size()) {
gates_inputs_.Shrink(id, new_size);
}
DCHECK_EQ(gates_type_[id] >> (1 << (inputs.size())), 0);
const int new_size = CanonicalizeShortGate(id);
if (new_size == 1) {
// We have a function of size 1! This is an equivalence.
//
// TODO(user): deal with it.
++arity1_equivalences;
input_literals_to_gate.RemoveFromFutureOutput(id);
const Literal a = Literal(gates_target_[id]);
const Literal b = Literal(gates_inputs_[id][0]);
const Literal rep_a = lrat_helper.GetRepresentativeWithProofSupport(a);
const Literal rep_b = lrat_helper.GetRepresentativeWithProofSupport(b);
if (rep_a != rep_b) {
++arity1_equivalences;
const auto [a_to_b, b_to_a] =
lrat_helper.AddShortGateEquivalence(rep_a, rep_b, {id});
if (!new_equivalence(rep_a, rep_b, a_to_b, b_to_a)) {
return false;
}
}
break;
} else if (new_size == 0) {
// We have a fixed function! Just fix the literal.
input_literals_to_gate.RemoveFromFutureOutput(id);
const Literal initial_to_fix =
(gates_type_[id] & 1) == 1 ? Literal(gates_target_[id])
: Literal(gates_target_[id]).Negated();
const Literal to_fix =
lrat_helper.GetRepresentativeWithProofSupport(initial_to_fix);
if (!assignment_.LiteralIsTrue(to_fix)) {
if (lrat_proof_handler_ == nullptr) {
if (!clause_manager_->InprocessingFixLiteral(to_fix, {})) {
return false;
}
} else {
const ClauseId clause_id =
lrat_helper.ProofForFixingLiteral(to_fix, id);
if (!clause_manager_->InprocessingAddUnitClause(clause_id,
to_fix)) {
return false;
}
}
++num_units;
const ClauseId clause_id =
lrat_helper.ProofForFixingLiteral(to_fix, id);
if (!fix_literal(to_fix, {clause_id})) return false;
}
input_literals_to_gate.RemoveFromFutureOutput(id);
break;
}
}

25
ortools/sat/sat_inprocessing.h
View File

@@ -449,6 +449,7 @@ class GateCongruenceClosure {
explicit GateCongruenceClosure(Model* model)
: assignment_(model->GetOrCreate<Trail>()->Assignment()),
sat_solver_(model->GetOrCreate<SatSolver>()),
trail_(model->GetOrCreate<Trail>()),
implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
clause_manager_(model->GetOrCreate<ClauseManager>()),
clause_id_generator_(model->GetOrCreate<ClauseIdGenerator>()),
@@ -508,9 +509,10 @@ class GateCongruenceClosure {
// Detects gates encoded in the given truth table, and add them to the set
// of gates. Returns the number of gate detected.
int ProcessTruthTable(absl::Span<const BooleanVariable> inputs,
SmallBitset truth_table,
absl::Span<const TruthTableId> ids_for_proof = {});
int ProcessTruthTable(
absl::Span<const BooleanVariable> inputs, SmallBitset truth_table,
absl::Span<const TruthTableId> ids_for_proof,
absl::Span<const std::pair<Literal, Literal>> binary_used);
// Add a small clause to the corresponding truth table.
template <int arity>
@@ -518,8 +520,13 @@ class GateCongruenceClosure {
absl::flat_hash_map<std::array<BooleanVariable, arity>,
TruthTableId>& ids);
// Make sure the small gate at given id is canonicalized.
// Returns its number of inputs.
int CanonicalizeShortGate(GateId id);
const VariablesAssignment& assignment_;
SatSolver* sat_solver_;
Trail* trail_;
BinaryImplicationGraph* implication_graph_;
ClauseManager* clause_manager_;
ClauseIdGenerator* clause_id_generator_;
@@ -554,6 +561,14 @@ class GateCongruenceClosure {
CompactVectorVector<GateId, LiteralIndex> gates_inputs_;
CompactVectorVector<GateId, const SatClause*> gates_clauses_;
// Truth tables on 2 variables are handled differently, and we don't use
// a TruthTableId indirection.
//
// TODO(user): it feels like we could benefit from just storing this all
// the time in the binary_implication graph. This allow to never add duplicate
// and detect easy case of fixing/equivalences right away. To investigate.
absl::flat_hash_map<std::array<BooleanVariable, 2>, SmallBitset> ids2_;
// Map (Xi) (sorted) to a bitmask corresponding to the allowed values.
// We loop over all short clauses to fill this. We actually store an "id"
// pointing in the vectors below.
@@ -571,6 +586,10 @@ class GateCongruenceClosure {
std::vector<TruthTableId> tmp_ids_;
std::vector<SatClause*> tmp_clauses_;
// Temporary SatClause* for binary, so we don't need to specialize too much
// code for them.
std::vector<std::unique_ptr<SatClause>> tmp_binary_clauses_;
// For stats.
double total_dtime_ = 0.0;
double total_wtime_ = 0.0;

11
ortools/sat/scheduling_helpers.cc
View File

@@ -531,6 +531,17 @@ void SchedulingConstraintHelper::AddReasonForBeingBeforeAssumingNoOverlap(
starts_[before].var == ends_[before].var &&
starts_[after].var == ends_[after].var;
if (fixed_size && sizes_[after].constant == 0 &&
sizes_[before].constant == 0) {
// If both sizes are fixed to zero use the trivial explanation.
const auto [expr, ub] =
EncodeDifferenceLowerThan(ends_[before], starts_[after], 0);
DCHECK_LE(linear2_bounds_->UpperBound(expr), ub);
linear2_bounds_->AddReasonForUpperBoundLowerThan(expr, ub, &literal_reason_,
&integer_reason_);
return;
}
// Prefer the straightforward linear2 explanation as it is more likely this
// comes from level zero or a single enforcement literal. Also handle the
// fixed size case. This explains with at most two integer bounds.