#include <pb_constraint.h>

Inheritance diagram for operations_research::sat::PbConstraints:

Public Member Functions
	PbConstraints (Model *model)

	PbConstraints (const PbConstraints &)=delete
	This type is neither copyable nor movable.

PbConstraints &	operator= (const PbConstraints &)=delete

	~PbConstraints () override

bool	Propagate (Trail *trail) final

void	Untrail (const Trail &trail, int trail_index) final

absl::Span< const Literal >	Reason (const Trail &trail, int trail_index, int64_t conflict_id) const final

void	Resize (int num_variables)
	Changes the number of variables.

bool	AddConstraint (const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)

bool	AddLearnedConstraint (const std::vector< LiteralWithCoeff > &cst, Coefficient rhs, Trail *trail)

int	NumberOfConstraints () const
	Returns the number of constraints managed by this class.

bool	IsEmpty () const final

void	ClearConflictingConstraint ()

UpperBoundedLinearConstraint *	ConflictingConstraint ()

UpperBoundedLinearConstraint *	ReasonPbConstraint (int trail_index) const

void	BumpActivity (UpperBoundedLinearConstraint *constraint)

void	RescaleActivities (double scaling_factor)

void	UpdateActivityIncrement ()

void	DeleteConstraint (int index)
	Only used for testing.

int64_t	num_constraint_lookups () const
	Some statistics.

int64_t	num_inspected_constraint_literals () const

int64_t	num_threshold_updates () const

Public Member Functions inherited from operations_research::sat::SatPropagator
	SatPropagator (const std::string &name)

	SatPropagator (const SatPropagator &)=delete
	This type is neither copyable nor movable.

SatPropagator &	operator= (const SatPropagator &)=delete

virtual	~SatPropagator ()=default

void	SetPropagatorId (int id)
	Sets/Gets this propagator unique id.

int	PropagatorId () const

bool	PropagatePreconditionsAreSatisfied (const Trail &trail) const
	######################## Implementations below ########################

bool	PropagationIsDone (const Trail &trail) const
	Returns true iff all the trail was inspected by this propagator.

Additional Inherited Members
Protected Attributes inherited from operations_research::sat::SatPropagator
const std::string	name_

int	propagator_id_

int	propagation_trail_index_

Detailed Description

Class responsible for managing a set of pseudo-Boolean constraints and their propagation.

Definition at line 528 of file pb_constraint.h.

Constructor & Destructor Documentation

◆ PbConstraints() [1/2]

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

inlineexplicit

Definition at line 530 of file pb_constraint.h.

◆ PbConstraints() [2/2]

operations_research::sat::PbConstraints::PbConstraints ( const PbConstraints & )

delete

This type is neither copyable nor movable.

◆ ~PbConstraints()

operations_research::sat::PbConstraints::~PbConstraints ( )

inlineoverride

Definition at line 546 of file pb_constraint.h.

Member Function Documentation

◆ AddConstraint()

bool operations_research::sat::PbConstraints::AddConstraint	(	const std::vector< LiteralWithCoeff > &	cst,
		Coefficient	rhs,
		Trail *	trail )

Adds a constraint in canonical form to the set of managed constraints. Note that this detects constraints with exactly the same terms. In this case, the constraint rhs is updated if the new one is lower or nothing is done otherwise.

There are some preconditions, and the function will return false if they are not met. The constraint can be added when the trail is not empty, however given the current propagated assignment:

The constraint cannot be conflicting.
The constraint cannot have propagated at an earlier decision level.

Todo
(user): This is relatively slow. Take the "transpose" all at once, and maybe put small constraints first on the to_update_ lists.

Special case if this is the first constraint.

Optimization if the constraint terms are duplicates.

Todo: (user): the index is needed to give the correct thresholds_ entry to InitializeRhs() below, but this linear scan is not super efficient.

The constraint is redundant, so there is nothing to do.

Definition at line 837 of file pb_constraint.cc.

◆ AddLearnedConstraint()

bool operations_research::sat::PbConstraints::AddLearnedConstraint	(	const std::vector< LiteralWithCoeff > &	cst,
		Coefficient	rhs,
		Trail *	trail )

Same as AddConstraint(), but also marks the added constraint as learned so that it can be deleted during the constraint cleanup phase.

The second test is to avoid marking a problem constraint as learned because of the "reuse last constraint" optimization.

Definition at line 898 of file pb_constraint.cc.

◆ BumpActivity()

void operations_research::sat::PbConstraints::BumpActivity ( UpperBoundedLinearConstraint * constraint )

Activity update functions.

Todo: (user): Remove duplication with other activity update functions.

Definition at line 1081 of file pb_constraint.cc.

◆ ClearConflictingConstraint()

void operations_research::sat::PbConstraints::ClearConflictingConstraint ( )

inline

ConflictingConstraint() returns the last PB constraint that caused a conflict. Calling ClearConflictingConstraint() reset this to nullptr.

Todo: (user): This is a hack to get the PB conflict, because the rest of the solver API assume only clause conflict. Find a cleaner way?

Definition at line 597 of file pb_constraint.h.

◆ ConflictingConstraint()

UpperBoundedLinearConstraint * operations_research::sat::PbConstraints::ConflictingConstraint ( )

