|
void | MinimizeCore (SatSolver *solver, std::vector< Literal > *core) |
|
std::function< void(Model *)> | BooleanLinearConstraint (int64 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst) |
|
std::function< void(Model *)> | CardinalityConstraint (int64 lower_bound, int64 upper_bound, const std::vector< Literal > &literals) |
|
std::function< void(Model *)> | ExactlyOneConstraint (const std::vector< Literal > &literals) |
|
std::function< void(Model *)> | AtMostOneConstraint (const std::vector< Literal > &literals) |
|
std::function< void(Model *)> | ClauseConstraint (absl::Span< const Literal > literals) |
|
std::function< void(Model *)> | Implication (Literal a, Literal b) |
|
std::function< void(Model *)> | Equality (Literal a, Literal b) |
|
std::function< void(Model *)> | ReifiedBoolOr (const std::vector< Literal > &literals, Literal r) |
|
std::function< void(Model *)> | EnforcedClause (absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause) |
|
std::function< void(Model *)> | ReifiedBoolAnd (const std::vector< Literal > &literals, Literal r) |
|
std::function< void(Model *)> | ReifiedBoolLe (Literal a, Literal b, Literal r) |
|
std::function< int64(const Model &)> | Value (Literal l) |
|
std::function< int64(const Model &)> | Value (BooleanVariable b) |
|
std::function< void(Model *)> | ExcludeCurrentSolutionAndBacktrack () |
|
std::string | SatStatusString (SatSolver::Status status) |
|
std::ostream & | operator<< (std::ostream &os, SatSolver::Status status) |
|