operations_research::sat::SatPropagator Class Reference

Base class for all the SAT constraints. More...

#include <sat_base.h>

Inheritance diagram for operations_research::sat::SatPropagator:

Public Member Functions
	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
virtual bool	Propagate (Trail *trail)=0
virtual void	Untrail (const Trail &, int trail_index)
virtual absl::Span< const Literal >	Reason (const Trail &, int, int64_t) 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.
virtual bool	IsEmpty () const

Protected Attributes
const std::string	name_
int	propagator_id_
int	propagation_trail_index_

Detailed Description

Base class for all the SAT constraints.

Definition at line 533 of file sat_base.h.

Constructor & Destructor Documentation

SatPropagator() [1/2]

operations_research::sat::SatPropagator::SatPropagator ( const std::string & name )

inlineexplicit

Definition at line 535 of file sat_base.h.

SatPropagator() [2/2]

operations_research::sat::SatPropagator::SatPropagator ( const SatPropagator & )

delete

This type is neither copyable nor movable.

~SatPropagator()

virtual operations_research::sat::SatPropagator::~SatPropagator ( )

virtualdefault

Member Function Documentation

IsEmpty()

virtual bool operations_research::sat::SatPropagator::IsEmpty ( ) const

inlinevirtual

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 in operations_research::sat::BinaryImplicationGraph, and operations_research::sat::PbConstraints.

Definition at line 605 of file sat_base.h.

operator=()

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

delete

Propagate()

virtual bool operations_research::sat::SatPropagator::Propagate ( Trail * trail )

pure virtual

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.

Implemented in operations_research::sat::BinaryImplicationGraph, operations_research::sat::ClauseManager, operations_research::sat::EnforcementPropagator, operations_research::sat::GenericLiteralWatcher, operations_research::sat::IntegerTrail, operations_research::sat::PbConstraints, operations_research::sat::PrecedencesPropagator, and operations_research::sat::SymmetryPropagator.

PropagatePreconditionsAreSatisfied()

bool operations_research::sat::SatPropagator::PropagatePreconditionsAreSatisfied ( const Trail & trail ) const

inline

######################## Implementations below ########################

Returns true if all the preconditions for Propagate() are satisfied. This is just meant to be used in a DCHECK.

Todo

(user): A few of these method should be moved in a .cc

Definition at line 617 of file sat_base.h.

PropagationIsDone()

bool operations_research::sat::SatPropagator::PropagationIsDone ( const Trail & trail ) const

inline

Returns true iff all the trail was inspected by this propagator.

Definition at line 597 of file sat_base.h.

PropagatorId()

int operations_research::sat::SatPropagator::PropagatorId ( ) const

inline

Definition at line 545 of file sat_base.h.

Reason()

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

inlinevirtual

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 in operations_research::sat::BinaryImplicationGraph, operations_research::sat::ClauseManager, operations_research::sat::IntegerTrail, operations_research::sat::PbConstraints, and operations_research::sat::SymmetryPropagator.

Definition at line 585 of file sat_base.h.

SetPropagatorId()

void operations_research::sat::SatPropagator::SetPropagatorId ( int id )

inline

Sets/Gets this propagator unique id.

Definition at line 544 of file sat_base.h.

Untrail()

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

inlinevirtual

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.

Reimplemented in operations_research::sat::EnforcementPropagator, operations_research::sat::GenericLiteralWatcher, operations_research::sat::IntegerTrail, operations_research::sat::PbConstraints, operations_research::sat::PrecedencesPropagator, and operations_research::sat::SymmetryPropagator.

Definition at line 567 of file sat_base.h.

Member Data Documentation

name_

const std::string operations_research::sat::SatPropagator::name_

protected

Definition at line 608 of file sat_base.h.

propagation_trail_index_

int operations_research::sat::SatPropagator::propagation_trail_index_

protected

Definition at line 610 of file sat_base.h.

propagator_id_

int operations_research::sat::SatPropagator::propagator_id_

protected

Definition at line 609 of file sat_base.h.

---

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

• ortools/sat/sat_base.h