inline

Definition at line 598 of file pb_constraint.h.

◆ DeleteConstraint()

void operations_research::sat::PbConstraints::DeleteConstraint ( int index )

inline

Only used for testing.

Definition at line 614 of file pb_constraint.h.

◆ IsEmpty()

bool operations_research::sat::PbConstraints::IsEmpty ( ) const

inlinefinalvirtual

Small optimization: If a propagator does not contain any "constraints" there is no point calling propagate on it. Before each propagation, the solver will checks for emptiness, and construct an optimized list of propagator before looping many time over the list.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 590 of file pb_constraint.h.

◆ num_constraint_lookups()

int64_t operations_research::sat::PbConstraints::num_constraint_lookups ( ) const

inline

Some statistics.

Definition at line 620 of file pb_constraint.h.

◆ num_inspected_constraint_literals()

int64_t operations_research::sat::PbConstraints::num_inspected_constraint_literals ( ) const

inline

Definition at line 621 of file pb_constraint.h.

◆ num_threshold_updates()

int64_t operations_research::sat::PbConstraints::num_threshold_updates ( ) const

inline

Definition at line 624 of file pb_constraint.h.

◆ NumberOfConstraints()

int operations_research::sat::PbConstraints::NumberOfConstraints ( ) const

inline

Returns the number of constraints managed by this class.

Definition at line 589 of file pb_constraint.h.

◆ operator=()

PbConstraints & operations_research::sat::PbConstraints::operator= ( const PbConstraints & )

delete

◆ Propagate()

bool operations_research::sat::PbConstraints::Propagate ( Trail * trail )

finalvirtual

Inspects the trail from propagation_trail_index_ until at least one literal is propagated. Returns false iff a conflict is detected (in which case trail->SetFailingClause() must be called).

This must update propagation_trail_index_ so that all the literals before it have been propagated. In particular, if nothing was propagated, then PropagationIsDone() must return true.

Implements operations_research::sat::SatPropagator.

Definition at line 948 of file pb_constraint.cc.

◆ Reason()

absl::Span< const Literal > operations_research::sat::PbConstraints::Reason	(	const Trail &	,
		int	,
		int64_t	) const

finalvirtual

Explains why the literal at given trail_index was propagated by returning a reason for this propagation. This will only be called for literals that are on the trail and were propagated by this class.

The interpretation is that because all the literals of a reason were assigned to false, we could deduce the assignment of the given variable.

The returned Span has to be valid until the literal is untrailed. A client can use trail_.GetEmptyVectorToStoreReason() if it doesn't have a memory location that already contains the reason.

If conlict id is positive, then this is called during first UIP resolution and we will backtrack over this literal right away, so we don't need to have a span that survive more than once.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 979 of file pb_constraint.cc.

◆ ReasonPbConstraint()

UpperBoundedLinearConstraint * operations_research::sat::PbConstraints::ReasonPbConstraint ( int trail_index ) const

Returns the underlying UpperBoundedLinearConstraint responsible for assigning the literal at given trail index.

Definition at line 991 of file pb_constraint.cc.

◆ RescaleActivities()

void operations_research::sat::PbConstraints::RescaleActivities ( double scaling_factor )

Definition at line 1091 of file pb_constraint.cc.

◆ Resize()

void operations_research::sat::PbConstraints::Resize ( int num_variables )

inline

Changes the number of variables.

Note: we avoid using up memory in the common case where there are no pb constraints at all. If there is 10 million variables, this vector alone will take 480 MB!

Definition at line 560 of file pb_constraint.h.

◆ Untrail()

void operations_research::sat::PbConstraints::Untrail	(	const Trail &	,
		int	trail_index )

finalvirtual

Reverts the state so that all the literals with a trail index greater or equal to the given one are not processed for propagation. Note that the trail current decision level is already reverted before this is called.

Todo: (user): Currently this is called at each Backtrack(), but we could bundle the calls in case multiple conflict one after the other are detected even before the Propagate() call of a SatPropagator is called.

Todo: (user): It is not yet 100% the case, but this can be guaranteed to be called with a trail index that will always be the start of a new decision level.

Only the constraints which were inspected during Propagate() need inspection during Untrail().

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 956 of file pb_constraint.cc.

◆ UpdateActivityIncrement()

void operations_research::sat::PbConstraints::UpdateActivityIncrement ( )

Definition at line 1098 of file pb_constraint.cc.

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

ortools/sat/pb_constraint.h
ortools/sat/pb_constraint.cc

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ PbConstraints() [1/2]

◆ PbConstraints() [2/2]

◆ ~PbConstraints()

Member Function Documentation

◆ AddConstraint()

◆ AddLearnedConstraint()

◆ BumpActivity()

◆ ClearConflictingConstraint()

◆ ConflictingConstraint()

◆ DeleteConstraint()

◆ IsEmpty()

◆ num_constraint_lookups()

◆ num_inspected_constraint_literals()

◆ num_threshold_updates()

◆ NumberOfConstraints()

◆ operator=()

◆ Propagate()

◆ Reason()

◆ ReasonPbConstraint()

◆ RescaleActivities()

◆ Resize()

◆ Untrail()

◆ UpdateActivityIncrement()