Detailed Description

This class represents a number in [0, ub]. The encoding uses ub binary variables x_i with i in [0, ub) where x_i means that the number is > i. It is called an EncodingNode, because it represents one node of the tree used to encode a cardinality constraint.

In practice, not all literals are explicitly created:

Only the literals in [lb, current_ub) are "active" at a given time.
The represented number is known to be >= lb.
It may be greater than current_ub, but the extra literals will be only created lazily. In all our solves, the literal current_ub - 1, will always be assumed to false (i.e. the number will be <= current_ub - 1).
Note that lb may increase and ub decrease as more information is learned about this node by the sat solver.

This is roughly based on the cardinality constraint encoding described in: Bailleux and Yacine Boufkhad, "Efficient CNF Encoding of Boolean Cardinality Constraints", In Proc. of CP 2003, pages 108-122, 2003.

Definition at line 61 of file encoding.h.

#include <encoding.h>

Public Member Functions
	EncodingNode ()=default
void	InitializeFullNode (int n, EncodingNode a, EncodingNode b, SatSolver *solver)
void	InitializeLazyNode (EncodingNode a, EncodingNode b, SatSolver *solver)
void	InitializeLazyCoreNode (Coefficient weight, EncodingNode a, EncodingNode b)
void	InitializeAmoNode (absl::Span< EncodingNode const > nodes, SatSolver solver)
Literal	GreaterThan (int i) const
int	size () const
	Accessors to size() and literals in [lb, current_ub).
Literal	literal (int i) const
bool	operator< (const EncodingNode &other) const
bool	IncreaseCurrentUB (SatSolver *solver)
void	TransformToBoolean (SatSolver *solver)
	Indicate that the node cannot grow further than its current assumption.
Coefficient	Reduce (const SatSolver &solver)
bool	AssumptionIs (Literal other) const
	GetAssumption() might need to create new literals.
Literal	GetAssumption (SatSolver *solver)
bool	HasNoWeight () const
void	IncreaseWeightLb ()
void	ApplyWeightUpperBound (Coefficient gap, SatSolver *solver)
void	set_weight (Coefficient w)
Coefficient	weight () const
void	set_depth (int depth)
int	depth () const
int	lb () const
int	weight_lb () const
int	current_ub () const
int	ub () const
EncodingNode *	child_a () const
EncodingNode *	child_b () const
std::string	DebugString (const VariablesAssignment &assignment) const
	We use the solver to display the current values of the literals.

Static Public Member Functions
static EncodingNode	ConstantNode (Coefficient weight)
static EncodingNode	LiteralNode (Literal l, Coefficient weight)
static EncodingNode	GenericNode (int lb, int ub, std::function< Literal(int x)> create_lit, Coefficient weight)

Constructor & Destructor Documentation

◆ EncodingNode()

operations_research::sat::EncodingNode::EncodingNode ( )

default

Member Function Documentation

◆ ApplyWeightUpperBound()

void operations_research::sat::EncodingNode::ApplyWeightUpperBound	(	Coefficient	gap,
		SatSolver *	solver )

Fix any literal that would cause the weight of this node to go over the gap.

Definition at line 197 of file encoding.cc.

◆ AssumptionIs()

bool operations_research::sat::EncodingNode::AssumptionIs ( Literal other ) const

GetAssumption() might need to create new literals.

Definition at line 231 of file encoding.cc.

◆ child_a()

EncodingNode * operations_research::sat::EncodingNode::child_a ( ) const

inline

Definition at line 153 of file encoding.h.

◆ child_b()

EncodingNode * operations_research::sat::EncodingNode::child_b ( ) const

inline

Definition at line 154 of file encoding.h.

◆ ConstantNode()

EncodingNode operations_research::sat::EncodingNode::ConstantNode ( Coefficient weight )

static

Static creation functions.

The generic version constructs a node with value in [lb, ub]. New literal "<=x" will be constructed using create_lit(x).

Definition at line 43 of file encoding.cc.

◆ current_ub()

int operations_research::sat::EncodingNode::current_ub ( ) const

inline

Definition at line 151 of file encoding.h.

◆ DebugString()

std::string operations_research::sat::EncodingNode::DebugString ( const VariablesAssignment & assignment ) const

We use the solver to display the current values of the literals.

Definition at line 256 of file encoding.cc.

◆ depth()

int operations_research::sat::EncodingNode::depth ( ) const

inline

Definition at line 147 of file encoding.h.

◆ GenericNode()

EncodingNode operations_research::sat::EncodingNode::GenericNode	(	int	lb,
		int	ub,
		std::function< Literal(int x)>	create_lit,
		Coefficient	weight )

static

Todo: (user): Not ideal, we should probably just provide index in the original objective for sorting purpose.

Definition at line 63 of file encoding.cc.

◆ GetAssumption()

Literal operations_research::sat::EncodingNode::GetAssumption ( SatSolver * solver )

Definition at line 237 of file encoding.cc.

◆ GreaterThan()

Literal operations_research::sat::EncodingNode::GreaterThan ( int i ) const

inline

Returns a literal with the meaning 'this node number is > i'. The given i must be in [lb_, current_ub).

Definition at line 97 of file encoding.h.

◆ HasNoWeight()

bool operations_research::sat::EncodingNode::HasNoWeight ( ) const

Definition at line 252 of file encoding.cc.

◆ IncreaseCurrentUB()

