| AddAtMostOne(absl::Span< const Literal > at_most_one) | operations_research::sat::BinaryImplicationGraph | |
| AddBinaryClause(Literal a, Literal b) | operations_research::sat::BinaryImplicationGraph | |
| AddImplication(Literal a, Literal b) | operations_research::sat::BinaryImplicationGraph | inline |
| BinaryImplicationGraph(Model *model) | operations_research::sat::BinaryImplicationGraph | inlineexplicit |
| BinaryImplicationGraph(const BinaryImplicationGraph &)=delete | operations_research::sat::BinaryImplicationGraph | |
| ChangeReason(int trail_index, Literal new_reason) | operations_research::sat::BinaryImplicationGraph | inline |
| CleanupAllRemovedAndFixedVariables() | operations_research::sat::BinaryImplicationGraph | |
| ComputeNumImplicationsForLog() const | operations_research::sat::BinaryImplicationGraph | inline |
| ComputeTransitiveReduction(bool log_info=false) | operations_research::sat::BinaryImplicationGraph | |
| DetectEquivalences(bool log_info=false) | operations_research::sat::BinaryImplicationGraph | |
| DirectImplications(Literal literal) | operations_research::sat::BinaryImplicationGraph | |
| DirectImplicationsEstimatedSize(Literal literal) const | operations_research::sat::BinaryImplicationGraph | inline |
| EnableSharing(bool enable) | operations_research::sat::BinaryImplicationGraph | inline |
| 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) | operations_research::sat::BinaryImplicationGraph | |
| ExtractAllBinaryClauses(Output *out) const | operations_research::sat::BinaryImplicationGraph | inline |
| FindFailedLiteralAroundVar(BooleanVariable var, bool *is_unsat) | operations_research::sat::BinaryImplicationGraph | |
| GenerateAtMostOnesWithLargeWeight(absl::Span< const Literal > literals, absl::Span< const double > lp_values, absl::Span< const double > reduced_costs) | operations_research::sat::BinaryImplicationGraph | |
| GetAllImpliedLiterals(Literal root) | operations_research::sat::BinaryImplicationGraph | |
| HeuristicAmoPartition(std::vector< Literal > *literals) | operations_research::sat::BinaryImplicationGraph | |
| Implications(Literal l) const | operations_research::sat::BinaryImplicationGraph | inline |
| IsDag() const | operations_research::sat::BinaryImplicationGraph | inline |
| IsEmpty() const final | operations_research::sat::BinaryImplicationGraph | inlinevirtual |
| IsRedundant(Literal l) const | operations_research::sat::BinaryImplicationGraph | inline |
| IsRemoved(Literal l) const | operations_research::sat::BinaryImplicationGraph | inline |
| literal_size() const | operations_research::sat::BinaryImplicationGraph | inline |
| MergeAtMostOnes(absl::Span< std::vector< Literal > > at_most_ones, int64_t max_num_explored_nodes=1e8, double *dtime=nullptr) | operations_research::sat::BinaryImplicationGraph | |
| MinimizeConflictExperimental(const Trail &trail, std::vector< Literal > *c) | operations_research::sat::BinaryImplicationGraph | |
| MinimizeConflictFirst(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked) | operations_research::sat::BinaryImplicationGraph | |
| MinimizeConflictFirstWithTransitiveReduction(const Trail &trail, std::vector< Literal > *c, absl::BitGenRef random) | operations_research::sat::BinaryImplicationGraph | |
| MinimizeConflictWithReachability(std::vector< Literal > *c) | operations_research::sat::BinaryImplicationGraph | |
| name_ | operations_research::sat::SatPropagator | protected |
| NextAtMostOne() | operations_research::sat::BinaryImplicationGraph | |
| num_inspections() const | operations_research::sat::BinaryImplicationGraph | inline |
| num_literals_removed() const | operations_research::sat::BinaryImplicationGraph | inline |
| num_minimization() const | operations_research::sat::BinaryImplicationGraph | inline |
| num_propagations() const | operations_research::sat::BinaryImplicationGraph | inline |
| num_redundant_implications() const | operations_research::sat::BinaryImplicationGraph | inline |
| num_redundant_literals() const | operations_research::sat::BinaryImplicationGraph | inline |
| NumImplicationOnVariableRemoval(BooleanVariable var) | operations_research::sat::BinaryImplicationGraph | |
| operator=(const BinaryImplicationGraph &)=delete | operations_research::sat::BinaryImplicationGraph | |
| operations_research::sat::SatPropagator::operator=(const SatPropagator &)=delete | operations_research::sat::SatPropagator | |
| Propagate(Trail *trail) final | operations_research::sat::BinaryImplicationGraph | virtual |
| PropagatePreconditionsAreSatisfied(const Trail &trail) const | operations_research::sat::SatPropagator | inline |
| propagation_trail_index_ | operations_research::sat::SatPropagator | protected |
| PropagationIsDone(const Trail &trail) const | operations_research::sat::SatPropagator | inline |
| propagator_id_ | operations_research::sat::SatPropagator | protected |
| PropagatorId() const | operations_research::sat::SatPropagator | inline |
| RandomImpliedLiteral(Literal lhs) | operations_research::sat::BinaryImplicationGraph | |
| Reason(const Trail &trail, int trail_index, int64_t conflict_id) const final | operations_research::sat::BinaryImplicationGraph | virtual |
| RemoveAllRedundantVariables(std::deque< std::vector< Literal > > *postsolve_clauses) | operations_research::sat::BinaryImplicationGraph | |
| RemoveBooleanVariable(BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses) | operations_research::sat::BinaryImplicationGraph | |
| RemoveDuplicates() | operations_research::sat::BinaryImplicationGraph | |
| RemoveFixedVariables() | operations_research::sat::BinaryImplicationGraph | |
| RepresentativeOf(Literal l) const | operations_research::sat::BinaryImplicationGraph | inline |
| ResetAtMostOneIterator() | operations_research::sat::BinaryImplicationGraph | inline |
| ResetWorkDone() | operations_research::sat::BinaryImplicationGraph | inline |
| Resize(int num_variables) | operations_research::sat::BinaryImplicationGraph | |
| ReverseTopologicalOrder() const | operations_research::sat::BinaryImplicationGraph | inline |
| SatPropagator(const std::string &name) | operations_research::sat::SatPropagator | inlineexplicit |
| SatPropagator(const SatPropagator &)=delete | operations_research::sat::SatPropagator | |
| SetAdditionCallback(std::function< void(Literal, Literal)> f) | operations_research::sat::BinaryImplicationGraph | inline |
| SetDratProofHandler(DratProofHandler *drat_proof_handler) | operations_research::sat::BinaryImplicationGraph | inline |
| SetPropagatorId(int id) | operations_research::sat::SatPropagator | inline |
| TransformIntoMaxCliques(std::vector< std::vector< Literal > > *at_most_ones, int64_t max_num_explored_nodes=1e8) | operations_research::sat::BinaryImplicationGraph | |
| Untrail(const Trail &, int trail_index) | operations_research::sat::SatPropagator | inlinevirtual |
| WorkDone() const | operations_research::sat::BinaryImplicationGraph | inline |
| ~BinaryImplicationGraph() override | operations_research::sat::BinaryImplicationGraph | inline |
| ~SatPropagator()=default | operations_research::sat::SatPropagator | virtual |