Stay organized with collections
Save and categorize content based on your preferences.
C++ Reference: class DomainDeductions
Note: This documentation is automatically generated.
If for each literal of a clause, we can infer a domain on an integer
variable, then we know that this variable domain is included in the union of
such infered domains.
This allows to propagate "element" like constraints encoded as enforced
linear relations, and other more general reasoning.
TODO(user): Also use these "deductions" in the solver directly. This is done
in good MIP solvers, and we should exploit them more.
TODO(user): Also propagate implicit clauses (lit, not(lit)). Maybe merge
that with probing code? it might be costly to store all deduction done by
probing though, but I think this is what MIP solver do.
Arguments: int literal_ref, int var, Domain domain
Adds the fact that enforcement => var \in domain.
Important: No need to store any deductions where the domain is a superset
of the current variable domain.
[[["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."],[[["\u003cp\u003eThe \u003ccode\u003eDomainDeductions\u003c/code\u003e class in C++ infers and stores domain restrictions on integer variables based on clause analysis.\u003c/p\u003e\n"],["\u003cp\u003eIt leverages enforced linear relations and other reasoning techniques to deduce these domain restrictions.\u003c/p\u003e\n"],["\u003cp\u003eDomain deductions can be added and retrieved using methods like \u003ccode\u003eAddDeduction\u003c/code\u003e and \u003ccode\u003eImpliedDomain\u003c/code\u003e.\u003c/p\u003e\n"],["\u003cp\u003eFuture improvements include directly using deductions in the solver and propagating implicit clauses.\u003c/p\u003e\n"]]],["The `DomainDeductions` class infers variable domains from clause literals. It allows propagating constraints like \"element\" and other reasoning. Key actions include: `AddDeduction`, which adds the fact that a literal implies a variable is within a domain; `ImpliedDomain`, which returns the deduced domain of a variable given a true literal, or all values if no information is found; `MarkProcessingAsDoneForNow`, to allow faster clause processing in future, and `NumDeductions` to know how many deductions were stored. It is meant to allow better inferences in the solver.\n"],null,[]]
