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.

Method
BlockedClauseSimplifier	Return type: explicit Arguments: Model* model
DoOneRound	Return type: void Arguments: bool log_info