Stay organized with collections
Save and categorize content based on your preferences.
C++ Reference: class BlockedClauseSimplifier
Note: This documentation is automatically generated.
A clause c is "blocked" by a literal l if all clauses containing the
negation of l resolve to trivial clause with c. Blocked clause can be
simply removed from the problem. At postsolve, if a blocked clause is not
satisfied, then l can simply be set to true without breaking any of the
clause containing not(l).
See the paper "Blocked Clause Elimination", Matti Jarvisalo, Armin Biere,
and Marijn Heule.
TODO(user): This requires that l only appear in clauses and not in the
integer part of CP-SAT.
[[["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\u003eBlocked clauses are clauses that can be safely removed from a problem because they are implied by other clauses.\u003c/p\u003e\n"],["\u003cp\u003eThis simplification technique is based on the concept of a literal "blocking" a clause if negating the literal and resolving always yields a trivial result.\u003c/p\u003e\n"],["\u003cp\u003eBlocked clause elimination can improve solver performance by reducing the number of clauses to consider and allowing for efficient postsolve adjustments.\u003c/p\u003e\n"],["\u003cp\u003eA current limitation of this implementation within CP-SAT is its exclusive applicability to clauses, excluding the integer component.\u003c/p\u003e\n"]]],["The `BlockedClauseSimplifier` class in C++ removes \"blocked\" clauses from a problem. A clause is blocked by a literal if all clauses containing the negation of that literal resolve to a trivial clause with it. These clauses can be removed, and if unsatisfied during postsolve, the literal can be set to true. The `BlockedClauseSimplifier` constructor takes a `Model* model`. `DoOneRound` executes one round of simplification, optionally logging information. This simplification technique is based on the \"Blocked Clause Elimination\" paper.\n"],null,["# BlockedClauseSimplifier\n\nC++ Reference: class BlockedClauseSimplifier\n============================================\n\n\nNote: This documentation is automatically generated.\nA clause c is \"blocked\" by a literal l if all clauses containing the negation of l resolve to trivial clause with c. Blocked clause can be simply removed from the problem. At postsolve, if a blocked clause is not satisfied, then l can simply be set to true without breaking any of the clause containing not(l). \n\nSee the paper \"Blocked Clause Elimination\", Matti Jarvisalo, Armin Biere, and Marijn Heule. \n\nTODO(user): This requires that l only appear in clauses and not in the integer part of CP-SAT.\n\n| Method ||\n|---------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------|\n| [`BlockedClauseSimplifier`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L260) | Return type: `explicit ` Arguments: `Model* model` \u003cbr /\u003e |\n| [`DoOneRound`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/sat_inprocessing.h#L267) | Return type: `void ` Arguments: `bool log_info` \u003cbr /\u003e |"]]
