OR-Tools  8.2
BinaryImplicationGraph

Detailed Description

Definition at line 456 of file clause.h.

Public Member Functions

 BinaryImplicationGraph (Model *model)
 
 ~BinaryImplicationGraph () override
 
bool Propagate (Trail *trail) final
 
absl::Span< const LiteralReason (const Trail &trail, int trail_index) const final
 
void Resize (int num_variables)
 
bool IsEmpty ()
 
void AddBinaryClause (Literal a, Literal b)
 
void AddImplication (Literal a, Literal b)
 
bool AddBinaryClauseDuringSearch (Literal a, Literal b)
 
ABSL_MUST_USE_RESULT bool AddAtMostOne (absl::Span< const Literal > at_most_one)
 
void MinimizeConflictWithReachability (std::vector< Literal > *c)
 
void MinimizeConflictExperimental (const Trail &trail, std::vector< Literal > *c)
 
void MinimizeConflictFirst (const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked)
 
void MinimizeConflictFirstWithTransitiveReduction (const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked, absl::BitGenRef random)
 
void RemoveFixedVariables ()
 
bool DetectEquivalences (bool log_info=false)
 
bool IsDag () const
 
const std::vector< LiteralIndex > & ReverseTopologicalOrder () const
 
const absl::InlinedVector< Literal, 6 > & Implications (Literal l) const
 
Literal RepresentativeOf (Literal l) const
 
bool ComputeTransitiveReduction (bool log_info=false)
 
bool TransformIntoMaxCliques (std::vector< std::vector< Literal > > *at_most_ones, int64 max_num_explored_nodes=1e8)
 
const std::vector< std::vector< Literal > > & GenerateAtMostOnesWithLargeWeight (const std::vector< Literal > &literals, const std::vector< double > &lp_values)
 
int64 num_propagations () const
 
int64 num_inspections () const
 
int64 num_minimization () const
 
int64 num_literals_removed () const
 
bool IsRedundant (Literal l) const
 
int64 num_redundant_literals () const
 
int64 num_redundant_implications () const
 
int64 num_implications () const
 
int64 literal_size () const
 
template<typename Output >
void ExtractAllBinaryClauses (Output *out) const
 
void SetDratProofHandler (DratProofHandler *drat_proof_handler)
 
void ChangeReason (int trail_index, Literal new_reason)
 
const std::vector< Literal > & DirectImplications (Literal literal)
 
int DirectImplicationsEstimatedSize (Literal literal) const
 
bool FindFailedLiteralAroundVar (BooleanVariable var, bool *is_unsat)
 
int64 NumImplicationOnVariableRemoval (BooleanVariable var)
 
void RemoveBooleanVariable (BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses)
 
bool IsRemoved (Literal l) const
 
void CleanupAllRemovedVariables ()
 
void SetPropagatorId (int id)
 
int PropagatorId () const
 
virtual void Untrail (const Trail &trail, int trail_index)
 
bool PropagatePreconditionsAreSatisfied (const Trail &trail) const
 
bool PropagationIsDone (const Trail &trail) const
 

Protected Attributes

const std::string name_
 
int propagator_id_
 
int propagation_trail_index_
 

Constructor & Destructor Documentation

◆ BinaryImplicationGraph()

BinaryImplicationGraph ( Model model)
inlineexplicit

Definition at line 458 of file clause.h.

◆ ~BinaryImplicationGraph()

~BinaryImplicationGraph ( )
inlineoverride

Definition at line 467 of file clause.h.

Member Function Documentation

◆ AddAtMostOne()

bool AddAtMostOne ( absl::Span< const Literal at_most_one)

Definition at line 531 of file clause.cc.

◆ AddBinaryClause()

void AddBinaryClause ( Literal  a,
Literal  b 
)

Definition at line 491 of file clause.cc.

◆ AddBinaryClauseDuringSearch()

bool AddBinaryClauseDuringSearch ( Literal  a,
Literal  b 
)

Definition at line 508 of file clause.cc.

◆ AddImplication()

void AddImplication ( Literal  a,
Literal  b 
)
inline

Definition at line 488 of file clause.h.

◆ ChangeReason()

void ChangeReason ( int  trail_index,
Literal  new_reason 
)
inline

Definition at line 674 of file clause.h.

◆ CleanupAllRemovedVariables()

void CleanupAllRemovedVariables ( )

Definition at line 1930 of file clause.cc.

◆ ComputeTransitiveReduction()

bool ComputeTransitiveReduction ( bool  log_info = false)

Definition at line 1311 of file clause.cc.

◆ DetectEquivalences()

bool DetectEquivalences ( bool  log_info = false)

Definition at line 1124 of file clause.cc.

◆ DirectImplications()

const std::vector< Literal > & DirectImplications ( Literal  literal)

Definition at line 1799 of file clause.cc.

◆ DirectImplicationsEstimatedSize()

int DirectImplicationsEstimatedSize ( Literal  literal) const
inline

Definition at line 693 of file clause.h.

◆ ExtractAllBinaryClauses()

void ExtractAllBinaryClauses ( Output *  out) const
inline

Definition at line 646 of file clause.h.

◆ FindFailedLiteralAroundVar()

bool FindFailedLiteralAroundVar ( BooleanVariable  var,
bool *  is_unsat 
)

Definition at line 1842 of file clause.cc.

◆ GenerateAtMostOnesWithLargeWeight()

