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