Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
operations_research::sat::SccGraph Class Reference

Detailed Description

Definition at line 1183 of file clause.cc.

Public Types

using Implications
using AtMostOnes
using SccFinder

Public Member Functions

 SccGraph (SccFinder *finder, Implications *graph, AtMostOnes *at_most_ones, std::vector< Literal > *at_most_one_buffer)
const std::vector< int32_t > & operator[] (int32_t node) const

Public Attributes

std::vector< Literalto_fix_
 All these literals where detected to be true during the SCC computation.
int64_t work_done_ = 0
 For the deterministic time.

Member Typedef Documentation

◆ AtMostOnes

◆ Implications

◆ SccFinder

Initial value:

Definition at line 1189 of file clause.cc.

Constructor & Destructor Documentation

◆ SccGraph()

operations_research::sat::SccGraph::SccGraph ( SccFinder * finder,
Implications * graph,
AtMostOnes * at_most_ones,
std::vector< Literal > * at_most_one_buffer )
inlineexplicit

Definition at line 1193 of file clause.cc.

Member Function Documentation

◆ operator[]()

const std::vector< int32_t > & operations_research::sat::SccGraph::operator[] ( int32_t node) const
inline

In the presence of at_most_ones_ constraints, expanding them implicitly to implications in the SCC computation can result in a quadratic complexity rather than a linear one in term of the input data structure size. So this test here is critical on problem with large at_most ones like the "ivu06-big.mps.gz" where without it, the full FindStronglyConnectedComponents() take more than on hour instead of less than a second!

We never expand a node twice.

If the first node is not settled, then we do explore the at_most_one constraint again. In "Mixed-Integer-Programming: Analyzing 12 years of progress", Tobias Achterberg and Roland Wunderling explains that an at most one need to be looped over at most twice. I am not sure exactly how that works, so for now we are not fully linear, but on actual instances, we only rarely run into this case.

Note
we change the previous node to explore at most one since the current node will be settled before the old ones.
Todo
(user): avoid looping more than twice on the same at most one constraints? Note that the second time we loop we have x => y => not(x), so we can already detect that x must be false which we detect below.

The first node is already settled and so are all its child. Only not(first_node) might still need exploring.

Definition at line 1201 of file clause.cc.

Member Data Documentation

◆ to_fix_

std::vector<Literal> operations_research::sat::SccGraph::to_fix_
mutable

All these literals where detected to be true during the SCC computation.

Definition at line 1274 of file clause.cc.

◆ work_done_

int64_t operations_research::sat::SccGraph::work_done_ = 0
mutable

For the deterministic time.

Definition at line 1277 of file clause.cc.


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