operations_research::sat::BoundedVariableElimination Class Reference

#include <sat_inprocessing.h>

Public Member Functions
	BoundedVariableElimination (Model *model)
bool	DoOneRound (bool log_info)

Detailed Description

Definition at line 317 of file sat_inprocessing.h.

Constructor & Destructor Documentation

BoundedVariableElimination()

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

inlineexplicit

Definition at line 319 of file sat_inprocessing.h.

Member Function Documentation

DoOneRound()

bool operations_research::sat::BoundedVariableElimination::DoOneRound

(

bool

log_info

)

We ignore redundant clause. This shouldn't cause any validity issue.

Todo

(user): but we shouldn't keep clauses containing removed literals. It is still valid to do so, but it should be less efficient.

Todo

(user): add a local dtime limit for the corner case where this take too much time. We can adapt the limit depending on how much we want to spend on inprocessing.

Make sure we fix variables first if needed. Note that because new binary clause might appear when we fix variables, we need a loop here.

Todo

(user): we might also find new equivalent variable l => var => l here, but for now we ignore those.

Currently we never re-add top if we just processed it.

Remove all redundant clause containing a removed literal. This avoid to re-introduce a removed literal via conflict learning.

Release some memory.

Definition at line 1156 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