# 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: Arguments: Fix the right-side variables with indices >= to the given upper_bound to false. |

`child_a` | Return type: |

`child_b` | Return type: |

`current_ub` | Return type: |

`depth` | Return type: |

`EncodingNode` | |

`EncodingNode` | Return type: Arguments: Constructs a EncodingNode of size one, just formed by the given literal. |

`GreaterThan` | Return type: Arguments: Returns a literal with the meaning 'this node number is > i'. The given i must be in [lb_, current_ub). |

`IncreaseCurrentUB` | Return type: Arguments: Creates a new literals and increases current_ub. Returns false if we were already at the upper bound for this node. |

`InitializeFullNode` | Return type: Arguments: 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: Arguments: 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: |

`literal` | Return type: Arguments: |

`Reduce` | Return type: Arguments: 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: Arguments: |

`size` | Return type: Accessors to size() and literals in [lb, current_ub). |

`ub` | Return type: |

`weight` | Return type: |