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 Literal >	Reason (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

Reimplemented in IntegerTrail, GenericLiteralWatcher, PbConstraints, PrecedencesPropagator, and SymmetryPropagator.

Definition at line 475 of file sat_base.h.

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:

Detailed Description

Public Member Functions

Protected Attributes

Constructor & Destructor Documentation

◆ BinaryImplicationGraph()

◆ ~BinaryImplicationGraph()

Member Function Documentation

◆ AddAtMostOne()

◆ AddBinaryClause()

◆ AddBinaryClauseDuringSearch()

◆ AddImplication()

◆ ChangeReason()

◆ CleanupAllRemovedVariables()

◆ ComputeTransitiveReduction()

◆ DetectEquivalences()

◆ DirectImplications()

◆ DirectImplicationsEstimatedSize()

◆ ExtractAllBinaryClauses()

◆ FindFailedLiteralAroundVar()

◆ GenerateAtMostOnesWithLargeWeight()

◆ Implications()

◆ IsDag()

◆ IsEmpty()

◆ IsRedundant()

◆ IsRemoved()

◆ literal_size()

◆ MinimizeConflictExperimental()

◆ MinimizeConflictFirst()

◆ MinimizeConflictFirstWithTransitiveReduction()

◆ MinimizeConflictWithReachability()

◆ num_implications()

◆ num_inspections()

◆ num_literals_removed()

◆ num_minimization()

◆ num_propagations()

◆ num_redundant_implications()

◆ num_redundant_literals()

◆ NumImplicationOnVariableRemoval()

◆ Propagate()

◆ PropagatePreconditionsAreSatisfied()

◆ PropagationIsDone()

◆ PropagatorId()

◆ Reason()

◆ RemoveBooleanVariable()

◆ RemoveFixedVariables()

◆ RepresentativeOf()

◆ Resize()

◆ ReverseTopologicalOrder()

◆ SetDratProofHandler()

◆ SetPropagatorId()

◆ TransformIntoMaxCliques()

◆ Untrail()

Member Data Documentation

◆ name_

◆ propagation_trail_index_

◆ propagator_id_