14#ifndef OR_TOOLS_SAT_INTEGER_H_
15#define OR_TOOLS_SAT_INTEGER_H_
28#include "absl/base/attributes.h"
29#include "absl/container/btree_map.h"
30#include "absl/container/flat_hash_map.h"
31#include "absl/container/inlined_vector.h"
32#include "absl/log/check.h"
33#include "absl/strings/str_cat.h"
34#include "absl/types/span.h"
53 absl::InlinedVector<std::pair<IntegerVariable, IntegerValue>, 2>;
67 return absl::StrCat(
"(lit(",
literal.Index().value(),
") * ",
103 : sat_solver_(model->GetOrCreate<
SatSolver>()),
104 trail_(model->GetOrCreate<
Trail>()),
107 num_created_variables_(0) {}
114 VLOG(1) <<
"#variables created = " << num_created_variables_;
154 IntegerVariable var)
const;
156 IntegerVariable var)
const;
200 IntegerValue value)
const;
214 if (lit.
Index() >= reverse_encoding_.size()) {
215 return empty_integer_literal_vector_;
217 return reverse_encoding_[lit];
223 if (lit.
Index() >= reverse_equality_encoding_.size()) {
224 return empty_integer_value_vector_;
226 return reverse_equality_encoding_[lit];
233 temp_associated_vars_.clear();
235 temp_associated_vars_.push_back(l.var);
238 temp_associated_vars_.push_back(var);
240 return temp_associated_vars_;
251 const IntegerVariable result = literal_view_[lit];
259 Literal lit, IntegerVariable* view =
nullptr,
260 bool* view_is_direct =
nullptr)
const;
271 IntegerValue* bound)
const;
276 DCHECK_EQ(0, sat_solver_->CurrentDecisionLevel());
278 Literal(sat_solver_->NewBooleanVariable(),
true);
279 literal_index_true_ = literal_true.
Index();
283 (void)sat_solver_->AddUnitClause(literal_true);
285 return Literal(literal_index_true_);
293 IntegerVariable var)
const;
307 void AddImplications(
308 const absl::btree_map<IntegerValue, Literal>& map,
309 absl::btree_map<IntegerValue, Literal>::const_iterator it,
317 bool add_implications_ =
true;
318 int64_t num_created_variables_ = 0;
336 absl::btree_map<IntegerValue, Literal>>
345 reverse_equality_encoding_;
348 mutable std::vector<IntegerVariable> temp_associated_vars_;
360 absl::flat_hash_map<std::pair<PositiveOnlyIndex, IntegerValue>,
Literal>
361 equality_to_associated_literal_;
365 absl::InlinedVector<ValueLiteralPair, 2>>
376 std::vector<IntegerValue> tmp_values_;
377 std::vector<ValueLiteralPair> tmp_encoding_;
380 mutable std::vector<ValueLiteralPair> partial_encoding_;
398 virtual void Explain(
int id, IntegerValue propagation_slack,
399 IntegerVariable var_to_explain,
int trail_index,
400 std::vector<Literal>* literals_reason,
401 std::vector<int>* trail_indices_reason) = 0;
414 trail_(model->GetOrCreate<
Trail>()),
415 sat_solver_(model->GetOrCreate<
SatSolver>()),
416 time_limit_(model->GetOrCreate<
TimeLimit>()),
431 void Untrail(const
Trail& trail,
int literal_trail_index) final;
433 int64_t conflict_id) const final;
440 return IntegerVariable(var_lbs_.size());
456 IntegerValue upper_bound);
500 bool IsFixed(IntegerVariable
i)
const;
574 absl::Span<const IntegerValue> coeffs,
575 std::vector<IntegerLiteral>* reason)
const;
579 absl::Span<const IntegerValue> coeffs,
580 absl::Span<const IntegerVariable> vars,
581 std::vector<IntegerLiteral>* reason)
const;
585 absl::Span<const IntegerValue> coeffs,
586 std::vector<int>* trail_indices)
const;
610 return EnqueueInternal(i_lit,
false, {}, {}, integer_trail_.size());
614 absl::Span<const IntegerLiteral> integer_reason) {
615 return EnqueueInternal(i_lit,
false, literal_reason, integer_reason,
616 integer_trail_.size());
629 IntegerLiteral i_lit, absl::Span<const IntegerLiteral> integer_reason);
639 std::vector<IntegerLiteral>* integer_reason);
650 absl::Span<const IntegerLiteral> integer_reason,
651 int trail_index_with_same_reason) {
652 return EnqueueInternal(i_lit,
false, literal_reason, integer_reason,
653 trail_index_with_same_reason);
660 const int trail_index = integer_trail_.size();
661 lazy_reasons_.push_back(LazyReasonEntry{explainer, propagation_slack,
662 i_lit.
var, id, trail_index});
663 return EnqueueInternal(i_lit,
true, {}, {}, 0);
678 absl::Span<const IntegerLiteral> integer_reason);
689 std::vector<Literal>* output)
const;
698 int64_t
timestamp()
const {
return num_enqueues_ + num_untrails_; }
708 watchers_.push_back(p);
714 absl::Span<const IntegerLiteral> integer_reason) {
715 DCHECK(ReasonIsValid(literal_reason, integer_reason));
716 std::vector<Literal>* conflict = trail_->MutableConflict();
717 conflict->assign(literal_reason.begin(), literal_reason.end());
722 DCHECK(ReasonIsValid({}, integer_reason));
723 std::vector<Literal>* conflict = trail_->MutableConflict();
731 return var_trail_index_[var] < var_lbs_.size();
737 reversible_classes_.push_back(rev);
740 int Index()
const {
return integer_trail_.size(); }
751 std::vector<IntegerLiteral>* output)
const;
775 return !delayed_to_fix_->literal_to_fix.empty() ||
776 !delayed_to_fix_->integer_literal_to_fix.empty();
782 std::function<
bool(absl::Span<const Literal> clause,
783 absl::Span<const IntegerLiteral> integers)>
785 debug_checker_ = std::move(checker);
796 IntegerValue target_min,
797 std::vector<int>* indices)
const {
798 int64_t num_processed = 0;
800 if (expr.IsConstant()) {
801 DCHECK_GE(expr.constant, target_min);
808 if (++num_processed % 5 == 0 && time_limit_->LimitReached())
return;
815 const int index = tmp_var_to_trail_index_in_queue_[expr.var];
816 if (index == std::numeric_limits<int>::max())
continue;
818 expr.ValueAt(integer_trail_[index].bound) >= target_min) {
819 has_dependency_ =
true;
827 FindLowestTrailIndexThatExplainBound(expr.GreaterOrEqual(target_min));
829 indices->push_back(index);
837 bool ReasonIsValid(absl::Span<const Literal> literal_reason,
838 absl::Span<const IntegerLiteral> integer_reason);
841 bool ReasonIsValid(
Literal lit, absl::Span<const Literal> literal_reason,
842 absl::Span<const IntegerLiteral> integer_reason);
844 absl::Span<const Literal> literal_reason,
845 absl::Span<const IntegerLiteral> integer_reason);
854 std::vector<Literal>* InitializeConflict(
856 absl::Span<const Literal> literals_reason,
857 absl::Span<const IntegerLiteral> bounds_reason);
860 int AppendReasonToInternalBuffers(
861 absl::Span<const Literal> literal_reason,
862 absl::Span<const IntegerLiteral> integer_reason);
865 ABSL_MUST_USE_RESULT
bool EnqueueInternal(
867 absl::Span<const Literal> literal_reason,
868 absl::Span<const IntegerLiteral> integer_reason,
869 int trail_index_with_same_reason);
872 void EnqueueLiteralInternal(
Literal literal,
bool use_lazy_reason,
873 absl::Span<const Literal> literal_reason,
874 absl::Span<const IntegerLiteral> integer_reason);
879 ABSL_MUST_USE_RESULT
bool EnqueueAssociatedIntegerLiteral(
883 void MergeReasonIntoInternal(std::vector<Literal>* output,
884 int64_t conflict_id)
const;
889 int FindLowestTrailIndexThatExplainBound(
IntegerLiteral i_lit)
const;
894 void ComputeLazyReasonIfNeeded(
int reason_index)
const;
901 absl::Span<const int> Dependencies(
int reason_index)
const;
907 void AppendLiteralsReason(
int reason_index,
908 std::vector<Literal>* output)
const;
911 std::string DebugString();
914 int64_t NextConflictId();
927 mutable int var_trail_index_cache_threshold_ = 0;
929 var_trail_index_cache_;
933 absl::flat_hash_map<IntegerValue, IntegerVariable> constant_map_;
940 int32_t prev_trail_index;
944 int32_t reason_index;
946 std::vector<TrailEntry> integer_trail_;
948 struct LazyReasonEntry {
949 LazyReasonInterface* explainer;
950 IntegerValue propagation_slack;
951 IntegerVariable var_to_explain;
953 int trail_index_at_propagation_time;
955 void Explain(std::vector<Literal>* literals,
956 std::vector<int>* dependencies)
const {
957 explainer->Explain(
id, propagation_slack, var_to_explain,
958 trail_index_at_propagation_time, literals,
962 std::vector<int> lazy_reason_decision_levels_;
963 std::vector<LazyReasonEntry> lazy_reasons_;
967 std::vector<int> integer_search_levels_;
970 std::vector<int> reason_decision_levels_;
971 std::vector<int> literals_reason_starts_;
972 std::vector<Literal> literals_reason_buffer_;
977 std::vector<int> bounds_reason_starts_;
978 mutable std::vector<int> cached_sizes_;
979 std::vector<IntegerLiteral> bounds_reason_buffer_;
980 mutable std::vector<int> trail_index_reason_buffer_;
983 mutable std::vector<Literal> lazy_reason_literals_;
984 mutable std::vector<int> lazy_reason_trail_indices_;
987 mutable bool has_dependency_ =
false;
988 mutable std::vector<int> tmp_queue_;
989 mutable std::vector<IntegerVariable> tmp_to_clear_;
990 mutable util_intops::StrongVector<IntegerVariable, int>
991 tmp_var_to_trail_index_in_queue_;
992 mutable SparseBitset<BooleanVariable> added_variables_;
995 struct RelaxHeapEntry {
999 bool operator<(
const RelaxHeapEntry& o)
const {
return index < o.index; }
1001 mutable std::vector<RelaxHeapEntry> relax_heap_;
1002 mutable std::vector<int> tmp_indices_;
1005 mutable SparseBitset<IntegerVariable> tmp_marked_;
1008 std::vector<IntegerLiteral> tmp_cleaned_reason_;
1011 std::vector<int> boolean_trail_index_to_reason_index_;
1015 int first_level_without_full_propagation_ = -1;
1020 mutable int64_t last_conflict_id_ = -1;
1021 mutable bool info_is_valid_on_subsequent_last_level_expansion_ =
false;
1022 mutable util_intops::StrongVector<IntegerVariable, int>
1023 var_to_trail_index_at_lower_level_;
1024 mutable std::vector<int> tmp_seen_;
1025 mutable std::vector<IntegerVariable> to_clear_for_lower_level_;
1027 int64_t num_enqueues_ = 0;
1028 int64_t num_untrails_ = 0;
1029 int64_t num_level_zero_enqueues_ = 0;
1030 mutable int64_t num_decisions_to_break_loop_ = 0;
1032 std::vector<SparseBitset<IntegerVariable>*> watchers_;
1033 std::vector<ReversibleInterface*> reversible_classes_;
1035 mutable Domain temp_domain_;
1036 DelayedRootLevelDeduction* delayed_to_fix_;
1037 IntegerDomains* domains_;
1038 IntegerEncoder* encoder_;
1040 SatSolver* sat_solver_;
1041 TimeLimit* time_limit_;
1042 const SatParameters& parameters_;
1047 absl::flat_hash_map<std::pair<LiteralIndex, IntegerVariable>, IntegerValue>
1050 std::function<bool(absl::Span<const Literal> clause,
1051 absl::Span<const IntegerLiteral> integers)>
1052 debug_checker_ =
nullptr;
1080 LOG(FATAL) <<
"Not implemented.";
1121 void Untrail(const
Trail& trail,
int literal_trail_index) final;
1150 void WatchLowerBound(IntegerVariable var,
int id,
int watch_index = -1);
1151 void WatchUpperBound(IntegerVariable var,
int id,
int watch_index = -1);
1208 bool_to_reset_on_backtrack_.push_back(is_in_dive);
1225 const std::function<
void(
const std::vector<IntegerVariable>&)> cb) {
1226 level_zero_modified_variable_callback_.push_back(cb);
1235 stop_propagation_callback_ = callback;
1256 void UpdateCallingNeeds(
Trail* trail);
1266 return id == o.id && watch_index == o.watch_index;
1270 literal_to_watcher_;
1273 std::vector<PropagatorInterface*> watchers_;
1274 SparseBitset<IntegerVariable> modified_vars_;
1277 SparseBitset<IntegerVariable> modified_vars_for_callback_;
1281 std::vector<std::deque<int>> queue_by_priority_;
1282 std::vector<bool> in_queue_;
1286 std::vector<bool> id_need_reversible_support_;
1287 std::vector<int> id_to_level_at_last_call_;
1288 RevVector<IdType, int> id_to_greatest_common_level_since_last_call_;
1289 std::vector<std::vector<ReversibleInterface*>> id_to_reversible_classes_;
1290 std::vector<std::vector<int*>> id_to_reversible_ints_;
1292 std::vector<std::vector<int>> id_to_watch_indices_;
1293 std::vector<int> id_to_priority_;
1294 std::vector<int> id_to_idempotence_;
1297 std::vector<int> propagator_ids_to_call_at_level_zero_;
1301 bool call_again_ =
false;
1303 std::vector<std::function<void(
const std::vector<IntegerVariable>&)>>
1304 level_zero_modified_variable_callback_;
1306 std::function<bool()> stop_propagation_callback_;
1308 std::vector<bool*> bool_to_reset_on_backtrack_;
1333 Literal l, IntegerVariable
i)
const {
1334 const auto it = conditional_lbs_.find({l.
Index(),
i});
1335 if (it != conditional_lbs_.end()) {
1336 return std::max(var_lbs_[
i], it->second);
1342 Literal l, AffineExpression expr)
const {
1348 Literal l, IntegerVariable
i)
const {
1359 IntegerVariable
i)
const {
1364 IntegerVariable
i)
const {
1411 IntegerVariable var)
const {
1413 DCHECK_LT(var, integer_trail_.size());
1414 return integer_trail_[var.value()].bound;
1418 IntegerVariable var)
const {
1423 return integer_trail_[var.value()].bound ==
1442 IntegerValue result = 0;
1443 for (
int i = 0;
i < 2; ++
i) {
1452 LinearExpression2 expr)
const {
1453 expr.SimpleCanonicalization();
1454 IntegerValue result = 0;
1455 for (
int i = 0;
i < 2; ++
i) {
1456 if (expr.coeffs[
i] != 0) {
1470 if (l.
Index() >= literal_to_watcher_.size()) {
1471 literal_to_watcher_.resize(l.
Index().value() + 1);
1473 literal_to_watcher_[l].
push_back({id, watch_index});
1479 if (var.value() >= var_to_watcher_.size()) {
1480 var_to_watcher_.resize(var.value() + 1);
1487 const WatchData data = {id, watch_index};
1488 if (!var_to_watcher_[var].empty() && var_to_watcher_[var].back() == data) {
1516 return [=](
Model* model) {
1523 return [=](
Model* model) {
1525 ->GetOrCreateConstantIntegerVariable(IntegerValue(value));
1531 return [=](
Model* model) {
1534 IntegerValue(lb), IntegerValue(ub));
1540 return [=](
Model* model) {
1541 return model->
GetOrCreate<IntegerTrail>()->AddIntegerVariable(domain);
1549 auto* encoder = model->GetOrCreate<IntegerEncoder>();
1550 const IntegerVariable candidate = encoder->GetLiteralView(lit);
1553 IntegerVariable var;
1554 auto* integer_trail = model->GetOrCreate<
IntegerTrail>();
1556 if (assignment.LiteralIsTrue(lit)) {
1557 var = integer_trail->GetOrCreateConstantIntegerVariable(IntegerValue(1));
1558 }
else if (assignment.LiteralIsFalse(lit)) {
1559 var = integer_trail->GetOrCreateConstantIntegerVariable(IntegerValue(0));
1561 var = integer_trail->AddIntegerVariable(IntegerValue(0), IntegerValue(1));
1564 encoder->AssociateToIntegerEqualValue(lit, var, IntegerValue(1));
1572 return [=](
Model* model) {
1577inline std::function<int64_t(
const Model&)>
LowerBound(IntegerVariable v) {
1578 return [=](
const Model& model) {
1579 return model.Get<IntegerTrail>()->
LowerBound(v).value();
1583inline std::function<int64_t(
const Model&)>
UpperBound(IntegerVariable v) {
1584 return [=](
const Model& model) {
1585 return model.Get<IntegerTrail>()->
UpperBound(v).value();
1589inline std::function<bool(
const Model&)>
IsFixed(IntegerVariable v) {
1590 return [=](
const Model& model) {
1591 const IntegerTrail* trail = model.Get<IntegerTrail>();
1592 return trail->LowerBound(v) == trail->UpperBound(v);
1597inline std::function<int64_t(
const Model&)>
Value(IntegerVariable v) {
1598 return [=](
const Model& model) {
1599 const IntegerTrail* trail = model.Get<IntegerTrail>();
1600 CHECK_EQ(trail->LowerBound(v), trail->UpperBound(v)) << v;
1601 return trail->LowerBound(v).value();
1607 return [=](
Model* model) {
1608 if (!model->GetOrCreate<IntegerTrail>()->Enqueue(
1610 std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1611 model->GetOrCreate<
SatSolver>()->NotifyThatModelIsUnsat();
1612 VLOG(1) <<
"Model trivially infeasible, variable " << v
1613 <<
" has upper bound " << model->Get(
UpperBound(v))
1614 <<
" and GreaterOrEqual() was called with a lower bound of "
1621 return [=](
Model* model) {
1624 std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1625 model->GetOrCreate<
SatSolver>()->NotifyThatModelIsUnsat();
1626 VLOG(1) <<
"Model trivially infeasible, variable " << v
1627 <<
" has lower bound " << model->Get(
LowerBound(v))
1628 <<
" and LowerOrEqual() was called with an upper bound of " << ub;
1634inline std::function<void(
Model*)>
Equality(IntegerVariable v, int64_t value) {
1635 return [=](
Model* model) {
1648 absl::Span<const Literal> enforcement_literals, IntegerLiteral
i) {
1649 return [=](
Model* model) {
1650 auto* sat_solver = model->GetOrCreate<SatSolver>();
1652 if (
i.bound <= integer_trail->LowerBound(
i.var)) {
1654 }
else if (
i.bound > integer_trail->UpperBound(
i.var)) {
1656 std::vector<Literal> clause;
1657 for (
const Literal literal : enforcement_literals) {
1658 clause.push_back(literal.Negated());
1660 sat_solver->AddClauseDuringSearch(clause);
1665 std::vector<Literal> clause{encoder->GetOrCreateAssociatedLiteral(
i)};
1666 for (
const Literal literal : enforcement_literals) {
1667 clause.push_back(literal.Negated());
1669 sat_solver->AddClauseDuringSearch(clause);
1677 int64_t lb, int64_t ub) {
1678 return [=](
Model* model) {
1683 v, IntegerValue(lb))));
1698 IntegerVariable var) {
1699 return [=](
Model* model) {
1701 if (!encoder->VariableIsFullyEncoded(var)) {
1702 encoder->FullyEncodeVariable(var);
void ClearAndResize(IntegerType size)
int NumPropagators() const
Returns the number of registered propagators.
void WatchUpperBound(AffineExpression e, int id)
bool Propagate(Trail *trail) final
void SetUntilNextBacktrack(bool *is_in_dive)
void RegisterReversibleInt(int id, int *rev)
void WatchAffineExpression(AffineExpression e, int id)
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
void WatchLowerBound(IntegerValue, int)
void WatchLiteral(Literal l, int id, int watch_index=-1)
void WatchIntegerVariable(IntegerValue, int)
void WatchUpperBound(IntegerVariable var, int id, int watch_index=-1)
~GenericLiteralWatcher() final=default
void Untrail(const Trail &trail, int literal_trail_index) final
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
void RegisterLevelZeroModifiedVariablesCallback(const std::function< void(const std::vector< IntegerVariable > &)> cb)
void SetStopPropagationCallback(std::function< bool()> callback)
void WatchUpperBound(IntegerValue, int)
void SetPropagatorPriority(int id, int priority)
void WatchIntegerVariable(IntegerVariable i, int id, int watch_index=-1)
void RegisterReversibleClass(int id, ReversibleInterface *rev)
void ReserveSpaceForNumVariables(int num_vars)
Memory optimization: you can call this before registering watchers.
int Register(PropagatorInterface *propagator)
Registers a propagator and returns its unique ids.
GenericLiteralWatcher & operator=(const GenericLiteralWatcher &)=delete
void CallOnNextPropagate(int id)
GenericLiteralWatcher(const GenericLiteralWatcher &)=delete
This type is neither copyable nor movable.
void CallAgainDuringThisPropagation()
GenericLiteralWatcher(Model *model)
void AlwaysCallAtLevelZero(int id)
const std::vector< ValueLiteralPair > & FullDomainEncoding(IntegerVariable var) const
IntegerEncoder & operator=(const IntegerEncoder &)=delete
std::pair< IntegerLiteral, IntegerLiteral > Canonicalize(IntegerLiteral i_lit) const
void AssociateToIntegerLiteral(Literal literal, IntegerLiteral i_lit)
const InlinedIntegerValueVector & GetEqualityLiterals(Literal lit) const
IntegerVariable GetLiteralView(Literal lit) const
void AddAllImplicationsBetweenAssociatedLiterals()
Literal GetFalseLiteral()
void FullyEncodeVariable(IntegerVariable var)
IntegerEncoder(const IntegerEncoder &)=delete
This type is neither copyable nor movable.
IntegerEncoder(Model *model)
Literal GetTrueLiteral()
Gets the literal always set to true, make it if it does not exist.
bool VariableIsFullyEncoded(IntegerVariable var) const
bool IsFixedOrHasAssociatedLiteral(IntegerLiteral i_lit) const
const std::vector< ValueLiteralPair > & PartialDomainEncoding(IntegerVariable var) const
LiteralIndex GetAssociatedEqualityLiteral(IntegerVariable var, IntegerValue value) const
const InlinedIntegerLiteralVector & GetIntegerLiterals(Literal lit) const
Returns the IntegerLiterals that were associated with the given Literal.
LiteralIndex SearchForLiteralAtOrBefore(IntegerLiteral i_lit, IntegerValue *bound) const
void ReserveSpaceForNumVariables(int num_vars)
Memory optimization: you can call this before encoding variables.
Literal GetOrCreateAssociatedLiteral(IntegerLiteral i_lit)
void AssociateToIntegerEqualValue(Literal literal, IntegerVariable var, IntegerValue value)
ABSL_MUST_USE_RESULT bool LiteralOrNegationHasView(Literal lit, IntegerVariable *view=nullptr, bool *view_is_direct=nullptr) const
const std::vector< IntegerVariable > & GetAllAssociatedVariables(Literal lit) const
std::vector< ValueLiteralPair > PartialGreaterThanEncoding(IntegerVariable var) const
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
bool UpdateEncodingOnInitialDomainChange(IntegerVariable var, Domain domain)
void DisableImplicationBetweenLiteral()
Literal GetOrCreateLiteralAssociatedToEquality(IntegerVariable var, IntegerValue value)
void NotifyThatPropagationWasAborted()
ABSL_MUST_USE_RESULT bool ConditionalEnqueue(Literal lit, IntegerLiteral i_lit, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason)
absl::Span< const Literal > Reason(const Trail &trail, int trail_index, int64_t conflict_id) const final
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
void RemoveLevelZeroBounds(std::vector< IntegerLiteral > *reason) const
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
int FindTrailIndexOfVarBefore(IntegerVariable var, int threshold) const
bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const
Returns true if the variable lower bound is still the one from level zero.
IntegerTrail & operator=(const IntegerTrail &)=delete
int NumConstantVariables() const
int64_t num_enqueues() const
void RegisterWatcher(SparseBitset< IntegerVariable > *p)
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
bool IsFixedAtLevelZero(IntegerVariable var) const
Returns true if the variable is fixed at level 0.
ABSL_MUST_USE_RESULT bool SafeEnqueue(IntegerLiteral i_lit, absl::Span< const IntegerLiteral > integer_reason)
void RelaxLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, std::vector< IntegerLiteral > *reason) const
bool IntegerLiteralIsTrue(IntegerLiteral l) const
Returns the current value (if known) of an IntegerLiteral.
IntegerValue UpperBound(IntegerVariable i) const
void AppendNewBoundsFrom(int base_index, std::vector< IntegerLiteral > *output) const
IntegerValue FixedValue(IntegerVariable i) const
Checks that the variable is fixed and returns its value.
bool IntegerLiteralIsFalse(IntegerLiteral l) const
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
bool HasPendingRootLevelDeduction() const
Return true if we can fix new fact at level zero.
IntegerVariable AddIntegerVariable()
void AddAllGreaterThanConstantReason(absl::Span< AffineExpression > exprs, IntegerValue target_min, std::vector< int > *indices) const
void RegisterReversibleClass(ReversibleInterface *rev)
bool ReportConflict(absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
int64_t timestamp() const
IntegerTrail(Model *model)
void AppendRelaxedLinearReason(IntegerValue slack, absl::Span< const IntegerValue > coeffs, absl::Span< const IntegerVariable > vars, std::vector< IntegerLiteral > *reason) const
Same as above but take in IntegerVariables instead of IntegerLiterals.
IntegerTrail(const IntegerTrail &)=delete
This type is neither copyable nor movable.
bool ReportConflict(absl::Span< const IntegerLiteral > integer_reason)
ABSL_MUST_USE_RESULT bool EnqueueWithLazyReason(IntegerLiteral i_lit, int id, IntegerValue propagation_slack, LazyReasonInterface *explainer)
Lazy reason API.
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
bool InPropagationLoop() const
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
bool IsFixed(IntegerVariable i) const
Checks if the variable is fixed.
IntegerVariable NumIntegerVariables() const
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason, int trail_index_with_same_reason)
IntegerValue ConditionalLowerBound(Literal l, IntegerVariable i) const
IntegerVariable NextVariableToBranchOnInPropagationLoop() const
IntegerValue ConditionalUpperBound(Literal l, IntegerVariable i) const
Returns the current upper bound assuming the literal is true.
const IntegerValue * LowerBoundsData() const
void RegisterDebugChecker(std::function< bool(absl::Span< const Literal > clause, absl::Span< const IntegerLiteral > integers)> checker)
int64_t num_level_zero_enqueues() const
Same as num_enqueues but only count the level zero changes.
ABSL_MUST_USE_RESULT bool RootLevelEnqueue(IntegerLiteral i_lit)
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
void MergeReasonInto(absl::Span< const IntegerLiteral > literals, std::vector< Literal > *output) const
void EnqueueLiteral(Literal literal, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
const Domain & InitialVariableDomain(IntegerVariable var) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Returns globally valid lower/upper bound on the given integer variable.
void Untrail(const Trail &trail, int literal_trail_index) final
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit)
IntegerVariable FirstUnassignedVariable() const
void ReserveSpaceForNumVariables(int num_vars)
bool Propagate(Trail *trail) final
IntegerVariable GetOrCreateConstantIntegerVariable(IntegerValue value)
std::vector< Literal > ReasonFor(IntegerLiteral literal) const
bool CurrentBranchHadAnIncompletePropagation()
virtual ~LazyReasonInterface()=default
LazyReasonInterface()=default
virtual void Explain(int id, IntegerValue propagation_slack, IntegerVariable var_to_explain, int trail_index, std::vector< Literal > *literals_reason, std::vector< int > *trail_indices_reason)=0
LiteralIndex Index() const
Base class for CP like propagators.
virtual ~PropagatorInterface()=default
virtual bool IncrementalPropagate(const std::vector< int > &)
virtual bool Propagate()=0
PropagatorInterface()=default
RevIntRepository(Model *model)
RevIntegerValueRepository(Model *model)
SatPropagator(const std::string &name)
void AddPropagator(SatPropagator *propagator)
void push_back(const value_type &val)
std::function< std::vector< ValueLiteralPair >(Model *)> FullyEncodeVariable(IntegerVariable var)
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::function< void(Model *)> Equality(IntegerVariable v, int64_t value)
Fix v to a given value.
bool operator==(const BoolArgumentProto &lhs, const BoolArgumentProto &rhs)
const LiteralIndex kNoLiteralIndex(-1)
std::function< int64_t(const Model &)> LowerBound(IntegerVariable v)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64_t ub)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
const IntegerVariable kNoIntegerVariable(-1)
absl::InlinedVector< std::pair< IntegerVariable, IntegerValue >, 2 > InlinedIntegerValueVector
std::function< void(Model *)> Implication(absl::Span< const Literal > enforcement_literals, IntegerLiteral i)
std::function< IntegerVariable(Model *)> ConstantIntegerVariable(int64_t value)
std::function< int64_t(const Model &)> Value(IntegerVariable v)
This checks that the variable is fixed.
std::function< int64_t(const Model &)> UpperBound(IntegerVariable v)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64_t lb, int64_t ub)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64_t lb)
absl::InlinedVector< IntegerLiteral, 2 > InlinedIntegerLiteralVector
std::function< void(Model *)> ImpliesInInterval(Literal in_interval, IntegerVariable v, int64_t lb, int64_t ub)
in_interval => v in [lb, ub].
bool VariableIsPositive(IntegerVariable i)
IntegerVariable CreateNewIntegerVariableFromLiteral(Literal lit, Model *model)
In SWIG mode, we don't want anything besides these top-level includes.
#define DEFINE_STRONG_INDEX_TYPE(index_type_name)
IntegerValue ValueAt(IntegerValue var_value) const
Returns the value of this affine expression given its variable value.
std::vector< IntegerLiteral > integer_literal_to_fix
std::vector< Literal > literal_to_fix
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral TrueLiteral()
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
void SimpleCanonicalization()
bool operator==(const LiteralValueValue &rhs) const
Used for testing.
std::string DebugString() const