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."],[],["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"]]
