AddAtMostOne(absl::Span< const Literal > at_most_one) | BinaryImplicationGraph | |
AddBinaryClause(Literal a, Literal b) | BinaryImplicationGraph | |
AddBinaryClauseDuringSearch(Literal a, Literal b) | BinaryImplicationGraph | |
AddImplication(Literal a, Literal b) | BinaryImplicationGraph | inline |
BinaryImplicationGraph(Model *model) | BinaryImplicationGraph | inlineexplicit |
ChangeReason(int trail_index, Literal new_reason) | BinaryImplicationGraph | inline |
CleanupAllRemovedVariables() | BinaryImplicationGraph | |
ComputeTransitiveReduction(bool log_info=false) | BinaryImplicationGraph | |
DetectEquivalences(bool log_info=false) | BinaryImplicationGraph | |
DirectImplications(Literal literal) | BinaryImplicationGraph | |
DirectImplicationsEstimatedSize(Literal literal) const | BinaryImplicationGraph | inline |
ExtractAllBinaryClauses(Output *out) const | BinaryImplicationGraph | inline |
FindFailedLiteralAroundVar(BooleanVariable var, bool *is_unsat) | BinaryImplicationGraph | |
GenerateAtMostOnesWithLargeWeight(const std::vector< Literal > &literals, const std::vector< double > &lp_values) | BinaryImplicationGraph | |
Implications(Literal l) const | BinaryImplicationGraph | inline |
IsDag() const | BinaryImplicationGraph | inline |
IsEmpty() | BinaryImplicationGraph | inline |
IsRedundant(Literal l) const | BinaryImplicationGraph | inline |
IsRemoved(Literal l) const | BinaryImplicationGraph | inline |
literal_size() const | BinaryImplicationGraph | inline |
MinimizeConflictExperimental(const Trail &trail, std::vector< Literal > *c) | BinaryImplicationGraph | |
MinimizeConflictFirst(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked) | BinaryImplicationGraph | |
MinimizeConflictFirstWithTransitiveReduction(const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked, absl::BitGenRef random) | BinaryImplicationGraph | |
MinimizeConflictWithReachability(std::vector< Literal > *c) | BinaryImplicationGraph | |
name_ | SatPropagator | protected |
num_implications() const | BinaryImplicationGraph | inline |
num_inspections() const | BinaryImplicationGraph | inline |
num_literals_removed() const | BinaryImplicationGraph | inline |
num_minimization() const | BinaryImplicationGraph | inline |
num_propagations() const | BinaryImplicationGraph | inline |
num_redundant_implications() const | BinaryImplicationGraph | inline |
num_redundant_literals() const | BinaryImplicationGraph | inline |
NumImplicationOnVariableRemoval(BooleanVariable var) | BinaryImplicationGraph | |
Propagate(Trail *trail) final | BinaryImplicationGraph | virtual |
PropagatePreconditionsAreSatisfied(const Trail &trail) const | SatPropagator | inline |
propagation_trail_index_ | SatPropagator | protected |
PropagationIsDone(const Trail &trail) const | SatPropagator | inline |
propagator_id_ | SatPropagator | protected |
PropagatorId() const | SatPropagator | inline |
Reason(const Trail &trail, int trail_index) const final | BinaryImplicationGraph | virtual |
RemoveBooleanVariable(BooleanVariable var, std::deque< std::vector< Literal >> *postsolve_clauses) | BinaryImplicationGraph | |
RemoveFixedVariables() | BinaryImplicationGraph | |
RepresentativeOf(Literal l) const | BinaryImplicationGraph | inline |
Resize(int num_variables) | BinaryImplicationGraph | |
ReverseTopologicalOrder() const | BinaryImplicationGraph | inline |
SatPropagator(const std::string &name) | SatPropagator | inlineexplicit |
SetDratProofHandler(DratProofHandler *drat_proof_handler) | BinaryImplicationGraph | inline |
SetPropagatorId(int id) | SatPropagator | inline |
TransformIntoMaxCliques(std::vector< std::vector< Literal >> *at_most_ones, int64 max_num_explored_nodes=1e8) | BinaryImplicationGraph | |
Untrail(const Trail &trail, int trail_index) | SatPropagator | inlinevirtual |
~BinaryImplicationGraph() override | BinaryImplicationGraph | inline |
~SatPropagator() | SatPropagator | inlinevirtual |