operations_research::sat::ObjectiveEncoder Class Reference

#include <encoding.h>

Public Member Functions
	ObjectiveEncoder (Model *model)
bool	ProcessCore (absl::Span< const Literal > core, Coefficient min_weight, Coefficient gap, std::string *info)
void	AddBaseNode (EncodingNode node)
const std::vector< EncodingNode * > &	nodes () const
std::vector< EncodingNode * > *	mutable_nodes ()

Detailed Description

The class reponsible for processing cores and maintaining a Boolean encoding of the linear objective.

Definition at line 232 of file encoding.h.

Constructor & Destructor Documentation

ObjectiveEncoder()

operations_research::sat::ObjectiveEncoder::ObjectiveEncoder ( Model * model )

inlineexplicit

Definition at line 234 of file encoding.h.

Member Function Documentation

AddBaseNode()

void operations_research::sat::ObjectiveEncoder::AddBaseNode ( EncodingNode node )

inline

Definition at line 245 of file encoding.h.

mutable_nodes()

std::vector< EncodingNode * > * operations_research::sat::ObjectiveEncoder::mutable_nodes ( )

inline

Definition at line 252 of file encoding.h.

nodes()

const std::vector< EncodingNode * > & operations_research::sat::ObjectiveEncoder::nodes ( ) const

inline

Todo

(user): Remove mutable version once refactoring is done.

Definition at line 251 of file encoding.h.

ProcessCore()

bool operations_research::sat::ObjectiveEncoder::ProcessCore	(	absl::Span< const Literal >	core,
		Coefficient	min_weight,
		Coefficient	gap,
		std::string *	info )

Updates the encoding using the given core. The literals in the core must match the order in nodes. Returns false if the model become infeasible.

Backtrack to be able to add new constraints.

Remove from nodes the EncodingNode in the core and put them in to_merge.

Since the nodes appear in order in the core, we can find the relevant "objective" variable efficiently with a simple linear scan in the nodes vector (done with index).

Todo

(user): propagate proper ub first.

We can distinguish the first literal of the node. By not counting its weight in node, and creating a new node for it.

Now keep processing with this new node instead.

Special case if the weight > min_weight. we keep it, but reduce its cost. This is the same "trick" as in WPM1 used to deal with weight. We basically split a clause with a larger weight in two identical clauses, one with weight min_weight that will be merged and one with the remaining weight.

Are the literal in amo relationship?

• If min_weight is large enough, we can infer that.
• If the size is small we can infer this via propagation.

Amongst the node to merge, if many are boolean nodes in an "at most one" relationship, it is super advantageous to exploit it during merging as we can regroup all nodes from an at most one in a single new node with a depth of 1.

Collect "boolean nodes".

For "small" core, with O(n) full propagation, we can discover possible at most ones. This is a bit costly but can significantly reduce the number of Booleans needed and has a good positive impact.

Todo

(user): this node is closed and can be removed from the core.

Unit propagation is not always symmetric.

Todo

(user): If assignment.LiteralIsTrue(bool_nodes[j]) We can minimize the core here by removing bool_nodes[i] from it. Note however that since we already minimized the core, this is unlikely to happen.

Convert.

Same case as above, all the nodes in the core are in a exactly_one.

Extract Amo nodes and set them to nullptr in to_merge.

Create the new node with proper constraints and weight.

Clean-up to_merge.

If all the literal of the core are in at_most_one, the core is actually an exactly_one. We just subtracted the min_cost above. We just have to enqueue a constant node with min_weight for the rest of the code to work.

Tricky: We need to enforce an upper bound of 1 on the nodes.

The negation of the literal in the core are in exactly one.

Todo

(user): If we infered the exactly one from the binary implication graph, there is no need to add the amo since it is already there.

Definition at line 586 of file encoding.cc.

---

The documentation for this class was generated from the following files:

• ortools/sat/encoding.h
• ortools/sat/encoding.cc