Fixes Booleans variables to true/false and see what is propagated. This
can:
- Fix some Boolean variables (if we reach a conflict while probing).
- Infer new direct implications. We add them directly to the
BinaryImplicationGraph and they can later be used to detect equivalent
literals, expand at most ones clique, etc...
- Tighten the bounds of integer variables. If we probe the two possible
values of a Boolean (b=0 and b=1), we get for each integer variables two
propagated domain D_0 and D_1. The level zero domain can then be
intersected with D_0 U D_1. This can restrict the lower/upper bounds of a
variable, but it can also create holes in the domain! This will detect
common cases like an integer variable in [0, 10] that actually only take
two values [0] or [10] depending on one Boolean.
Returns false if the problem was proved INFEASIBLE during probing.
TODO(user): For now we process the Boolean in their natural order, this is
not the most efficient.
TODO(user): This might generate a lot of new direct implications. We might
not want to add them directly to the BinaryImplicationGraph and could
instead use them directly to detect equivalent literal like in
ProbeAndFindEquivalentLiteral(). The situation is not clear.
TODO(user): More generally, we might want to register any literal => bound
in the IntegerEncoder. This would allow to remember them and use them in
other part of the solver (cuts, lifting, ...).
TODO(user): Rename to include Integer in the name and distinguish better
from FailedLiteralProbing() below.
[[["Easy to understand","easyToUnderstand","thumb-up"],["Solved my problem","solvedMyProblem","thumb-up"],["Other","otherUp","thumb-up"]],[["Missing the information I need","missingTheInformationINeed","thumb-down"],["Too complicated / too many steps","tooComplicatedTooManySteps","thumb-down"],["Out of date","outOfDate","thumb-down"],["Samples / code issue","samplesCodeIssue","thumb-down"],["Other","otherDown","thumb-down"]],["Last updated 2024-08-06 UTC."],[[["The `Prober` class in C++ is used to analyze Boolean variables and their implications within a constraint programming model."],["It can fix variables, deduce new implications, and tighten the bounds of integer variables based on the propagation of Boolean values."],["Probing helps simplify the model and potentially detect infeasibility early on."],["The class provides methods like `ProbeBooleanVariables` and `ProbeOneVariable` to perform probing on specific variables or the entire model."],["Users can register a callback function to observe the propagation process and inferred literals using `SetPropagationCallback`."]]],["The `Prober` class in C++ facilitates probing Boolean variables to improve problem solving. Key actions include: `ProbeBooleanVariables`, which fixes variables to true/false, infers implications, and tightens integer variable bounds, and it can be called on all variables or a subset. `ProbeOneVariable` probes a single Boolean variable. The `SetPropagationCallback` allows for monitoring each propagation. Statistics are available via `num_new_binary_clauses` and `num_new_literals_fixed`, which are reset when `ProbleBooleanVariables()` is called.\n"]]
