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."],[[["Blocked clauses are clauses that can be safely removed from a problem because they are implied by other clauses."],["This simplification technique is based on the concept of a literal \"blocking\" a clause if negating the literal and resolving always yields a trivial result."],["Blocked clause elimination can improve solver performance by reducing the number of clauses to consider and allowing for efficient postsolve adjustments."],["A current limitation of this implementation within CP-SAT is its exclusive applicability to clauses, excluding the integer component."]]],["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"]]
