#include <clause.h>

Inheritance diagram for operations_research::sat::BinaryImplicationGraph:

Public Member Functions
	BinaryImplicationGraph (Model *model)

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

BinaryImplicationGraph &	operator= (const BinaryImplicationGraph &)=delete

	~BinaryImplicationGraph () override

bool	Propagate (Trail *trail) final
	SatPropagator interface.

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

void	Resize (int num_variables)
	Resizes the data structure.

bool	IsEmpty () const final
	Returns true if there is no constraints in this class.

bool	AddBinaryClause (Literal a, Literal b)

bool	AddImplication (Literal a, Literal b)

void	EnableSharing (bool enable)

void	SetAdditionCallback (std::function< void(Literal, Literal)> f)

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, 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_t max_num_explored_nodes=1e8)

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

std::vector< absl::Span< const Literal > >	HeuristicAmoPartition (std::vector< Literal > *literals)

int64_t	num_propagations () const
	Number of literal propagated by this class (including conflicts).

int64_t	num_inspections () const
	Number of literals inspected by this class during propagation.

int64_t	num_minimization () const
	MinimizeClause() stats.

int64_t	num_literals_removed () const

bool	IsRedundant (Literal l) const

int64_t	num_redundant_literals () const

int64_t	num_redundant_implications () const
	Number of implications removed by transitive reduction.

int64_t	num_implications () const

int64_t	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)

LiteralIndex	RandomImpliedLiteral (Literal lhs)

int	DirectImplicationsEstimatedSize (Literal literal) const

bool	FindFailedLiteralAroundVar (BooleanVariable var, bool *is_unsat)

int64_t	NumImplicationOnVariableRemoval (BooleanVariable var)

void	RemoveBooleanVariable (BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses)
	For all possible a => var => b, add a => b.

bool	IsRemoved (Literal l) const

void	RemoveAllRedundantVariables (std::deque< std::vector< Literal > > *postsolve_clauses)

void	CleanupAllRemovedAndFixedVariables ()

void	ResetWorkDone ()

int64_t	WorkDone () const

template<bool use_weight = true>
std::vector< Literal >	ExpandAtMostOneWithWeight (absl::Span< const Literal > at_most_one, const util_intops::StrongVector< LiteralIndex, bool > &can_be_included, const util_intops::StrongVector< LiteralIndex, double > &expanded_lp_values)
	Same as ExpandAtMostOne() but try to maximize the weight in the clique.

void	ResetAtMostOneIterator ()
	Restarts the at_most_one iterator.

absl::Span< const Literal >	NextAtMostOne ()
	Returns the next at_most_one, or a span of size 0 when finished.

void	RemoveDuplicates ()
	Clean up implications list that might have duplicates.

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

virtual void	Untrail (const Trail &, int trail_index)

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

Special class to store and propagate clauses of size 2 (i.e. implication). Such clauses are never deleted. Together, they represent the 2-SAT part of the problem. Note that 2-SAT satisfiability is a polynomial problem, but W2SAT (weighted 2-SAT) is NP-complete.

Todo: (user): Most of the note below are done, but we currently only applies the reduction before the solve. We should consider doing more in-processing. The code could probably still be improved too.

Note(user): All the variables in a strongly connected component are equivalent and can be thus merged as one. This is relatively cheap to compute from time to time (linear complexity). We will also get contradiction (a <=> not a) this way. This is done by DetectEquivalences().

Note(user): An implication (a => not a) implies that a is false. I am not sure it is worth detecting that because if the solver assign a to true, it will learn that right away. I don't think we can do it faster.

Note(user): The implication graph can be pruned. This is called the transitive reduction of a graph. For instance If a => {b,c} and b => {c}, then there is no need to store a => {c}. The transitive reduction is unique on an acyclic graph. Computing it will allow for a faster propagation and memory reduction. It is however not cheap. Maybe simple lazy heuristics to remove redundant arcs are better. Note that all the learned clauses we add will never be redundant (but they could introduce cycles). This is done by ComputeTransitiveReduction().

Note(user): This class natively support at most one constraints. This is a way to reduced significantly the memory and size of some 2-SAT instances. However, it is not fully exploited for pure SAT problems. See TransformIntoMaxCliques().

Note(user): Add a preprocessor to remove duplicates in the implication lists.

