#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)

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.

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 195 of file encoding.cc.

◆ AssumptionIs()

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

GetAssumption() might need to create new literals.

Definition at line 229 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 41 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 254 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 61 of file encoding.cc.

◆ GetAssumption()

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

Definition at line 235 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 250 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 157 of file encoding.cc.

◆ IncreaseWeightLb()

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

Definition at line 245 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 99 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 79 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 142 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 126 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 50 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 173 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 209 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

Public Member Functions

Static Public Member Functions

Detailed Description

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()