18#ifndef OR_TOOLS_SAT_ENCODING_H_
19#define OR_TOOLS_SAT_ENCODING_H_
28#include "ortools/sat/boolean_problem.pb.h"
77 int size()
const {
return literals_.size(); }
87 return depth_ > other.depth_ ||
88 (depth_ == other.depth_ && other.for_sorting_ > for_sorting_);
106 Coefficient
weight()
const {
return weight_; }
108 int depth()
const {
return depth_; }
109 int lb()
const {
return lb_; }
111 int ub()
const {
return ub_; }
119 BooleanVariable for_sorting_;
126 std::vector<Literal> literals_;
132#if defined(_M_X64) && defined(_DEBUG)
134static_assert(
sizeof(EncodingNode) == 72,
135 "ERROR_EncodingNode_is_not_well_compacted");
139static_assert(
sizeof(EncodingNode) <= 64,
140 "ERROR_EncodingNode_is_not_well_compacted");
146EncodingNode
LazyMerge(EncodingNode*
a, EncodingNode*
b, SatSolver* solver);
157EncodingNode
FullMerge(Coefficient upper_bound, EncodingNode*
a,
158 EncodingNode*
b, SatSolver* solver);
163 const std::vector<EncodingNode*>& nodes,
165 std::deque<EncodingNode>* repository);
171 std::deque<EncodingNode>* repository);
178 const std::vector<Literal>& literals,
179 const std::vector<Coefficient>& coeffs, Coefficient* offset,
180 std::deque<EncodingNode>* repository);
182 const LinearObjective& objective_proto, Coefficient* offset,
183 std::deque<EncodingNode>* repository);
189 Coefficient upper_bound, Coefficient stratified_lower_bound,
190 Coefficient* lower_bound, std::vector<EncodingNode*>* nodes,
196 const std::vector<Literal>& core);
202 Coefficient upper_bound);
206void ProcessCore(
const std::vector<Literal>& core, Coefficient min_weight,
207 std::deque<EncodingNode>* repository,
208 std::vector<EncodingNode*>* nodes, SatSolver* solver);
#define CHECK_LT(val1, val2)
#define CHECK_GE(val1, val2)
int Reduce(const SatSolver &solver)
bool IncreaseCurrentUB(SatSolver *solver)
EncodingNode * child_b() const
void InitializeLazyNode(EncodingNode *a, EncodingNode *b, SatSolver *solver)
void InitializeFullNode(int n, EncodingNode *a, EncodingNode *b, SatSolver *solver)
Coefficient weight() const
Literal literal(int i) const
void ApplyUpperBound(int64 upper_bound, SatSolver *solver)
EncodingNode * child_a() const
void set_weight(Coefficient w)
Literal GreaterThan(int i) const
bool operator<(const EncodingNode &other) const
Coefficient ComputeCoreMinWeight(const std::vector< EncodingNode * > &nodes, const std::vector< Literal > &core)
EncodingNode * MergeAllNodesWithDeque(Coefficient upper_bound, const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
std::vector< Literal > ReduceNodesAndExtractAssumptions(Coefficient upper_bound, Coefficient stratified_lower_bound, Coefficient *lower_bound, std::vector< EncodingNode * > *nodes, SatSolver *solver)
EncodingNode * LazyMergeAllNodeWithPQ(const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
void IncreaseNodeSize(EncodingNode *node, SatSolver *solver)
EncodingNode LazyMerge(EncodingNode *a, EncodingNode *b, SatSolver *solver)
EncodingNode FullMerge(Coefficient upper_bound, EncodingNode *a, EncodingNode *b, SatSolver *solver)
void ProcessCore(const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver)
Coefficient MaxNodeWeightSmallerThan(const std::vector< EncodingNode * > &nodes, Coefficient upper_bound)
std::vector< EncodingNode * > CreateInitialEncodingNodes(const std::vector< Literal > &literals, const std::vector< Coefficient > &coeffs, Coefficient *offset, std::deque< EncodingNode > *repository)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...