bool operations_research::sat::EncodingNode::IncreaseCurrentUB ( SatSolver * solver )

Creates a new literals and increases current_ub. Returns false if we were already at the upper bound for this node.

Definition at line 159 of file encoding.cc.

◆ IncreaseWeightLb()

void operations_research::sat::EncodingNode::IncreaseWeightLb ( )

Definition at line 247 of file encoding.cc.

◆ InitializeAmoNode()

void operations_research::sat::EncodingNode::InitializeAmoNode	(	absl::Span< EncodingNode *const >	nodes,
		SatSolver *	solver )

If we know that all the literals[0] of the given nodes are in "at most one" relationship, we can create a node that is the sum of them with a simple encoding. This does create linking implications.

node_lit => new_lit.

If new_literal is true then one of the lit must be true.

Note: this is not needed for correctness though.

Definition at line 101 of file encoding.cc.

◆ InitializeFullNode()

void operations_research::sat::EncodingNode::InitializeFullNode	(	int	n,
		EncodingNode *	a,
		EncodingNode *	b,
		SatSolver *	solver )

Creates a "full" encoding node on n new variables, the represented number beeing in [lb, ub = lb + n). The variables are added to the given solver with the basic implications linking them: literal(0) >= ... >= literal(n-1)

Definition at line 81 of file encoding.cc.

◆ InitializeLazyCoreNode()

void operations_research::sat::EncodingNode::InitializeLazyCoreNode	(	Coefficient	weight,
		EncodingNode *	a,
		EncodingNode *	b )

Merging the node of the same depth in order seems to help a bit.

Definition at line 144 of file encoding.cc.

◆ InitializeLazyNode()

void operations_research::sat::EncodingNode::InitializeLazyNode	(	EncodingNode *	a,
		EncodingNode *	b,
		SatSolver *	solver )

Creates a "lazy" encoding node representing the sum of a and b. Only one literals will be created by this operation. Note that no clauses linking it with a or b are added by this function.

Merging the node of the same depth in order seems to help a bit.

Definition at line 128 of file encoding.cc.

◆ lb()

int operations_research::sat::EncodingNode::lb ( ) const

inline

Definition at line 149 of file encoding.h.

◆ literal()

Literal operations_research::sat::EncodingNode::literal ( int i ) const

inline

Definition at line 101 of file encoding.h.

◆ LiteralNode()

EncodingNode operations_research::sat::EncodingNode::LiteralNode	(	Literal	l,
		Coefficient	weight )

static

Definition at line 52 of file encoding.cc.

◆ operator<()

bool operations_research::sat::EncodingNode::operator< ( const EncodingNode & other ) const

inline

Sort by decreasing depth first and then by increasing variable index. This is meant to be used by the priority queue in MergeAllNodesWithPQ().

Definition at line 109 of file encoding.h.

◆ Reduce()

Coefficient operations_research::sat::EncodingNode::Reduce ( const SatSolver & solver )

Removes the left-side literals fixed to 1. Note that this increases lb_ and reduces the number of active literals. It also removes any right-side literals fixed to 0. If such a literal exists, ub is updated accordingly.

Return the overall weight increase.

Definition at line 175 of file encoding.cc.

◆ set_depth()

void operations_research::sat::EncodingNode::set_depth ( int depth )

inline

The depth is mainly used as an heuristic to decide which nodes to merge first. See the < operator.

Definition at line 146 of file encoding.h.

◆ set_weight()

void operations_research::sat::EncodingNode::set_weight ( Coefficient w )

inline

Definition at line 138 of file encoding.h.

◆ size()

int operations_research::sat::EncodingNode::size ( ) const

inline

Accessors to size() and literals in [lb, current_ub).

Definition at line 100 of file encoding.h.

◆ TransformToBoolean()

void operations_research::sat::EncodingNode::TransformToBoolean ( SatSolver * solver )

Indicate that the node cannot grow further than its current assumption.

Todo: (user): Avoid creating a Boolean just to fix it!

Definition at line 211 of file encoding.cc.

◆ ub()

int operations_research::sat::EncodingNode::ub ( ) const

inline

Definition at line 152 of file encoding.h.

◆ weight()

Coefficient operations_research::sat::EncodingNode::weight ( ) const

inline

Definition at line 142 of file encoding.h.

◆ weight_lb()

int operations_research::sat::EncodingNode::weight_lb ( ) const

inline

Definition at line 150 of file encoding.h.

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

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

Detailed Description

Public Member Functions

Static Public Member Functions

Constructor & Destructor Documentation

◆ EncodingNode()

Member Function Documentation

◆ ApplyWeightUpperBound()

◆ AssumptionIs()

◆ child_a()

◆ child_b()

◆ ConstantNode()

◆ current_ub()

◆ DebugString()

◆ depth()

◆ GenericNode()

◆ GetAssumption()

◆ GreaterThan()

◆ HasNoWeight()

◆ IncreaseCurrentUB()

◆ IncreaseWeightLb()

◆ InitializeAmoNode()

◆ InitializeFullNode()

◆ InitializeLazyCoreNode()

◆ InitializeLazyNode()

◆ lb()

◆ literal()

◆ LiteralNode()

◆ operator<()

◆ Reduce()

◆ set_depth()

◆ set_weight()

◆ size()

◆ TransformToBoolean()

◆ ub()

◆ weight()

◆ weight_lb()