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 | |
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(const std::vector< Literal > &literals, const std::vector< double > &lp_values) | 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 |
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_implications() const | operations_research::sat::BinaryImplicationGraph | inline |
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 |