27#include "absl/container/flat_hash_map.h"
28#include "absl/log/check.h"
29#include "absl/strings/str_cat.h"
30#include "absl/types/span.h"
64 std::function<
Literal(
int x)> create_lit,
70 node.create_lit_ = std::move(create_lit);
73 node.literals_.push_back(node.create_lit_(
lb));
77 node.for_sorting_ = node.literals_[0].Variable();
83 CHECK(literals_.empty()) <<
"Already initialized";
85 const BooleanVariable first_var_index(solver->
NumVariables());
87 for (
int i = 0;
i < n; ++
i) {
88 literals_.push_back(
Literal(first_var_index +
i,
true));
93 lb_ = a->lb_ +
b->lb_;
95 depth_ = 1 + std::max(a->depth_,
b->depth_);
98 for_sorting_ = first_var_index;
103 CHECK_GE(nodes.size(), 2);
104 CHECK(literals_.empty()) <<
"Already initialized";
106 const Literal new_literal(var,
true);
107 literals_.push_back(new_literal);
114 std::vector<Literal> clause{new_literal.
Negated()};
117 clause.push_back(node->literals_[0]);
119 depth_ = std::max(node->depth_ + 1, depth_);
120 for_sorting_ = std::min(for_sorting_, node->for_sorting_);
130 CHECK(literals_.empty()) <<
"Already initialized";
131 const BooleanVariable first_var_index(solver->
NumVariables());
133 literals_.emplace_back(first_var_index,
true);
136 ub_ = a->ub_ +
b->ub_;
137 lb_ = a->lb_ +
b->lb_;
138 depth_ = 1 + std::max(a->depth_,
b->depth_);
141 for_sorting_ = std::min(a->for_sorting_,
b->for_sorting_);
146 CHECK(literals_.empty()) <<
"Already initialized";
149 ub_ = a->ub_ +
b->ub_;
151 weight_lb_ = a->lb_ +
b->lb_;
152 lb_ = weight_lb_ + 1;
153 depth_ = 1 + std::max(a->depth_,
b->depth_);
156 for_sorting_ = std::min(a->for_sorting_,
b->for_sorting_);
161 if (create_lit_ !=
nullptr) {
162 literals_.emplace_back(create_lit_(
current_ub()));
164 CHECK_NE(solver,
nullptr);
165 literals_.emplace_back(BooleanVariable(solver->
NumVariables()),
true);
168 if (literals_.size() > 1) {
170 literals_[literals_.size() - 2]);
176 if (!literals_.empty()) {
178 while (
i < literals_.size() &&
183 literals_.erase(literals_.begin(), literals_.begin() +
i);
184 while (!literals_.empty() &&
186 literals_.pop_back();
187 ub_ = lb_ + literals_.size();
191 if (weight_lb_ >= lb_)
return Coefficient(0);
192 const Coefficient result = Coefficient(lb_ - weight_lb_) * weight_;
198 CHECK_GT(weight_, 0);
199 const Coefficient num_allowed = (gap / weight_);
200 if (num_allowed > std::numeric_limits<int>::max() / 2)
return;
202 std::max(0, (weight_lb_ - lb_) +
static_cast<int>(num_allowed.value()));
203 if (
size() <= new_size)
return;
204 for (
int i = new_size;
i <
size(); ++
i) {
207 literals_.resize(new_size);
208 ub_ = lb_ + new_size;
213 for (
int i = 1;
i <
size(); ++
i) {
233 const int index = weight_lb_ - lb_;
234 return index < literals_.size() && literals_[index].Negated() == other;
239 const int index = weight_lb_ - lb_;
240 CHECK_GE(index, 0) <<
"Not reduced?";
241 while (index >= literals_.size()) {
244 return literals_[index].Negated();
248 CHECK_LT(weight_lb_ - lb_, literals_.size());
253 return weight_ == 0 || weight_lb_ >= ub_;
259 absl::StrAppend(&result,
"depth:", depth_);
260 absl::StrAppend(&result,
" [", lb_,
",", lb_ + literals_.size(),
"]");
261 absl::StrAppend(&result,
" ub:", ub_);
262 absl::StrAppend(&result,
" weight:", weight_.value());
263 absl::StrAppend(&result,
" weight_lb:", weight_lb_);
264 absl::StrAppend(&result,
" values:");
265 const size_t limit = 20;
267 for (
int i = 0;
i < std::min(literals_.size(), limit); ++
i) {
277 absl::StrAppend(&result,
" val:", lb_ + value);
293 std::vector<EncodingNode*> to_process;
294 to_process.push_back(node);
301 const bool complete_encoding =
false;
303 while (!to_process.empty()) {
307 to_process.pop_back();
310 if (a ==
nullptr)
continue;
311 CHECK_NE(solver,
nullptr);
323 CHECK_GE(a->
current_ub() - 1 +
b->lb(), target - 1);
326 to_process.push_back(a);
331 if (
b->current_ub() !=
b->ub()) {
332 CHECK_GE(
b->current_ub() - 1 + a->
lb(), target - 1);
333 if (
b->current_ub() - 1 + a->
lb() < target) {
334 CHECK(
b->IncreaseCurrentUB(solver));
335 to_process.push_back(
b);
340 for (
int ia = a->
lb(); ia < a->current_ub(); ++ia) {
341 const int ib = target - ia;
342 if (complete_encoding && ib >=
b->lb() && ib < b->current_ub()) {
347 if (complete_encoding && ib ==
b->ub()) {
352 if (ib - 1 ==
b->lb() - 1) {
356 if ((ib - 1) >=
b->lb() && (ib - 1) <
b->current_ub()) {
360 b->GreaterThan(ib - 1).Negated());
366 const int ib = target - (a->
lb() - 1);
367 if ((ib - 1) ==
b->lb() - 1) {
370 if ((ib - 1) >=
b->lb() && (ib - 1) <
b->current_ub()) {
372 b->GreaterThan(ib - 1).Negated());
378 const int ib = target - a->
ub();
379 if (complete_encoding && ib >=
b->lb() && ib < b->current_ub()) {
394 std::min(Coefficient(a->
size() +
b->size()), upper_bound).value();
396 for (
int ia = 0; ia < a->
size(); ++ia) {
397 if (ia +
b->size() < size) {
408 for (
int ib = 0; ib <
b->size(); ++ib) {
409 if (ib + a->
size() < size) {
420 for (
int ia = 0; ia < a->
size(); ++ia) {
421 for (
int ib = 0; ib <
b->size(); ++ib) {
422 if (ia + ib < size) {
427 if (ia + ib + 1 < size) {
431 b->literal(ib).Negated());
434 b->literal(ib).Negated());
442 const std::vector<EncodingNode*>& nodes,
444 std::deque<EncodingNode>* repository) {
445 std::deque<EncodingNode*> dq(nodes.begin(), nodes.end());
446 while (dq.size() > 1) {
451 repository->push_back(
FullMerge(upper_bound, a,
b, solver));
452 dq.push_back(&repository->back());
458struct SortEncodingNodePointers {
459 bool operator()(EncodingNode* a, EncodingNode*
b)
const {
return *a < *
b; }
464 Coefficient weight,
const std::vector<EncodingNode*>& nodes,
465 SatSolver* solver, std::deque<EncodingNode>* repository) {
466 std::priority_queue<EncodingNode*, std::vector<EncodingNode*>,
467 SortEncodingNodePointers>
468 pq(nodes.begin(), nodes.end());
469 while (pq.size() > 2) {
474 repository->push_back(
LazyMerge(a,
b, solver));
475 pq.push(&repository->back());
478 CHECK_EQ(pq.size(), 2);
493bool EncodingNodeByWeight(
const EncodingNode* a,
const EncodingNode*
b) {
494 return a->
weight() <
b->weight();
497bool EncodingNodeByDepth(
const EncodingNode* a,
const EncodingNode*
b) {
498 return a->depth() <
b->depth();
503void ReduceNodes(Coefficient upper_bound, Coefficient* lower_bound,
504 std::vector<EncodingNode*>* nodes,
SatSolver* solver) {
510 *lower_bound += n->Reduce(*solver);
516 const Coefficient gap = upper_bound - *lower_bound;
522 n->ApplyWeightUpperBound(gap, solver);
527 nodes->erase(std::remove_if(nodes->begin(), nodes->end(),
536 std::sort(nodes->begin(), nodes->end(), EncodingNodeByDepth);
539 std::sort(nodes->begin(), nodes->end(), EncodingNodeByWeight);
545 std::reverse(nodes->begin(), nodes->end());
550 const std::vector<EncodingNode*>& nodes,
553 std::vector<Literal> assumptions;
555 if (n->weight() >= stratified_lower_bound) {
556 assumptions.push_back(n->GetAssumption(solver));
563 absl::Span<const Literal> core) {
566 for (
int i = 0;
i < core.size(); ++
i) {
567 for (; index < nodes.size() && !nodes[index]->AssumptionIs(core[
i]);
570 CHECK_LT(index, nodes.size());
571 min_weight = std::min(min_weight, nodes[index]->weight());
577 Coefficient upper_bound) {
578 Coefficient result(0);
580 CHECK_GT(n->weight(), 0);
581 if (n->weight() < upper_bound) {
582 result = std::max(result, n->weight());
589 Coefficient min_weight, Coefficient gap,
592 if (!sat_solver_->ResetToLevelZero())
return false;
593 if (core.size() == 1) {
594 return sat_solver_->AddUnitClause(core[0].Negated());
598 std::vector<EncodingNode*> to_merge;
601 std::vector<EncodingNode*> new_nodes;
602 for (
int i = 0;
i < core.size(); ++
i) {
606 for (; !nodes_[index]->AssumptionIs(core[
i]); ++index) {
607 CHECK_LT(index, nodes_.size());
608 new_nodes.push_back(nodes_[index]);
610 CHECK_LT(index, nodes_.size());
614 if (alternative_encoding_ && node->
ub() > node->
lb() + 1) {
618 new_nodes.push_back(node);
621 repository_.push_back(
623 repository_.back().set_depth(node->
depth());
624 node = &repository_.back();
627 to_merge.push_back(node);
634 if (node->
weight() > min_weight) {
636 new_nodes.push_back(node);
640 for (; index < nodes_.size(); ++index) {
641 new_nodes.push_back(nodes_[index]);
649 bool in_exactly_one = (2 * min_weight) > gap;
655 if (!in_exactly_one) {
657 std::vector<Literal> bool_nodes;
658 absl::flat_hash_map<LiteralIndex, int> node_indices;
659 for (
int i = 0;
i < to_merge.size(); ++
i) {
662 if (node.
size() != 1)
continue;
663 if (node.
ub() != node.
lb() + 1)
continue;
665 if (node_indices.contains(node.
literal(0).
Index()))
continue;
667 bool_nodes.push_back(node.
literal(0));
673 std::vector<int> buffer;
674 std::vector<absl::Span<const Literal>> decomposition;
675 if (params_.core_minimization_level() > 1 && bool_nodes.size() < 300 &&
676 bool_nodes.size() > 1) {
677 const auto& assignment = sat_solver_->Assignment();
678 const int size = bool_nodes.size();
679 std::vector<std::vector<int>> graph(size);
680 for (
int i = 0;
i < size; ++
i) {
681 if (!sat_solver_->ResetToLevelZero())
return false;
682 if (!sat_solver_->EnqueueDecisionIfNotConflicting(bool_nodes[
i])) {
686 for (
int j = 0; j < size; ++j) {
687 if (
i == j)
continue;
688 if (assignment.LiteralIsFalse(bool_nodes[j])) {
689 graph[
i].push_back(j);
692 graph[j].push_back(
i);
701 if (!sat_solver_->ResetToLevelZero())
return false;
703 for (std::vector<int>& adj : graph) {
706 const std::vector<absl::Span<int>> index_decompo =
710 std::vector<Literal> new_order;
711 for (
const int i : buffer) new_order.push_back(bool_nodes[
i]);
712 bool_nodes = new_order;
713 for (
const auto span : index_decompo) {
714 if (span.size() == 1)
continue;
715 decomposition.push_back(absl::MakeSpan(
716 bool_nodes.data() + (span.data() - buffer.data()), span.size()));
719 decomposition = implications_->HeuristicAmoPartition(&bool_nodes);
723 if (decomposition.size() == 1 && decomposition[0].size() == core.size()) {
724 in_exactly_one =
true;
727 int num_in_decompo = 0;
728 if (!in_exactly_one) {
729 for (
const auto amo : decomposition) {
730 num_in_decompo += amo.size();
733 std::vector<EncodingNode*> amo_nodes;
735 const int index = node_indices.at(l.Index());
736 amo_nodes.push_back(to_merge[index]);
737 to_merge[index] =
nullptr;
745 to_merge.push_back(n);
747 if (num_in_decompo > 0) {
748 absl::StrAppend(info,
" amo:", decomposition.size(),
749 " lit:", num_in_decompo);
755 if (node ==
nullptr)
continue;
756 to_merge[new_size++] = node;
758 to_merge.resize(new_size);
765 if (in_exactly_one) {
768 node->TransformToBoolean(sat_solver_);
771 absl::StrAppend(info,
" exo");
773 nodes_.push_back(&repository_.back());
778 std::vector<LiteralWithCoeff> cst;
779 cst.reserve(core.size());
781 cst.emplace_back(l.Negated(), Coefficient(1));
783 sat_solver_->AddLinearConstraint(
784 true, Coefficient(1),
785 true, Coefficient(1), &cst);
786 return !sat_solver_->ModelIsUnsat();
790 min_weight, to_merge, sat_solver_, &repository_));
791 absl::StrAppend(info,
" d:", nodes_.back()->depth());
792 return !sat_solver_->ModelIsUnsat();
void InitializeLazyCoreNode(Coefficient weight, EncodingNode *a, EncodingNode *b)
Literal GreaterThan(int i) const
bool AssumptionIs(Literal other) const
GetAssumption() might need to create new literals.
void InitializeFullNode(int n, EncodingNode *a, EncodingNode *b, SatSolver *solver)
Coefficient Reduce(const SatSolver &solver)
void InitializeLazyNode(EncodingNode *a, EncodingNode *b, SatSolver *solver)
int size() const
Accessors to size() and literals in [lb, current_ub).
std::string DebugString(const VariablesAssignment &assignment) const
We use the solver to display the current values of the literals.
static EncodingNode GenericNode(int lb, int ub, std::function< Literal(int x)> create_lit, Coefficient weight)
static EncodingNode ConstantNode(Coefficient weight)
void set_weight(Coefficient w)
void ApplyWeightUpperBound(Coefficient gap, SatSolver *solver)
bool IncreaseCurrentUB(SatSolver *solver)
static EncodingNode LiteralNode(Literal l, Coefficient weight)
Coefficient weight() const
void TransformToBoolean(SatSolver *solver)
Indicate that the node cannot grow further than its current assumption.
EncodingNode * child_b() const
Literal literal(int i) const
EncodingNode * child_a() const
void InitializeAmoNode(absl::Span< EncodingNode *const > nodes, SatSolver *solver)
Literal GetAssumption(SatSolver *solver)
LiteralIndex Index() const
BooleanVariable Variable() const
bool ProcessCore(absl::Span< const Literal > core, Coefficient min_weight, Coefficient gap, std::string *info)
static constexpr MaxSatAssumptionOrder DEFAULT_ASSUMPTION_ORDER
::operations_research::sat::SatParameters_MaxSatAssumptionOrder max_sat_assumption_order() const
static constexpr MaxSatAssumptionOrder ORDER_ASSUMPTION_BY_WEIGHT
static constexpr MaxSatAssumptionOrder ORDER_ASSUMPTION_BY_DEPTH
bool max_sat_reverse_assumption_order() const
BooleanVariable NewBooleanVariable()
bool AddProblemClause(absl::Span< const Literal > literals)
bool AddBinaryClause(Literal a, Literal b)
Same as AddProblemClause() below, but for small clauses.
void Backtrack(int target_level)
const SatParameters & parameters() const
ABSL_MUST_USE_RESULT bool AddUnitClause(Literal true_literal)
bool AddTernaryClause(Literal a, Literal b, Literal c)
const VariablesAssignment & Assignment() const
void SetNumVariables(int num_variables)
bool LiteralIsFalse(Literal literal) const
bool LiteralIsTrue(Literal literal) const
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
EncodingNode * MergeAllNodesWithDeque(Coefficient upper_bound, const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
std::vector< Literal > ExtractAssumptions(Coefficient stratified_lower_bound, const std::vector< EncodingNode * > &nodes, SatSolver *solver)
void ReduceNodes(Coefficient upper_bound, Coefficient *lower_bound, std::vector< EncodingNode * > *nodes, SatSolver *solver)
Coefficient ComputeCoreMinWeight(const std::vector< EncodingNode * > &nodes, absl::Span< const Literal > core)
EncodingNode LazyMerge(EncodingNode *a, EncodingNode *b, SatSolver *solver)
EncodingNode FullMerge(Coefficient upper_bound, EncodingNode *a, EncodingNode *b, SatSolver *solver)
EncodingNode * LazyMergeAllNodeWithPQAndIncreaseLb(Coefficient weight, const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
void IncreaseNodeSize(EncodingNode *node, SatSolver *solver)
std::vector< absl::Span< int > > AtMostOneDecomposition(const std::vector< std::vector< int > > &graph, absl::BitGenRef random, std::vector< int > *buffer)
Coefficient MaxNodeWeightSmallerThan(const std::vector< EncodingNode * > &nodes, Coefficient upper_bound)
const Coefficient kCoefficientMax(std::numeric_limits< Coefficient::ValueType >::max())
In SWIG mode, we don't want anything besides these top-level includes.