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.
Except as otherwise noted, the content of this page is licensed under the Creative Commons Attribution 4.0 License, and code samples are licensed under the Apache 2.0 License. For details, see the Google Developers Site Policies. Java is a registered trademark of Oracle and/or its affiliates.
Last updated 2024-08-06 UTC.
[null,null,["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 |"]]
