C++ Reference: class EncodingNode

This documentation is automatically generated.

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.
Method
ApplyUpperBound

Return type: void

Arguments: int64 upper_bound, SatSolver* solver

Fix the right-side variables with indices >= to the given upper_bound to false.

child_a

Return type: EncodingNode*

child_b

Return type: EncodingNode*

current_ub

Return type: int

depth

Return type: int

EncodingNode

EncodingNode

Return type: explicit

Arguments: Literal l

Constructs a EncodingNode of size one, just formed by the given literal.

GreaterThan

Return type: Literal

Arguments: int i

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

IncreaseCurrentUB

Return type: bool

Arguments: SatSolver* solver

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

InitializeFullNode

Return type: void

Arguments: 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)

InitializeLazyNode

Return type: void

Arguments: 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.

lb

Return type: int

literal

Return type: Literal

Arguments: int i

Reduce

Return type: int

Arguments: const SatSolver& solver

Removes the left-side literals fixed to 1 and returns the number of literals removed this way. 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.

set_weight

Return type: void

Arguments: Coefficient w

size

Return type: int

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

ub

Return type: int

weight

Return type: Coefficient