14#ifndef OR_TOOLS_SAT_SOLUTION_CRUSH_H_
15#define OR_TOOLS_SAT_SOLUTION_CRUSH_H_
23#include "absl/container/flat_hash_map.h"
24#include "absl/container/inlined_vector.h"
25#include "absl/types/span.h"
65 absl::Span<const int64_t>
GetVarValues()
const {
return var_values_; }
71 const absl::flat_hash_map<int, int64_t>&
solution);
88 int var, absl::Span<
const std::pair<int, int64_t>> linear,
94 absl::Span<const int64_t> coeffs,
111 int var, int64_t value, absl::Span<
const std::pair<int, int64_t>> linear,
118 int literal,
bool value, absl::Span<
const std::pair<int, int64_t>> linear,
136 int64_t value_if_true, int64_t value_if_false);
166 int ref, int64_t min_value, int64_t max_value,
167 absl::Span<
const std::pair<int, Domain>> dominating_refs);
175 absl::Span<
const std::unique_ptr<SparsePermutation>> generators);
183 absl::Span<const int> vars,
184 absl::Span<const int64_t> coeffs,
192 int64_t min_level, int64_t max_level,
193 absl::Span<const int> level_vars,
201 int active_i,
int active_j);
210 int prod_var, int64_t default_div_value,
211 int64_t default_prod_value);
222 absl::Span<const int> prod_vars);
230 absl::Span<const int> enforcement_lits);
252 absl::Span<const StateVar> state_vars,
253 absl::Span<const TransitionVar> transition_vars);
269 absl::Span<const int> existing_row_lits,
270 absl::Span<const TableRowLiteral> new_row_lits);
294 const CpModelProto& model, absl::Span<const int> x_intervals,
295 absl::Span<const int> y_intervals,
296 absl::Span<const BoxInAreaLiteral> box_in_area_lits);
299 bool HasValue(
int var)
const {
return var_has_value_[var]; }
301 int64_t GetVarValue(
int var)
const {
return var_values_[var]; }
303 bool GetLiteralValue(
int lit)
const {
305 return RefIsPositive(lit) ? GetVarValue(var) : !GetVarValue(var);
308 std::optional<int64_t> GetRefValue(
int ref)
const {
310 if (!HasValue(var))
return std::nullopt;
311 return RefIsPositive(ref) ? GetVarValue(var) : -GetVarValue(var);
314 std::optional<int64_t> GetExpressionValue(
315 const LinearExpressionProto& expr)
const {
316 int64_t result = expr.offset();
317 for (
int i = 0;
i < expr.vars().size(); ++
i) {
318 if (expr.coeffs(
i) == 0)
continue;
319 if (!HasValue(expr.vars(
i)))
return std::nullopt;
320 result += expr.coeffs(
i) * GetVarValue(expr.vars(
i));
325 void SetVarValue(
int var, int64_t value) {
326 var_has_value_[var] =
true;
327 var_values_[var] = value;
330 void SetLiteralValue(
int lit,
bool value) {
334 void SetRefValue(
int ref,
int value) {
338 void PermuteVariables(
const SparsePermutation& permutation);
340 bool solution_is_loaded_ =
false;
341 std::vector<bool> var_has_value_;
343 std::vector<int64_t> var_values_;
void LoadSolution(int num_vars, const absl::flat_hash_map< int, int64_t > &solution)
void SetIntModExpandedVars(const ConstraintProto &ct, int div_var, int prod_var, int64_t default_div_value, int64_t default_prod_value)
void SetLinearWithComplexDomainExpandedVars(const LinearConstraintProto &linear, absl::Span< const int > bucket_lits)
void StoreSolutionAsHint(CpModelProto &model) const
Stores the solution as a hint in the given model.
absl::Span< const int64_t > GetVarValues() const
Visible for testing.
void SetLinMaxExpandedVars(const LinearArgumentProto &lin_max, absl::Span< const int > enforcement_lits)
void SetVarToConjunction(int var, absl::Span< const int > conjunction)
void SetReservoirCircuitVars(const ReservoirConstraintProto &reservoir, int64_t min_level, int64_t max_level, absl::Span< const int > level_vars, const CircuitConstraintProto &circuit)
void SetVarToValueIf(int var, int64_t value, int condition_lit)
Sets the value of var to value if the value of condition_lit is true.
void Resize(int new_size)
void AssignVariableToPackingArea(const CompactVectorVector< int, Rectangle > &areas, const CpModelProto &model, absl::Span< const int > x_intervals, absl::Span< const int > y_intervals, absl::Span< const BoxInAreaLiteral > box_in_area_lits)
void SetAutomatonExpandedVars(const AutomatonConstraintProto &automaton, absl::Span< const StateVar > state_vars, absl::Span< const TransitionVar > transition_vars)
SolutionCrush & operator=(SolutionCrush &&)=delete
void SetVarToValueIfLinearConstraintViolated(int var, int64_t value, absl::Span< const std::pair< int, int64_t > > linear, const Domain &domain)
void SetVarToReifiedPrecedenceLiteral(int var, const LinearExpressionProto &time_i, const LinearExpressionProto &time_j, int active_i, int active_j)
void MakeLiteralsEqual(int lit1, int lit2)
void UpdateLiteralsWithDominance(int lit, int dominating_lit)
void SetLiteralToValueIfLinearConstraintViolated(int literal, bool value, absl::Span< const std::pair< int, int64_t > > linear, const Domain &domain)
void UpdateRefsWithDominance(int ref, int64_t min_value, int64_t max_value, absl::Span< const std::pair< int, Domain > > dominating_refs)
SolutionCrush & operator=(const SolutionCrush &)=delete
void SetIntProdExpandedVars(const LinearArgumentProto &int_prod, absl::Span< const int > prod_vars)
void SetVarToLinearExpressionIf(int var, const LinearExpressionProto &expr, int condition_lit)
void MaybeSetLiteralToValueEncoding(int literal, int var, int64_t value)
SolutionCrush(SolutionCrush &&)=delete
void SetOrUpdateVarToDomain(int var, const Domain &domain)
void MaybeUpdateVarWithSymmetriesToValue(int var, bool value, absl::Span< const std::unique_ptr< SparsePermutation > > generators)
void SetVarToLinearExpression(int var, absl::Span< const std::pair< int, int64_t > > linear, int64_t offset=0)
void UpdateLiteralsToFalseIfDifferent(int lit1, int lit2)
void SetLiteralToValueIf(int literal, bool value, int condition_lit)
void SetTableExpandedVars(absl::Span< const int > column_vars, absl::Span< const int > existing_row_lits, absl::Span< const TableRowLiteral > new_row_lits)
void SetVarToConditionalValue(int var, absl::Span< const int > condition_lits, int64_t value_if_true, int64_t value_if_false)
void SetVarToClause(int var, absl::Span< const int > clause)
bool SolutionIsLoaded() const
SolutionCrush(const SolutionCrush &)=delete
SolutionCrush is neither copyable nor movable.
void SetVarToLinearConstraintSolution(std::optional< int > var_index, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t rhs)
bool RefIsPositive(int ref)
In SWIG mode, we don't want anything besides these top-level includes.
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
Represents var = "automaton is in state `state` at time `time`".
std::vector< absl::InlinedVector< int64_t, 2 > > var_values