operations_research::sat::BlockedClauseSimplifier Class Reference

#include <sat_inprocessing.h>

Public Member Functions
	BlockedClauseSimplifier (Model *model)
void	DoOneRound (bool log_info)

Detailed Description

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.

Definition at line 274 of file sat_inprocessing.h.

Constructor & Destructor Documentation

BlockedClauseSimplifier()

operations_research::sat::BlockedClauseSimplifier::BlockedClauseSimplifier ( Model * model )

inlineexplicit

Definition at line 276 of file sat_inprocessing.h.

Member Function Documentation

DoOneRound()

void operations_research::sat::BlockedClauseSimplifier::DoOneRound

(

bool

log_info

)

Avoid doing too much work here on large problem.

Note

we still what to empty the queue.

Release some memory.

Definition at line 968 of file sat_inprocessing.cc.

---

The documentation for this class was generated from the following files:

• ortools/sat/sat_inprocessing.h
• ortools/sat/sat_inprocessing.cc