operations_research::sat::ContinuousProber Class Reference

#include <integer_search.h>

Public Member Functions
	ContinuousProber (const CpModelProto &model_proto, Model *model)
	The model_proto is just used to construct the lists of variable to probe.
SatSolver::Status	Probe ()

Detailed Description

This class will loop continuously on model variables and try to probe/shave its bounds.

Definition at line 329 of file integer_search.h.

Constructor & Destructor Documentation

ContinuousProber()

operations_research::sat::ContinuousProber::ContinuousProber	(	const CpModelProto &	model_proto,
		Model *	model )

The model_proto is just used to construct the lists of variable to probe.

Build variable lists.

Todo

(user): Ideally, we should scan the internal model. But there can be a large blowup of variables during loading, which slows down the probing part. Using model variables is a good heuristic to select 'impactful' Boolean variables.

Definition at line 1605 of file integer_search.cc.

Member Function Documentation

Probe()

SatSolver::Status operations_research::sat::ContinuousProber::Probe

(

)

Starts or continues probing variables and their bounds. It returns:

• SatSolver::INFEASIBLE if the problem is proven infeasible.
• SatSolver::FEASIBLE when a feasible solution is found
• SatSolver::LIMIT_REACHED if the limit stored in the model is reached Calling Probe() after it has returned FEASIBLE or LIMIT_REACHED will resume probing from its previous state.

Continuous probing procedure.

Todo

(user):

• sort variables before the iteration (statically or dynamically)
• compress clause databases regularly (especially the implication graph)
• better interleaving of the probing and shaving phases
• move the shaving code directly in the probing class
• probe all variables and not just the model ones

Backtrack to level 0 in case we are not there.

Store current statistics to detect an iteration without any improvement.

Probe variable bounds.

Todo

(user): Probe optional variables.

Probe Boolean variables from the model.

Probe clauses of the SAT model.

Probe at_most_ones of the SAT model.

Probe combinations of Booleans variables.

Note

the product is always >= 0.

We use a limit to make sure we do not overflow.

Adjust the active_limit.

Reset all counters.

Update the use_shaving_ parameter.

Todo

(user): Currently, the heuristics is that we alternate shaving and not shaving, unless use_shaving_in_probing_search is false.

Remove fixed Boolean variables.

Remove fixed integer variables.

Definition at line 1661 of file integer_search.cc.

---

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

• ortools/sat/integer_search.h
• ortools/sat/integer_search.cc