14 #ifndef OR_TOOLS_SAT_INTEGER_H_
15 #define OR_TOOLS_SAT_INTEGER_H_
26 #include "absl/container/flat_hash_map.h"
27 #include "absl/container/inlined_vector.h"
28 #include "absl/strings/str_cat.h"
29 #include "absl/types/span.h"
70 const double kInfinity = std::numeric_limits<double>::infinity();
73 return static_cast<double>(
value.value());
76 template <
class IntType>
78 return IntType(std::abs(t.value()));
81 inline IntegerValue
CeilRatio(IntegerValue dividend,
82 IntegerValue positive_divisor) {
84 const IntegerValue result = dividend / positive_divisor;
85 const IntegerValue adjust =
86 static_cast<IntegerValue
>(result * positive_divisor < dividend);
87 return result + adjust;
91 IntegerValue positive_divisor) {
93 const IntegerValue result = dividend / positive_divisor;
94 const IntegerValue adjust =
95 static_cast<IntegerValue
>(result * positive_divisor > dividend);
96 return result - adjust;
103 IntegerValue positive_divisor) {
105 const IntegerValue m = dividend % positive_divisor;
106 return m < 0 ? m + positive_divisor : m;
115 *result = IntegerValue(add);
127 return IntegerVariable(i.value() ^ 1);
131 return (i.value() & 1) == 0;
135 return IntegerVariable(i.value() & (~1));
141 return PositiveOnlyIndex(
var.value() / 2);
146 const std::vector<IntegerVariable>& vars);
184 ? absl::StrCat(
"I",
var.value() / 2,
">=",
bound.value())
185 : absl::StrCat(
"I",
var.value() / 2,
"<=", -
bound.value());
190 IntegerValue
bound = IntegerValue(0);
241 IntegerValue
coeff = IntegerValue(0);
281 num_created_variables_(0) {}
284 VLOG(1) <<
"#variables created = " << num_created_variables_;
333 IntegerVariable
var)
const;
377 IntegerValue
value)
const;
391 if (lit.
Index() >= reverse_encoding_.
size()) {
392 return empty_integer_literal_vector_;
394 return reverse_encoding_[lit.
Index()];
401 if (lit.
Index() >= full_reverse_encoding_.
size()) {
402 return empty_integer_literal_vector_;
404 return full_reverse_encoding_[lit.
Index()];
410 return newly_fixed_integer_literals_;
413 newly_fixed_integer_literals_.clear();
422 return literal_view_[lit.
Index()];
434 IntegerValue*
bound)
const;
442 literal_index_true_ = literal_true.
Index();
445 return Literal(literal_index_true_);
453 IntegerVariable
var)
const {
454 if (
var >= encoding_by_var_.size()) {
455 return std::map<IntegerValue, Literal>();
457 return encoding_by_var_[
var];
473 void AddImplications(
const std::map<IntegerValue, Literal>& map,
474 std::map<IntegerValue, Literal>::const_iterator it,
480 bool add_implications_ =
true;
481 int64 num_created_variables_ = 0;
497 full_reverse_encoding_;
498 std::vector<IntegerLiteral> newly_fixed_integer_literals_;
510 absl::flat_hash_map<std::pair<PositiveOnlyIndex, IntegerValue>,
Literal>
511 equality_to_associated_literal_;
525 std::vector<IntegerValue> tmp_values_;
540 parameters_(*
model->GetOrCreate<SatParameters>()) {
550 void Untrail(const
Trail& trail,
int literal_trail_index) final;
552 int trail_index) const final;
559 return IntegerVariable(vars_.
size());
575 IntegerValue upper_bound);
619 const LiteralIndex is_ignored_literal = is_ignored_literals_[i];
625 return Literal(is_ignored_literals_[i]);
634 is_ignored_literals_[i] == is_considered.
NegatedIndex());
640 IntegerValue
LowerBound(IntegerVariable i)
const;
641 IntegerValue
UpperBound(IntegerVariable i)
const;
644 bool IsFixed(IntegerVariable i)
const;
688 absl::Span<const IntegerValue> coeffs,
689 std::vector<IntegerLiteral>* reason)
const;
693 absl::Span<const IntegerValue> coeffs,
694 absl::Span<const IntegerVariable> vars,
695 std::vector<IntegerLiteral>* reason)
const;
699 absl::Span<const IntegerValue> coeffs,
700 std::vector<int>* trail_indices)
const;
723 ABSL_MUST_USE_RESULT
bool Enqueue(
725 absl::Span<const IntegerLiteral> integer_reason);
734 ABSL_MUST_USE_RESULT
bool Enqueue(
736 absl::Span<const IntegerLiteral> integer_reason,
737 int trail_index_with_same_reason);
752 std::vector<Literal>* literals, std::vector<int>* dependencies)>;
759 absl::Span<const IntegerLiteral> integer_reason);
769 std::vector<Literal>* output)
const;
788 watchers_.push_back(p);
794 absl::Span<const IntegerLiteral> integer_reason) {
795 DCHECK(ReasonIsValid(literal_reason, integer_reason));
797 conflict->assign(literal_reason.begin(), literal_reason.end());
802 DCHECK(ReasonIsValid({}, integer_reason));
811 return vars_[
var].current_trail_index < vars_.
size();
817 reversible_classes_.push_back(rev);
820 int Index()
const {
return integer_trail_.size(); }
848 return !literal_to_fix_.empty() || !integer_literal_to_fix_.empty();
854 bool ReasonIsValid(absl::Span<const Literal> literal_reason,
855 absl::Span<const IntegerLiteral> integer_reason);
860 std::vector<Literal>* InitializeConflict(
862 absl::Span<const Literal> literals_reason,
863 absl::Span<const IntegerLiteral> bounds_reason);
866 ABSL_MUST_USE_RESULT
bool EnqueueInternal(
868 absl::Span<const Literal> literal_reason,
869 absl::Span<const IntegerLiteral> integer_reason,
870 int trail_index_with_same_reason);
874 absl::Span<const Literal> literal_reason,
875 absl::Span<const IntegerLiteral> integer_reason);
880 ABSL_MUST_USE_RESULT
bool EnqueueAssociatedIntegerLiteral(
884 void MergeReasonIntoInternal(std::vector<Literal>* output)
const;
889 int FindLowestTrailIndexThatExplainBound(
IntegerLiteral i_lit)
const;
894 void ComputeLazyReasonIfNeeded(
int trail_index)
const;
901 absl::Span<const int> Dependencies(
int trail_index)
const;
907 void AppendLiteralsReason(
int trail_index,
908 std::vector<Literal>* output)
const;
911 std::string DebugString();
916 IntegerValue current_bound;
919 int current_trail_index;
929 mutable int var_trail_index_cache_threshold_ = 0;
934 absl::flat_hash_map<IntegerValue, IntegerVariable> constant_map_;
941 int32 prev_trail_index;
948 std::vector<TrailEntry> integer_trail_;
949 std::vector<LazyReasonFunction> lazy_reasons_;
953 std::vector<int> integer_search_levels_;
960 std::vector<int> reason_decision_levels_;
961 std::vector<int> literals_reason_starts_;
962 std::vector<int> bounds_reason_starts_;
963 std::vector<Literal> literals_reason_buffer_;
968 std::vector<IntegerLiteral> bounds_reason_buffer_;
969 mutable std::vector<int> trail_index_reason_buffer_;
972 mutable std::vector<Literal> lazy_reason_literals_;
973 mutable std::vector<int> lazy_reason_trail_indices_;
984 RevMap<absl::flat_hash_map<IntegerVariable, int>>
985 var_to_current_lb_interval_index_;
988 mutable bool has_dependency_ =
false;
989 mutable std::vector<int> tmp_queue_;
990 mutable std::vector<IntegerVariable> tmp_to_clear_;
992 tmp_var_to_trail_index_in_queue_;
993 mutable SparseBitset<BooleanVariable> added_variables_;
1000 std::vector<Literal> literal_to_fix_;
1001 std::vector<IntegerLiteral> integer_literal_to_fix_;
1004 struct RelaxHeapEntry {
1008 bool operator<(
const RelaxHeapEntry& o)
const {
return index < o.index; }
1010 mutable std::vector<RelaxHeapEntry> relax_heap_;
1011 mutable std::vector<int> tmp_indices_;
1014 mutable SparseBitset<IntegerVariable> tmp_marked_;
1020 std::vector<int> boolean_trail_index_to_integer_one_;
1024 int first_level_without_full_propagation_ = -1;
1026 int64 num_enqueues_ = 0;
1027 int64 num_untrails_ = 0;
1028 int64 num_level_zero_enqueues_ = 0;
1029 mutable int64 num_decisions_to_break_loop_ = 0;
1031 std::vector<SparseBitset<IntegerVariable>*> watchers_;
1032 std::vector<ReversibleInterface*> reversible_classes_;
1034 IntegerDomains* domains_;
1035 IntegerEncoder* encoder_;
1037 const SatParameters& parameters_;
1100 void Untrail(
const Trail& trail,
int literal_trail_index)
final;
1186 const std::function<
void(
const std::vector<IntegerVariable>&)> cb) {
1187 level_zero_modified_variable_callback_.push_back(cb);
1198 void UpdateCallingNeeds(
Trail* trail);
1208 return id == o.id && watch_index == o.watch_index;
1213 std::vector<PropagatorInterface*> watchers_;
1214 SparseBitset<IntegerVariable> modified_vars_;
1218 std::vector<std::deque<int>> queue_by_priority_;
1219 std::vector<bool> in_queue_;
1222 DEFINE_INT_TYPE(IdType,
int32);
1223 std::vector<int> id_to_level_at_last_call_;
1224 RevVector<IdType, int> id_to_greatest_common_level_since_last_call_;
1225 std::vector<std::vector<ReversibleInterface*>> id_to_reversible_classes_;
1226 std::vector<std::vector<int*>> id_to_reversible_ints_;
1227 std::vector<std::vector<int>> id_to_watch_indices_;
1228 std::vector<int> id_to_priority_;
1229 std::vector<int> id_to_idempotence_;
1232 std::vector<int> propagator_ids_to_call_at_level_zero_;
1237 std::vector<std::function<void(
const std::vector<IntegerVariable>&)>>
1238 level_zero_modified_variable_callback_;
1248 IntegerValue
bound) {
1254 IntegerValue
bound) {
1269 IntegerValue
bound)
const {
1284 return vars_[i].current_bound;
1292 return vars_[i].current_bound == -vars_[
NegationOf(i)].current_bound;
1314 IntegerVariable i)
const {
1319 IntegerVariable i)
const {
1334 IntegerVariable
var)
const {
1335 return integer_trail_[
var.value()].bound;
1339 IntegerVariable
var)
const {
1344 return integer_trail_[
var.value()].bound ==
1350 if (l.
Index() >= literal_to_watcher_.
size()) {
1351 literal_to_watcher_.
resize(l.
Index().value() + 1);
1359 if (
var.value() >= var_to_watcher_.
size()) {
1360 var_to_watcher_.
resize(
var.value() + 1);
1367 const WatchData data = {id, watch_index};
1368 if (!var_to_watcher_[
var].empty() && var_to_watcher_[
var].back() == data) {
1405 ->GetOrCreateConstantIntegerVariable(IntegerValue(
value));
1414 IntegerValue(lb), IntegerValue(ub));
1434 IntegerVariable
var;
1436 if (assignment.LiteralIsTrue(lit)) {
1438 }
else if (assignment.LiteralIsFalse(lit)) {
1444 encoder->AssociateToIntegerEqualValue(lit,
var, IntegerValue(1));
1482 std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1484 VLOG(1) <<
"Model trivially infeasible, variable " << v
1486 <<
" and GreaterOrEqual() was called with a lower bound of "
1496 std::vector<Literal>(), std::vector<IntegerLiteral>())) {
1498 LOG(
WARNING) <<
"Model trivially infeasible, variable " << v
1500 <<
" and LowerOrEqual() was called with an upper bound of "
1521 const std::vector<Literal>& enforcement_literals,
IntegerLiteral i) {
1528 std::vector<Literal> clause;
1555 v, IntegerValue(lb))));
1569 inline std::function<std::vector<IntegerEncoder::ValueLiteralPair>(Model*)>
1585 std::function<void(Model*)>
1591 #endif // OR_TOOLS_SAT_INTEGER_H_