const std::vector< std::vector< Literal > > & GenerateAtMostOnesWithLargeWeight ( const std::vector< Literal > &  literals,
const std::vector< double > &  lp_values 
)

Definition at line 1645 of file clause.cc.

◆ Implications()

const absl::InlinedVector< Literal, 6 > & Implications ( Literal  l) const
inline

Definition at line 554 of file clause.h.

◆ IsDag()

bool IsDag ( ) const
inline

Definition at line 543 of file clause.h.

◆ IsEmpty()

bool IsEmpty ( )
inline

Definition at line 483 of file clause.h.

◆ IsRedundant()

bool IsRedundant ( Literal  l) const
inline

Definition at line 620 of file clause.h.

◆ IsRemoved()

bool IsRemoved ( Literal  l) const
inline

Definition at line 708 of file clause.h.

◆ literal_size()

int64 literal_size ( ) const
inline

Definition at line 636 of file clause.h.

◆ MinimizeConflictExperimental()

void MinimizeConflictExperimental ( const Trail trail,
std::vector< Literal > *  c 
)

Definition at line 911 of file clause.cc.

◆ MinimizeConflictFirst()

void MinimizeConflictFirst ( const Trail trail,
std::vector< Literal > *  c,
SparseBitset< BooleanVariable > *  marked 
)

Definition at line 831 of file clause.cc.

◆ MinimizeConflictFirstWithTransitiveReduction()

void MinimizeConflictFirstWithTransitiveReduction ( const Trail trail,
std::vector< Literal > *  c,
SparseBitset< BooleanVariable > *  marked,
absl::BitGenRef  random 
)

Definition at line 849 of file clause.cc.

◆ MinimizeConflictWithReachability()

void MinimizeConflictWithReachability ( std::vector< Literal > *  c)

Definition at line 754 of file clause.cc.

◆ num_implications()

int64 num_implications ( ) const
inline

Definition at line 635 of file clause.h.

◆ num_inspections()

int64 num_inspections ( ) const
inline

Definition at line 608 of file clause.h.

◆ num_literals_removed()

int64 num_literals_removed ( ) const
inline

Definition at line 612 of file clause.h.

◆ num_minimization()

int64 num_minimization ( ) const
inline

Definition at line 611 of file clause.h.

◆ num_propagations()

int64 num_propagations ( ) const
inline

Definition at line 605 of file clause.h.

◆ num_redundant_implications()

int64 num_redundant_implications ( ) const
inline

Definition at line 627 of file clause.h.

◆ num_redundant_literals()

int64 num_redundant_literals ( ) const
inline

Definition at line 621 of file clause.h.

◆ NumImplicationOnVariableRemoval()

int64 NumImplicationOnVariableRemoval ( BooleanVariable  var)

Definition at line 1867 of file clause.cc.

◆ Propagate()

bool Propagate ( Trail trail)
finalvirtual

Implements SatPropagator.

Definition at line 730 of file clause.cc.

◆ PropagatePreconditionsAreSatisfied()

bool PropagatePreconditionsAreSatisfied ( const Trail trail) const
inlineinherited

Definition at line 517 of file sat_base.h.

◆ PropagationIsDone()

bool PropagationIsDone ( const Trail trail) const
inlineinherited

Definition at line 500 of file sat_base.h.

◆ PropagatorId()

int PropagatorId ( ) const
inlineinherited

Definition at line 453 of file sat_base.h.

◆ Reason()

absl::Span< const Literal > Reason ( const Trail trail,
int  trail_index 
) const
finalvirtual

Reimplemented from SatPropagator.

Definition at line 742 of file clause.cc.

◆ RemoveBooleanVariable()

void RemoveBooleanVariable ( BooleanVariable  var,
std::deque< std::vector< Literal > > *  postsolve_clauses 
)

Definition at line 1887 of file clause.cc.

◆ RemoveFixedVariables()

void RemoveFixedVariables ( )

Definition at line 962 of file clause.cc.

◆ RepresentativeOf()

Literal RepresentativeOf ( Literal  l) const
inline

Definition at line 561 of file clause.h.

◆ Resize()

void Resize ( int  num_variables)

Definition at line 477 of file clause.cc.

◆ ReverseTopologicalOrder()

const std::vector< LiteralIndex > & ReverseTopologicalOrder ( ) const
inline

Definition at line 547 of file clause.h.

◆ SetDratProofHandler()

void SetDratProofHandler ( DratProofHandler drat_proof_handler)
inline

Definition at line 667 of file clause.h.

◆ SetPropagatorId()

void SetPropagatorId ( int  id)
inlineinherited

Definition at line 452 of file sat_base.h.

◆ TransformIntoMaxCliques()

bool TransformIntoMaxCliques ( std::vector< std::vector< Literal > > *  at_most_ones,
int64  max_num_explored_nodes = 1e8 
)

Definition at line 1500 of file clause.cc.

◆ Untrail()

virtual void Untrail ( const Trail trail,
int  trail_index 
)
inlinevirtualinherited

Member Data Documentation

◆ name_

const std::string name_
protectedinherited

Definition at line 505 of file sat_base.h.

◆ propagation_trail_index_

int propagation_trail_index_
protectedinherited

Definition at line 507 of file sat_base.h.

◆ propagator_id_

int propagator_id_
protectedinherited

Definition at line 506 of file sat_base.h.


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