#include <presolve_util.h>

Public Member Functions
void	AddDeduction (int literal_ref, int var, Domain domain)

Domain	ImpliedDomain (int literal_ref, int var) const

std::vector< std::pair< int, Domain > >	ProcessClause (absl::Span< const int > clause)

void	MarkProcessingAsDoneForNow ()

int	NumDeductions () const
	Returns the total number of "deductions" stored by this class.

Detailed Description

If for each literal of a clause, we can infer a domain on an integer variable, then we know that this variable domain is included in the union of such infered domains.

This allows to propagate "element" like constraints encoded as enforced linear relations, and other more general reasoning.

Todo: (user): Also use these "deductions" in the solver directly. This is done in good MIP solvers, and we should exploit them more.

Todo: (user): Also propagate implicit clauses (lit, not(lit)). Maybe merge that with probing code? it might be costly to store all deduction done by probing though, but I think this is what MIP solver do.

Definition at line 100 of file presolve_util.h.

Member Function Documentation

◆ AddDeduction()

void operations_research::sat::DomainDeductions::AddDeduction	(	int	literal_ref,
		int	var,
		Domain	domain )

Adds the fact that enforcement => var \in domain.

Important: No need to store any deductions where the domain is a superset of the current variable domain.

New element.

Existing element.

Definition at line 66 of file presolve_util.cc.

◆ ImpliedDomain()

Domain operations_research::sat::DomainDeductions::ImpliedDomain	(	int	literal_ref,
		int	var ) const

Returns the domain of var when literal_ref is true. If there is no information, returns Domain::AllValues().

Definition at line 91 of file presolve_util.cc.

◆ MarkProcessingAsDoneForNow()

void operations_research::sat::DomainDeductions::MarkProcessingAsDoneForNow ( )

inline

Optimization. Any following ProcessClause() will be fast if no more deduction touching that clause are added.

Definition at line 124 of file presolve_util.h.

◆ NumDeductions()

int operations_research::sat::DomainDeductions::NumDeductions ( ) const

inline

Returns the total number of "deductions" stored by this class.

Definition at line 129 of file presolve_util.h.

◆ ProcessClause()

std::vector< std::pair< int, Domain > > operations_research::sat::DomainDeductions::ProcessClause ( absl::Span< const int > clause )

Returns list of (var, domain) that were deduced because: 1/ We have a domain deduction for var and all literal from the clause 2/ So we can take the union of all the deduced domains.

Todo: (user): We could probably be even more efficient. We could also compute exactly what clauses need to be "waked up" as new deductions are added.

We only need to process this clause if something changed since last time.

Count for each variable, how many times it appears in the deductions lists.

Clear the counts.

Compute the domain unions.

Definition at line 99 of file presolve_util.cc.

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

ortools/sat/presolve_util.h
ortools/sat/presolve_util.cc