Note: all the learned clauses we add will never create duplicates.

References for most of the above and more:

Brafman RI, "A simplifier for propositional formulas with many binary clauses", IEEE Trans Syst Man Cybern B Cybern. 2004 Feb;34(1):52-9. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.4911
Marijn J. H. Heule, Matti Järvisalo, Armin Biere, "Efficient CNF Simplification Based on Binary Implication Graphs", Theory and Applications of Satisfiability Testing - SAT 2011, Lecture Notes in Computer Science Volume 6695, 2011, pp 201-215 http://www.cs.helsinki.fi/u/mjarvisa/papers/heule-jarvisalo-biere.sat11.pdf

Definition at line 480 of file clause.h.

Constructor & Destructor Documentation

◆ BinaryImplicationGraph() [1/2]

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

inlineexplicit

Definition at line 482 of file clause.h.

◆ BinaryImplicationGraph() [2/2]

operations_research::sat::BinaryImplicationGraph::BinaryImplicationGraph ( const BinaryImplicationGraph & )

delete

This type is neither copyable nor movable.

◆ ~BinaryImplicationGraph()

operations_research::sat::BinaryImplicationGraph::~BinaryImplicationGraph ( )

inlineoverride

Definition at line 498 of file clause.h.

Member Function Documentation

◆ AddAtMostOne()

bool operations_research::sat::BinaryImplicationGraph::AddAtMostOne ( absl::Span< const Literal > at_most_one )

An at most one constraint of size n is a compact way to encode n * (n - 1) implications. This must only be called at level zero.

Returns false if this creates a conflict. Currently this can only happens if there is duplicate literal already assigned to true in this constraint.

Todo: (user): Our algorithm could generalize easily to at_most_ones + a list of literals that will be false if one of the literal in the amo is at one. It is a way to merge common list of implications.

If the final AMO size is smaller than at_most_one_expansion_size parameters, we fully expand it.

Temporarily copy the at_most_one constraint at the end of at_most_one_buffer_. It will be cleaned up and added by CleanUpAndAddAtMostOnes().

Definition at line 591 of file clause.cc.

◆ AddBinaryClause()

bool operations_research::sat::BinaryImplicationGraph::AddBinaryClause	(	Literal	a,
		Literal	b )

Adds the binary clause (a OR b), which is the same as (not a => b).

Note: it is also equivalent to (not b => a).

Preconditions:

If we are at root node, then none of the literal should be assigned. This is Checked and is there to track inefficiency as we do not need a clause in this case.
If we are at a positive decision level, we will propagate something if we can. However, if both literal are false, we will just return false and do nothing. In all other case, we will return true.

Todo
(user): Not all of the solver knows about representative literal, do use them here to maintains invariant? Explore this when we start cleaning our clauses using equivalence during search. We can easily do it for every conflict we learn instead of here.

Tricky: If this is the first clause, the propagator will be added and assumed to be in a "propagated" state. This makes sure this is the case.

