operations_research::sat::Prober Class Reference

#include <probing.h>

Public Member Functions
	Prober (Model *model)
bool	ProbeBooleanVariables (double deterministic_time_limit)
bool	ProbeBooleanVariables (double deterministic_time_limit, absl::Span< const BooleanVariable > bool_vars)
bool	ProbeOneVariable (BooleanVariable b)
bool	ProbeDnf (absl::string_view name, absl::Span< const std::vector< Literal > > dnf)
int	num_decisions () const
int	num_new_literals_fixed () const
int	num_new_binary_clauses () const
void	SetPropagationCallback (std::function< void(Literal decision)> f)

Detailed Description

Definition at line 40 of file probing.h.

Constructor & Destructor Documentation

Prober()

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

explicit

Definition at line 48 of file probing.cc.

Member Function Documentation

num_decisions()

int operations_research::sat::Prober::num_decisions ( ) const

inline

Statistics. They are reset each time ProbleBooleanVariables() is called. Note however that we do not reset them on a call to ProbeOneVariable().

Definition at line 95 of file probing.h.

num_new_binary_clauses()

int operations_research::sat::Prober::num_new_binary_clauses ( ) const

inline

Definition at line 97 of file probing.h.

num_new_literals_fixed()

int operations_research::sat::Prober::num_new_literals_fixed ( ) const

inline

Definition at line 96 of file probing.h.

ProbeBooleanVariables() [1/2]

bool operations_research::sat::Prober::ProbeBooleanVariables

(

double

deterministic_time_limit

)

Fixes Booleans variables to true/false and see what is propagated. This can:

• Fix some Boolean variables (if we reach a conflict while probing).
• Infer new direct implications. We add them directly to the BinaryImplicationGraph and they can later be used to detect equivalent literals, expand at most ones clique, etc...
• Tighten the bounds of integer variables. If we probe the two possible values of a Boolean (b=0 and b=1), we get for each integer variables two propagated domain D_0 and D_1. The level zero domain can then be intersected with D_0 U D_1. This can restrict the lower/upper bounds of a variable, but it can also create holes in the domain! This will detect common cases like an integer variable in [0, 10] that actually only take two values [0] or [10] depending on one Boolean.

Returns false if the problem was proved INFEASIBLE during probing.

Todo

(user): For now we process the Boolean in their natural order, this is not the most efficient.

Todo

(user): This might generate a lot of new direct implications. We might not want to add them directly to the BinaryImplicationGraph and could instead use them directly to detect equivalent literal like in ProbeAndFindEquivalentLiteral(). The situation is not clear.

Todo

(user): More generally, we might want to register any literal => bound in the IntegerEncoder. This would allow to remember them and use them in other part of the solver (cuts, lifting, ...).

Todo

(user): Rename to include Integer in the name and distinguish better from FailedLiteralProbing() below.

Definition at line 59 of file probing.cc.

ProbeBooleanVariables() [2/2]

bool operations_research::sat::Prober::ProbeBooleanVariables	(	double	deterministic_time_limit,
		absl::Span< const BooleanVariable >	bool_vars )

Same as above method except it probes only on the variables given in 'bool_vars'.

Reset statistics.

Resize the propagated sparse bitset.

Reset the solver in case it was already used.

Todo

(user): Instead of an hard deterministic limit, we should probably use a lower one, but reset it each time we have found something useful.

Propagate b=1 and then b=0.

Update stats.

Display stats.

Definition at line 220 of file probing.cc.

ProbeDnf()

bool operations_research::sat::Prober::ProbeDnf	(	absl::string_view	name,
		absl::Span< const std::vector< Literal > >	dnf )

Probes the given problem DNF (disjunction of conjunctions). Since one of the conjunction must be true, we might be able to fix literal or improve integer bounds if all conjunction propagate the same thing.

Reset the solver in case it was already used.

We can exit safely as nothing will be propagated.

If the literal has been pushed without any conflict, the level should have been increased.

Todo

(user): Can we use the callback_?

Process propagated literals.

Process propagated integer bounds.

Fix literals implied by the dnf.

Fix integer bounds implied by the dnf.

Definition at line 302 of file probing.cc.

ProbeOneVariable()

bool operations_research::sat::Prober::ProbeOneVariable

(

BooleanVariable

b

)

Resize the propagated sparse bitset.

Reset the solver in case it was already used.

Statistics

Definition at line 203 of file probing.cc.

SetPropagationCallback()

void operations_research::sat::Prober::SetPropagationCallback ( std::function< void(Literal decision)> f )

inline

Register a callback that will be called on each "propagation". One can inspect the VariablesAssignment to see what are the inferred literals.

Definition at line 102 of file probing.h.

---

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

• ortools/sat/probing.h
• ortools/sat/probing.cc