Todo: (user): Like this we will duplicate all binary clause from the problem. However this leads to a simpler API (since we don't need to special case the loading of the original clauses) and we mainly use drat proof for testing anyway.

Definition at line 531 of file clause.cc.

◆ AddImplication()

bool operations_research::sat::BinaryImplicationGraph::AddImplication	(	Literal	a,
		Literal	b )

inline

Definition at line 529 of file clause.h.

◆ ChangeReason()

void operations_research::sat::BinaryImplicationGraph::ChangeReason	(	int	trail_index,
		Literal	new_reason )

inline

Changes the reason of the variable at trail index to a binary reason.

Note: the implication "new_reason => trail_[trail_index]" should be part of the implication graph.

Definition at line 734 of file clause.h.

◆ CleanupAllRemovedAndFixedVariables()

void operations_research::sat::BinaryImplicationGraph::CleanupAllRemovedAndFixedVariables ( )

The code assumes that everything is already propagated. Otherwise we will remove implications that didn't propagate yet!

Clean-up at most ones.

Note: to please the invariant() we also removed fixed literal above.

Definition at line 2330 of file clause.cc.

◆ ComputeTransitiveReduction()

bool operations_research::sat::BinaryImplicationGraph::ComputeTransitiveReduction ( bool log_info = false )

Prunes the implication graph by calling first DetectEquivalences() to remove cycle and then by computing the transitive reduction of the remaining DAG.

Note: this can be slow (num_literals graph traversals), so we abort early if we start doing too much work.

Returns false if the model is detected to be UNSAT (this needs to call DetectEquivalences() if not already done).

Note: as a side effect this also do a full "failed literal probing" using the binary implication graph only.

Todo: (user): Track which literal have new implications, and only process the antecedants of these.

Todo: (user): the situation with fixed variable is not really "clean". Simplify the code so we are sure we don't run into issue or have to deal with any of that here.

For each node we do a graph traversal and only keep the literals at maximum distance 1. This only works because we have a DAG when ignoring the "redundant" literal marked by DetectEquivalences(). Note that we also need no duplicates in the implications list for correctness which is also guaranteed by DetectEquivalences().

Todo: (user): We should be able to reuse some propagation like it is done for tree-look. Once a node is processed, we just need to process a node that implies it. Test if we can make this faster. Alternatively, only clear a part of is_marked_ (after the first child of root in reverse topo order).

Todo: (user): Can we exploit the fact that the implication graph is a skew-symmetric graph (isomorphic to its transposed) so that we do less work?

In most situation reverse_topological_order_ contains no redundant, fixed or removed variables. But the reverse_topological_order_ is only recomputed when new binary are added to the graph, not when new variable are fixed.

This is a "poor" version of the tree look stuff, but it does show good improvement. If we just processed one of the child of root, we don't need to re-explore it.

Todo: (user): Another optim we can do is that we never need to expand any node with a reverse topo order smaller or equal to the min of the ones in this list.

This is a corner case where because of equivalent literal, root appear in implications_[root], we will remove it below.

When this happens, then root must be false, we handle this just after the loop.

We have a DAG, so direct_child could only be marked first.

Also mark all the ones reachable through the root AMOs.

Failed literal probing. If both x and not(x) are marked then root must be false. Note that because we process "roots" in reverse topological order, we will fix the LCA of x and not(x) first.

We tested that at the beginning.

We propagate right away the binary implications so that we do not need to consider all antecedents of root in the transitive reduction.

Note: direct_implications will be cleared by RemoveFixedVariables() that will need to inspect it to completely remove Literal(root) from all lists.

Only keep the non-marked literal (and the redundant one which are never marked). We mark root to remove it in the corner case where it was there.

Abort if the computation involved is too big.

If we aborted early, we might no longer have both a=>b and not(b)=>not(a). This is not desirable has some algo relies on this invariant. We fix this here.

Definition at line 1441 of file clause.cc.

◆ DetectEquivalences()

bool operations_research::sat::BinaryImplicationGraph::DetectEquivalences ( bool log_info = false )

Returns false if the model is unsat, otherwise detects equivalent variable (with respect to the implications only) and reorganize the propagation lists accordingly.

Todo: (user): Completely get rid of such literal instead? it might not be reasonable code-wise to remap our literals in all of our constraints though.

This was already called, and no new constraint where added. Note that new fixed variable cannot create new equivalence, only new binary clauses do.

Lets remove all fixed variables first.

Todo: (user): We could just do it directly though.

The old values will still be valid.

If one is fixed then all must be fixed. Note that the reason why the propagation didn't already do that and we don't always get fixed component of size 1 is because of the potential newly fixed literals above.

In any case, all fixed literals are marked as redundant.

Next component.

We ignore variable that appear in no constraints.

We always take the smallest literal index (which also corresponds to the smallest BooleanVariable index) as a representative. This make sure that the representative of a literal l and the one of not(l) will be the negation of each other. There is also reason to think that it is heuristically better to use a BooleanVariable that was created first.

Note: because we process list in reverse topological order, this is only needed if there is any equivalence before this point.

Sets the representative.

Detect if x <=> not(x) which means unsat. Note that we relly on the fact that when sorted, they will both be consecutive in the list.

Merge all the lists in implications_[representative].

Note: we do not want representative in its own list.

Add representative <=> literal.

Remark: this relation do not need to be added to a DRAT proof since the redundant variables should never be used again for a pure SAT problem.

Remap all at most ones. Remove fixed variables, process duplicates. Note that this might result in more implications when we expand small at most one.

Definition at line 1248 of file clause.cc.

◆ DirectImplications()

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

The literals that are "directly" implied when literal is set to true. This is not a full "reachability". It includes at most ones propagation. The set of all direct implications is enough to describe the implications graph completely.

When doing blocked clause elimination of bounded variable elimination, one only need to consider this list and not the full reachability.

Todo

(user): lazy cleanup the lists on is_removed_?

(user): Mark fixed variable as is_removed_ for faster iteration?

Clear old state.

Fill new state.

Definition at line 2140 of file clause.cc.

◆ DirectImplicationsEstimatedSize()

int operations_research::sat::BinaryImplicationGraph::DirectImplicationsEstimatedSize ( Literal literal ) const

inline

A proxy for DirectImplications().size(), However we currently do not maintain it perfectly. It is exact each time DirectImplications() is called, and we update it in some situation but we don't deal with fixed variables, at_most ones and duplicates implications for now.

Definition at line 758 of file clause.h.

◆ EnableSharing()

void operations_research::sat::BinaryImplicationGraph::EnableSharing ( bool enable )

inline

When set, the callback will be called on ALL newly added binary clauses.

The EnableSharing() function can be used to disable sharing temporarily for the clauses that are imported from the Shared repository already.

Todo: (user): this is meant to share clause between workers, hopefully the contention will not be too high. Double check and maybe add a batch version were we keep new implication and add them in batches.

Definition at line 541 of file clause.h.

◆ ExpandAtMostOneWithWeight()

template<bool use_weight>

template std::vector< Literal > operations_research::sat::BinaryImplicationGraph::ExpandAtMostOneWithWeight< false >	(	absl::Span< const Literal >	at_most_one,
		const util_intops::StrongVector< LiteralIndex, bool > &	can_be_included,
		const util_intops::StrongVector< LiteralIndex, double > &	expanded_lp_values )

Same as ExpandAtMostOne() but try to maximize the weight in the clique.

Make sure both version are compiled.

Do not spend too much time here.

We can't generate a violated cut this way. This is because intersection contains all the possible ways to extend the current clique.

Expand? The negation of any literal in the intersection is a valid way to extend the clique.

Heuristic: use literal with largest lp value. We randomize slightly.

If we don't use weight, we prefer variable that comes first.

Definition at line 1802 of file clause.cc.

◆ ExtractAllBinaryClauses()

template<typename Output >

void operations_research::sat::BinaryImplicationGraph::ExtractAllBinaryClauses ( Output * out ) const

inline

Extract all the binary clauses managed by this class. The Output type must support an AddBinaryClause(Literal a, Literal b) function.

Important: This currently does NOT include at most one constraints.

Todo: (user): When extracting to cp_model.proto we could be more efficient by extracting bool_and constraint with many lhs terms.

Todo: (user): Ideally we should just never have duplicate clauses in this class. But it seems we do in some corner cases, so lets not output them twice.

Note(user): We almost always have both a => b and not(b) => not(a) in our implications_ database. Except if ComputeTransitiveReduction() was aborted early, but in this case, if only one is present, the other could be removed, so we shouldn't need to output it.

Definition at line 707 of file clause.h.

◆ FindFailedLiteralAroundVar()

bool operations_research::sat::BinaryImplicationGraph::FindFailedLiteralAroundVar	(	BooleanVariable	var,
		bool *	is_unsat )

Variable elimination by replacing everything of the form a => var => b by a => b. We ignore any a => a so the number of new implications is not always just the product of the two direct implication list of var and not(var). However, if a => var => a, then a and var are equivalent, so this case will be removed if one run DetectEquivalences() before this. Similarly, if a => var => not(a) then a must be false and this is detected and dealt with by FindFailedLiteralAroundVar().

not(l) => literal => l.

Definition at line 2212 of file clause.cc.

◆ GenerateAtMostOnesWithLargeWeight()

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

LP clique cut heuristic. Returns a set of "at most one" constraints on the given literals or their negation that are violated by the current LP solution. Note that this assumes that lp_value(lit) = 1 - lp_value(lit.Negated()).

The literal and lp_values vector are in one to one correspondence. We will only generate clique with these literals or their negation.

Todo: (user): Refine the heuristic and unit test!

We only want to generate a cut with literals from the LP, not extra ones.

We want highest sum first.

First heuristic. Currently we only consider violated at most one of size 2, and extend them. Right now, the code is a bit slow to try too many at every LP node so it is why we are defensive like this. Note also that because we currently still statically add the initial implications, this will only add cut based on newly learned binary clause. Or the one that were not added to the relaxation in the first place.

We consider only one candidate for each current_literal.

Do not genate too many cut at once.

Expand to a maximal at most one each candidates before returning them.

Note: we only expand using literal from the LP.

Definition at line 1894 of file clause.cc.

◆ HeuristicAmoPartition()

std::vector< absl::Span< const Literal > > operations_research::sat::BinaryImplicationGraph::HeuristicAmoPartition ( std::vector< Literal > * literals )

Heuristically identify "at most one" between the given literals, swap them around and return these amo as span inside the literals vector.

Todo: (user): Add a limit to make sure this do not take too much time.

Todo

(user): Use deterministic limit.

(user): Explore the graph instead of just looking at full amo, especially since we expand small ones.

Priority queue of (intersection_size, start_of_amo).

Compute for each at most one that might overlap, its overlaping size and stores its start in the at_most_one_buffer_.

This is in O(num_literal in amo).

Abort early if we are done.

Consume AMOs, update size.

Recompute size.

re-add with new size.

Mark the literal of that at most one at false.

Extract the intersection by moving it in [num_processed, num_processed + intersection_size).

Definition at line 1983 of file clause.cc.

◆ Implications()

const absl::InlinedVector< Literal, 6 > & operations_research::sat::BinaryImplicationGraph::Implications ( Literal l ) const

inline

Returns the list of literal "directly" implied by l. Beware that this can easily change behind your back if you modify the solver state.

Definition at line 607 of file clause.h.

◆ IsDag()

bool operations_research::sat::BinaryImplicationGraph::IsDag ( ) const

inline

Returns true if DetectEquivalences() has been called and no new binary clauses have been added since then. When this is true then there is no cycle in the binary implication graph (modulo the redundant literals that form a cycle with their representative).

Definition at line 596 of file clause.h.

◆ IsEmpty()

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

inlinefinalvirtual

Returns true if there is no constraints in this class.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 514 of file clause.h.

◆ IsRedundant()

bool operations_research::sat::BinaryImplicationGraph::IsRedundant ( Literal l ) const

inline

Returns true if this literal is fixed or is equivalent to another literal. This means that it can just be ignored in most situation.

Note: the set (and thus number) of redundant literal can only grow over time. This is because we always use the lowest index as representative of an equivalent class, so a redundant literal will stay that way.

Definition at line 681 of file clause.h.

◆ IsRemoved()

bool operations_research::sat::BinaryImplicationGraph::IsRemoved ( Literal l ) const

inline

Definition at line 773 of file clause.h.

◆ literal_size()

int64_t operations_research::sat::BinaryImplicationGraph::literal_size ( ) const

inline

Definition at line 697 of file clause.h.

◆ MinimizeConflictExperimental()

void operations_research::sat::BinaryImplicationGraph::MinimizeConflictExperimental	(	const Trail &	trail,
		std::vector< Literal > *	conflict )

Todo: (user): Also consider at most one?

Identify and remove the redundant literals from the given conflict. 1/ If a -> b then a can be removed from the conflict clause. This is because not b -> not a. 2/ a -> b can only happen if level(a) <= level(b). 3/ Because of 2/, cycles can appear only at the same level. The vector is_simplified_ is used to avoid removing all elements of a cycle. Note that this is not optimal in the sense that we may not remove a literal that can be removed.

Note: there is no need to explore the unique literal of the highest decision level since it can't be removed. Because this is a conflict, such literal is always at position 0, so we start directly at 1.

Definition at line 1025 of file clause.cc.

◆ MinimizeConflictFirst()

void operations_research::sat::BinaryImplicationGraph::MinimizeConflictFirst	(	const Trail &	trail,
		std::vector< Literal > *	conflict,
		SparseBitset< BooleanVariable > *	marked )

Same as MinimizeConflictWithReachability() but also mark (in the given SparseBitset) the reachable literal already assigned to false. These literals will be implied if the 1-UIP literal is assigned to false, and the classic minimization algorithm can take advantage of that.

Todo: (user): if this is false, then we actually have a conflict of size 2. This can only happen if the binary clause was not propagated properly if for instance we do chronological bactracking without re-enqueing the consequence of a binary clause.

Definition at line 941 of file clause.cc.

◆ MinimizeConflictFirstWithTransitiveReduction()

void operations_research::sat::BinaryImplicationGraph::MinimizeConflictFirstWithTransitiveReduction	(	const Trail &	trail,
		std::vector< Literal > *	conflict,
		absl::BitGenRef	random )

Same as MinimizeConflictFirst() but take advantage of this reachability computation to remove redundant implication in the implication list of the first UIP conflict.

The randomization allow to find more redundant implication since to find a => b and remove b, a must be before b in direct_implications. Note that a std::reverse() could work too. But randomization seems to work better. Probably because it has other impact on the search tree.

The literal is already marked! so it must be implied by one of the previous literal in the direct_implications list. We can safely remove it.

Definition at line 963 of file clause.cc.

◆ MinimizeConflictWithReachability()

void operations_research::sat::BinaryImplicationGraph::MinimizeConflictWithReachability ( std::vector< Literal > * conflict )

Uses the binary implication graph to minimize the given conflict by removing literals that implies others. The idea is that if a and b are two literals from the given conflict and a => b (which is the same as not(b) => not(a)) then a is redundant and can be removed.

Note: removing as many literals as possible is too time consuming, so we use different heuristics/algorithms to do this minimization. See the binary_minimization_algorithm SAT parameter and the .cc for more details about the different algorithms.

Here, we remove all the literal whose negation are implied by the negation of the 1-UIP literal (which always appear first in the given conflict). Note that this algorithm is "optimal" in the sense that it leads to a minimized conflict with a backjump level as low as possible. However, not all possible literals are removed.

Todo: (user): Also consider at most one?

Compute the reachability from the literal "not(conflict->front())" using an iterative dfs.

Todo: (user): This sounds like a good idea, but somehow it seems better not to do that even though it is almost for free. Investigate more.

The idea here is that since we already compute the reachability from the root literal, we can use this computation to remove any implication root_literal => b if there is already root_literal => a and b is reachable from a.

We treat the direct implications differently so we can also remove the redundant implications from this list at the same time.

The "trick" is to unmark 'l'. This way, if we explore it twice, it means that this l is reachable from some other 'l' from the direct implication list. Remarks:

We don't loose too much complexity when this happen since a literal can be unmarked only once, so in the worst case we loop twice over its children. Moreover, this literal will be pruned for later calls.
This is correct, i.e. we can't prune too many literals because of a strongly connected component. Proof by contradiction: If we take the first (in direct_implications) literal from a removed SCC, it must have marked all the others. But because they are marked, they will not be explored again and so can't mark the first literal.

Now we can prune the direct implications list and make sure are the literals there are marked.

Definition at line 864 of file clause.cc.

◆ NextAtMostOne()

absl::Span< const Literal > operations_research::sat::BinaryImplicationGraph::NextAtMostOne ( )

Returns the next at_most_one, or a span of size 0 when finished.

Definition at line 2466 of file clause.cc.

◆ num_implications()

int64_t operations_research::sat::BinaryImplicationGraph::num_implications ( ) const

inline

Returns the number of current implications. Note that a => b and not(b) => not(a) are counted separately since they appear separately in our propagation lists. The number of size 2 clauses that represent the same thing is half this number.

Definition at line 696 of file clause.h.

◆ num_inspections()

int64_t operations_research::sat::BinaryImplicationGraph::num_inspections ( ) const

inline

Number of literals inspected by this class during propagation.

Definition at line 669 of file clause.h.

◆ num_literals_removed()

int64_t operations_research::sat::BinaryImplicationGraph::num_literals_removed ( ) const

inline

Definition at line 673 of file clause.h.

◆ num_minimization()

int64_t operations_research::sat::BinaryImplicationGraph::num_minimization ( ) const

inline

MinimizeClause() stats.

Definition at line 672 of file clause.h.

◆ num_propagations()

int64_t operations_research::sat::BinaryImplicationGraph::num_propagations ( ) const

inline

Number of literal propagated by this class (including conflicts).

Definition at line 666 of file clause.h.

◆ num_redundant_implications()

int64_t operations_research::sat::BinaryImplicationGraph::num_redundant_implications ( ) const

inline

Number of implications removed by transitive reduction.

Definition at line 688 of file clause.h.

◆ num_redundant_literals()

int64_t operations_research::sat::BinaryImplicationGraph::num_redundant_literals ( ) const

inline

Definition at line 682 of file clause.h.

◆ NumImplicationOnVariableRemoval()

int64_t operations_research::sat::BinaryImplicationGraph::NumImplicationOnVariableRemoval ( BooleanVariable var )

We should have dealt with that in FindFailedLiteralAroundVar().

l => literal => l: equivalent variable!

Definition at line 2237 of file clause.cc.

◆ operator=()

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

delete

◆ Propagate()

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

finalvirtual

SatPropagator interface.

Implements operations_research::sat::SatPropagator.

Definition at line 839 of file clause.cc.

◆ RandomImpliedLiteral()

LiteralIndex operations_research::sat::BinaryImplicationGraph::RandomImpliedLiteral ( Literal lhs )

Returns a random literal in DirectImplications(lhs). Note that this is biased if lhs appear in some most one, but it is constant time, which is a lot faster than computing DirectImplications() and then sampling from it.

We are unlucky and just picked the wrong literal: take a different one.

Definition at line 2185 of file clause.cc.

◆ Reason()

absl::Span< const Literal > operations_research::sat::BinaryImplicationGraph::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 852 of file clause.cc.

◆ RemoveAllRedundantVariables()

void operations_research::sat::BinaryImplicationGraph::RemoveAllRedundantVariables ( std::deque< std::vector< Literal > > * postsolve_clauses )

Definition at line 2308 of file clause.cc.

◆ RemoveBooleanVariable()

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

For all possible a => var => b, add a => b.

Notify the deletion to the proof checker and the postsolve.

Note: we want var first in these clauses for the postsolve.

We need to remove any occurrence of var in our implication lists, this will be delayed to the CleanupAllRemovedVariables() call.

Definition at line 2257 of file clause.cc.

◆ RemoveDuplicates()

void operations_research::sat::BinaryImplicationGraph::RemoveDuplicates ( )

Clean up implications list that might have duplicates.

Definition at line 519 of file clause.cc.

◆ RemoveFixedVariables()

void operations_research::sat::BinaryImplicationGraph::RemoveFixedVariables ( )

This must only be called at decision level 0 after all the possible propagations. It:

Removes the variable at true from the implications lists.
Frees the propagation list of the assigned literals.

Nothing to do if nothing changed since last call.

The code assumes that everything is already propagated. Otherwise we will remove implications that didn't propagate yet!

If b is true and a -> b then because not b -> not a, all the implications list that contains b will be marked by this process. And the ones that contains not(b) should correspond to a false literal!

Todo: (user): This might not be true if we remove implication by transitive reduction and the process was aborted due to the computation limit. I think it will be good to maintain that invariant though, otherwise fixed literals might never be removed from these lists...

We mark its representative instead.

Todo: (user): This might be a bit slow. Do not call all the time if needed, this shouldn't change the correctness of the code.

Definition at line 1076 of file clause.cc.

◆ RepresentativeOf()

Literal operations_research::sat::BinaryImplicationGraph::RepresentativeOf ( Literal l ) const

inline

Returns the representative of the equivalence class of l (or l itself if it is on its own). Note that DetectEquivalences() should have been called to get any non-trival results.

Definition at line 614 of file clause.h.

◆ ResetAtMostOneIterator()

void operations_research::sat::BinaryImplicationGraph::ResetAtMostOneIterator ( )

inline

Restarts the at_most_one iterator.

Definition at line 792 of file clause.h.

◆ ResetWorkDone()

void operations_research::sat::BinaryImplicationGraph::ResetWorkDone ( )

inline

ExpandAtMostOneWithWeight() will increase this, so a client can put a limit on this possibly expansive operation.

Definition at line 780 of file clause.h.

◆ Resize()

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

Resizes the data structure.

--— BinaryImplicationGraph --—

Definition at line 501 of file clause.cc.

◆ ReverseTopologicalOrder()

const std::vector< LiteralIndex > & operations_research::sat::BinaryImplicationGraph::ReverseTopologicalOrder ( ) const

inline

One must call DetectEquivalences() first, this is CHECKed. Returns a list so that if x => y, then x is after y.

Definition at line 600 of file clause.h.

◆ SetAdditionCallback()

void operations_research::sat::BinaryImplicationGraph::SetAdditionCallback ( std::function< void(Literal, Literal)> f )

inline

Definition at line 542 of file clause.h.

◆ SetDratProofHandler()

void operations_research::sat::BinaryImplicationGraph::SetDratProofHandler ( DratProofHandler * drat_proof_handler )

inline

Definition at line 727 of file clause.h.

◆ TransformIntoMaxCliques()

bool operations_research::sat::BinaryImplicationGraph::TransformIntoMaxCliques	(	std::vector< std::vector< Literal > > *	at_most_ones,
		int64_t	max_num_explored_nodes = 1e8 )

Another way of representing an implication graph is a list of maximal "at most one" constraints, each forming a max-clique in the incompatibility graph. This representation is useful for having a good linear relaxation.

This function will transform each of the given constraint into a maximal one in the underlying implication graph. Constraints that are redundant after other have been expanded (i.e. included into) will be cleared.

Note: the order of constraints will be conserved.

Returns false if the model is detected to be UNSAT (this needs to call DetectEquivalences() if not already done).

The code below assumes a DAG.

Data to detect inclusion of base amo into extend amo.

We starts by processing larger constraints first. But we want the output order to be stable.

Note(user): Because we always use literal with the smallest variable indices as representative, this make sure that if possible, we express the clique in term of user provided variable (that are always created first).

Remap the clique to only use representative.

We skip anything that can be presolved further as the code below do not handle duplicate well.

Todo: (user): Shall we presolve it here?

Special case for clique of size 2, we don't expand them if they are included in an already added clique.

Save the non-extended version as possible subset.

Todo: (user): Detect on the fly is superset already exist.

We only expand the clique as long as we didn't spend too much time.

Save the extended version as possible superset.

Also index clique for size 2 quick lookup.

Remove clique (before extension) that are included in an extended one.

Abort if one was already deleted.

If an extended clique already cover a deleted one, we cannot try to remove it by looking at its non-extended version.

Definition at line 1658 of file clause.cc.

◆ WorkDone()

int64_t operations_research::sat::BinaryImplicationGraph::WorkDone ( ) const

inline

Definition at line 781 of file clause.h.

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

ortools/sat/clause.h
ortools/sat/clause.cc

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ BinaryImplicationGraph() [1/2]

◆ BinaryImplicationGraph() [2/2]

◆ ~BinaryImplicationGraph()

Member Function Documentation

◆ AddAtMostOne()

◆ AddBinaryClause()

◆ AddImplication()

◆ ChangeReason()

◆ CleanupAllRemovedAndFixedVariables()

◆ ComputeTransitiveReduction()

◆ DetectEquivalences()

◆ DirectImplications()

◆ DirectImplicationsEstimatedSize()

◆ EnableSharing()

◆ ExpandAtMostOneWithWeight()

◆ ExtractAllBinaryClauses()

◆ FindFailedLiteralAroundVar()

◆ GenerateAtMostOnesWithLargeWeight()

◆ HeuristicAmoPartition()

◆ Implications()

◆ IsDag()

◆ IsEmpty()

◆ IsRedundant()

◆ IsRemoved()

◆ literal_size()

◆ MinimizeConflictExperimental()

◆ MinimizeConflictFirst()

◆ MinimizeConflictFirstWithTransitiveReduction()

◆ MinimizeConflictWithReachability()

◆ NextAtMostOne()

◆ num_implications()

◆ num_inspections()

◆ num_literals_removed()

◆ num_minimization()

◆ num_propagations()

◆ num_redundant_implications()

◆ num_redundant_literals()

◆ NumImplicationOnVariableRemoval()

◆ operator=()

◆ Propagate()

◆ RandomImpliedLiteral()

◆ Reason()

◆ RemoveAllRedundantVariables()

◆ RemoveBooleanVariable()

◆ RemoveDuplicates()

◆ RemoveFixedVariables()

◆ RepresentativeOf()

◆ ResetAtMostOneIterator()

◆ ResetWorkDone()

◆ Resize()

◆ ReverseTopologicalOrder()

◆ SetAdditionCallback()

◆ SetDratProofHandler()

◆ TransformIntoMaxCliques()

◆ WorkDone()