19#ifndef OR_TOOLS_SAT_SAT_SOLVER_H_
20#define OR_TOOLS_SAT_SAT_SOLVER_H_
31#include "absl/base/attributes.h"
32#include "absl/log/check.h"
33#include "absl/types/span.h"
94 CHECK_LT(2 * num_vars, std::numeric_limits<int32_t>::max());
96 return BooleanVariable(num_vars);
139 bool use_upper_bound, Coefficient upper_bound,
140 std::vector<LiteralWithCoeff>* cst);
155 owned_propagators_.push_back(std::move(propagator));
163 decision_policy_->SetAssignmentPreference(literal, weight);
166 return decision_policy_->AllPreferences();
169 return decision_policy_->ResetDecisionHeuristic();
214 const std::vector<Literal>& assumptions,
215 int64_t max_number_of_conflicts = -1);
279 Literal true_literal,
int* first_propagation_index =
nullptr);
347 template <
typename Output>
353 if (num_processed_fixed_variables_ < trail_->Index()) {
356 clauses_propagator_->DeleteRemovedClauses();
361 binary_implication_graph_->ExtractAllBinaryClauses(out);
362 for (
SatClause* clause : clauses_propagator_->AllClausesInCreationOrder()) {
363 if (!clauses_propagator_->IsRemovable(clause)) {
364 out->AddClause(clause->AsSpan());
387 const std::vector<Decision>&
Decisions()
const {
return decisions_; }
447 drat_proof_handler_ = drat_proof_handler;
448 clauses_propagator_->SetDratProofHandler(drat_proof_handler_);
449 binary_implication_graph_->SetDratProofHandler(drat_proof_handler_);
474 bool minimize_new_clauses_only =
false);
481 current - deterministic_time_at_last_advanced_time_limit_);
482 deterministic_time_at_last_advanced_time_limit_ = current;
489 if (!decisions_.empty())
return decisions_[0].trail_index;
491 return trail_->Index();
506 clauses_propagator_->EnsureNewClauseIndexInitialized();
520 bool ClauseIsValidUnderDebugAssignment(
521 absl::Span<const Literal> clause)
const;
522 bool PBConstraintIsValidUnderDebugAssignment(
523 absl::Span<const LiteralWithCoeff> cst, Coefficient rhs)
const;
531 Status SolveInternal(
int assumption_level);
548 Status ReapplyDecisionsUpTo(
int level,
549 int* first_propagation_index =
nullptr);
552 bool IsMemoryLimitReached()
const;
555 bool SetModelUnsat();
558 int DecisionLevel(BooleanVariable var)
const {
565 SatClause* ReasonClauseOrNull(BooleanVariable var)
const;
566 UpperBoundedLinearConstraint* ReasonPbConstraintOrNull(
567 BooleanVariable var)
const;
578 bool ResolvePBConflict(BooleanVariable var,
579 MutableUpperBoundedLinearConstraint* conflict,
588 bool ClauseIsUsedAsReason(SatClause* clause)
const {
589 const BooleanVariable var = clause->PropagatedLiteral().Variable();
592 ReasonClauseOrNull(var) == clause;
597 bool AddProblemClauseInternal(absl::Span<const Literal> literals);
602 bool AddLinearConstraintInternal(
const std::vector<LiteralWithCoeff>& cst,
603 Coefficient rhs, Coefficient max_value);
606 void CanonicalizeLinear(std::vector<LiteralWithCoeff>* cst,
607 Coefficient* bound_shift, Coefficient* max_value);
615 int AddLearnedClauseAndEnqueueUnitPropagation(
616 const std::vector<Literal>& literals,
bool is_redundant);
620 void EnqueueNewDecision(Literal literal);
626 bool PropagationIsDone()
const;
629 void InitializePropagators();
632 void ProcessNewlyFixedVariablesForDratProof();
636 int ComputeMaxTrailIndex(absl::Span<const Literal> clause)
const;
650 void ComputeFirstUIPConflict(
651 int max_trail_index, std::vector<Literal>* conflict,
652 std::vector<Literal>* reason_used_to_infer_the_conflict,
653 std::vector<SatClause*>* subsumed_clauses);
658 void ComputeUnionOfReasons(absl::Span<const Literal>
input,
659 std::vector<Literal>* literals);
665 void ComputePBConflict(
int max_trail_index, Coefficient initial_slack,
666 MutableUpperBoundedLinearConstraint* conflict,
667 int* backjump_level);
677 void MinimizeConflict(std::vector<Literal>* conflict);
678 void MinimizeConflictExperimental(std::vector<Literal>* conflict);
679 void MinimizeConflictSimple(std::vector<Literal>* conflict);
680 void MinimizeConflictRecursively(std::vector<Literal>* conflict);
683 bool CanBeInferedFromConflictVariables(BooleanVariable variable);
690 bool IsConflictValid(absl::Span<const Literal> literals);
694 int ComputeBacktrackLevel(absl::Span<const Literal> literals);
709 template <
typename LiteralList>
710 int ComputeLbd(
const LiteralList& literals);
714 void CleanClauseDatabaseIfNeeded();
718 void BumpReasonActivities(absl::Span<const Literal> literals);
719 void BumpClauseActivity(SatClause* clause);
720 void RescaleClauseActivities(
double scaling_factor);
721 void UpdateClauseActivityIncrement();
723 std::string DebugString(
const SatClause& clause)
const;
724 std::string StatusString(
Status status)
const;
725 std::string RunningStatisticsString()
const;
730 bool SubsumptionIsInteresting(BooleanVariable variable,
int max_size);
731 void KeepAllClausesUsedToInfer(BooleanVariable variable);
737 void TryToMinimizeClause(SatClause* clause);
741 std::unique_ptr<Model> owned_model_;
743 BooleanVariable num_variables_ = BooleanVariable(0);
747 BinaryImplicationGraph* binary_implication_graph_;
748 ClauseManager* clauses_propagator_;
749 PbConstraints* pb_constraints_;
752 std::vector<SatPropagator*> propagators_;
753 std::vector<SatPropagator*> non_empty_propagators_;
756 std::vector<SatPropagator*> external_propagators_;
757 SatPropagator* last_propagator_ =
nullptr;
760 std::vector<std::unique_ptr<SatPropagator>> owned_propagators_;
763 bool track_binary_clauses_;
764 BinaryClauseManager binary_clauses_;
768 TimeLimit* time_limit_;
769 SatParameters* parameters_;
770 RestartPolicy* restart_;
771 SatDecisionPolicy* decision_policy_;
772 SolverLogger* logger_;
775 VariablesAssignment debug_assignment_;
781 int current_decision_level_ = 0;
782 std::vector<Decision> decisions_;
786 int last_decision_or_backtrack_trail_index_ = 0;
789 int assumption_level_ = 0;
790 std::vector<Literal> assumptions_;
795 int num_processed_fixed_variables_ = 0;
796 double deterministic_time_of_last_fixed_variables_cleanup_ = 0.0;
799 int drat_num_processed_fixed_variables_ = 0;
808 bool model_is_unsat_ =
false;
811 double clause_activity_increment_;
815 int num_learned_clause_before_cleanup_ = 0;
817 int64_t minimization_by_propagation_threshold_ = 0;
820 SparseBitset<BooleanVariable> is_marked_;
821 SparseBitset<BooleanVariable> is_independent_;
822 SparseBitset<BooleanVariable> tmp_mark_;
823 std::vector<int> min_trail_index_per_level_;
826 std::vector<BooleanVariable> dfs_stack_;
827 std::vector<BooleanVariable> variable_to_process_;
830 std::vector<Literal> literals_scratchpad_;
834 SparseBitset<SatDecisionLevel> is_level_marked_;
837 std::vector<Literal> learned_conflict_;
838 std::vector<Literal> reason_used_to_infer_the_conflict_;
839 std::vector<Literal> extra_reason_literals_;
840 std::vector<SatClause*> subsumed_clauses_;
847 bool block_clause_deletion_ =
false;
851 VariableWithSameReasonIdentifier same_reason_identifier_;
854 bool is_relevant_for_core_computation_;
857 MutableUpperBoundedLinearConstraint pb_conflict_;
862 double deterministic_time_at_last_advanced_time_limit_ = 0;
864 DratProofHandler* drat_proof_handler_;
866 mutable StatsGroup stats_;
887 int64_t lower_bound, int64_t upper_bound,
888 std::vector<LiteralWithCoeff>* cst) {
889 return [=](
Model* model) {
891 true, Coefficient(lower_bound),
892 true, Coefficient(upper_bound), cst);
897 int64_t lower_bound, int64_t upper_bound,
898 absl::Span<const Literal> literals) {
899 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
901 std::vector<LiteralWithCoeff> cst;
902 cst.reserve(literals.size());
903 for (
int i = 0;
i < literals.size(); ++
i) {
904 cst.emplace_back(literals[
i], 1);
907 true, Coefficient(lower_bound),
908 true, Coefficient(upper_bound), &cst);
913 absl::Span<const Literal> literals) {
914 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
916 std::vector<LiteralWithCoeff> cst;
917 cst.reserve(literals.size());
918 for (
const Literal l : literals) {
919 cst.emplace_back(l, Coefficient(1));
922 true, Coefficient(1),
923 true, Coefficient(1), &cst);
928 absl::Span<const Literal> literals) {
929 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
931 std::vector<LiteralWithCoeff> cst;
932 cst.reserve(literals.size());
933 for (
const Literal l : literals) {
934 cst.emplace_back(l, Coefficient(1));
937 false, Coefficient(0),
938 true, Coefficient(1), &cst);
943 absl::Span<const Literal> literals) {
951 return [=](
Model* model) {
957inline std::function<void(
Model*)>
Equality(Literal a, Literal
b) {
958 return [=](
Model* model) {
966 absl::Span<const Literal> literals, Literal r) {
967 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
969 std::vector<Literal> clause;
970 for (
const Literal l : literals) {
976 clause.push_back(r.Negated());
983 absl::Span<const Literal> enforcement_literals,
984 absl::Span<const Literal> clause) {
985 return [=](
Model* model) {
986 std::vector<Literal> tmp;
987 for (
const Literal l : enforcement_literals) {
988 tmp.push_back(l.Negated());
990 for (
const Literal l : clause) {
1001 absl::Span<const Literal> literals, Literal r) {
1002 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
1004 std::vector<Literal> clause;
1005 for (
const Literal l : literals) {
1007 clause.push_back(l.Negated());
1011 clause.push_back(r);
1027inline std::function<int64_t(
const Model&)>
Value(Literal l) {
1028 return [=](
const Model& model) {
1036inline std::function<int64_t(
const Model&)>
Value(BooleanVariable
b) {
1037 return [=](
const Model& model) {
1049 return [=](
Model* model) {
1055 std::vector<Literal> clause_to_exclude_solution;
1056 clause_to_exclude_solution.reserve(current_level);
1057 for (
int i = 0;
i < current_level; ++
i) {
1058 clause_to_exclude_solution.push_back(
1059 sat_solver->
Decisions()[
i].literal.Negated());
void AdvanceDeterministicTime(double deterministic_duration)
T Add(std::function< T(Model *)> f)
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
Base class for all the SAT constraints.
Status EnqueueDecisionAndBacktrackOnConflict(Literal true_literal, int *first_propagation_index=nullptr)
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
void LoadDebugSolution(absl::Span< const Literal > solution)
Status SolveWithTimeLimit(TimeLimit *time_limit)
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
double deterministic_time() const
const std::vector< BinaryClause > & NewlyAddedBinaryClauses()
SatSolver(const SatSolver &)=delete
This type is neither copyable nor movable.
bool MinimizeByPropagation(double dtime, bool minimize_new_clauses_only=false)
void ProcessCurrentConflict()
Status UnsatStatus() const
SolverLogger * mutable_logger()
Hack to allow to temporarily disable logging if it is enabled.
bool AddBinaryClauses(absl::Span< const BinaryClause > clauses)
void SetAssignmentPreference(Literal literal, float weight)
BooleanVariable NewBooleanVariable()
void ProcessNewlyFixedVariables()
Simplifies the problem when new variables are assigned at level 0.
bool ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)
int64_t num_branches() const
Some statistics since the creation of the solver.
void NotifyThatModelIsUnsat()
bool AddProblemClause(absl::Span< const Literal > literals)
std::vector< Literal > GetLastIncompatibleDecisions()
bool RestoreSolverToAssumptionLevel()
bool AddBinaryClause(Literal a, Literal b)
Same as AddProblemClause() below, but for small clauses.
void TrackBinaryClauses(bool value)
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void EnsureNewClauseIndexInitialized()
int64_t num_failures() const
void ResetDecisionHeuristic()
bool ModelIsUnsat() const
void Backtrack(int target_level)
bool ReapplyAssumptionsIfNeeded()
void ClearNewlyAddedBinaryClauses()
int64_t num_propagations() const
int64_t num_backtracks() const
const SatParameters & parameters() const
bool EnqueueDecisionIfNotConflicting(Literal true_literal)
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
ABSL_MUST_USE_RESULT bool Propagate()
bool ExtractClauses(Output *out)
std::vector< Literal > GetDecisionsFixing(absl::Span< const Literal > literals)
void SetAssumptionLevel(int assumption_level)
std::vector< std::pair< Literal, float > > AllPreferences() const
int64_t num_restarts() const
ABSL_MUST_USE_RESULT bool AddUnitClause(Literal true_literal)
bool AddTernaryClause(Literal a, Literal b, Literal c)
void TakePropagatorOwnership(std::unique_ptr< SatPropagator > propagator)
SatSolver & operator=(const SatSolver &)=delete
void AdvanceDeterministicTime(TimeLimit *limit)
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions, int64_t max_number_of_conflicts=-1)
const VariablesAssignment & Assignment() const
int CurrentDecisionLevel() const
int AssumptionLevel() const
ABSL_MUST_USE_RESULT bool ResetToLevelZero()
void SaveDebugAssignment()
void AddLastPropagator(SatPropagator *propagator)
const std::vector< Decision > & Decisions() const
ABSL_MUST_USE_RESULT bool FinishPropagation()
const Trail & LiteralTrail() const
void SetNumVariables(int num_variables)
Counters counters() const
int64_t NumFixedVariables() const
void AddPropagator(SatPropagator *propagator)
void SetParameters(const SatParameters ¶meters)
const AssignmentInfo & Info(BooleanVariable var) const
const VariablesAssignment & Assignment() const
bool VariableIsAssigned(BooleanVariable var) const
Returns true iff the given variable is assigned.
bool LiteralIsTrue(Literal literal) const
std::function< void(Model *)> Equality(IntegerVariable v, int64_t value)
Fix v to a given value.
std::string SatStatusString(SatSolver::Status status)
Returns a string representation of a SatSolver::Status.
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
std::function< void(Model *)> EnforcedClause(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
enforcement_literals => clause.
std::function< void(Model *)> ReifiedBoolLe(Literal a, Literal b, Literal r)
r <=> (a <= b).
std::function< void(Model *)> ReifiedBoolAnd(absl::Span< const Literal > literals, Literal r)
std::function< void(Model *)> Implication(absl::Span< const Literal > enforcement_literals, IntegerLiteral i)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
std::function< int64_t(const Model &)> Value(IntegerVariable v)
This checks that the variable is fixed.
std::function< void(Model *)> AtMostOneConstraint(absl::Span< const Literal > literals)
std::function< void(Model *)> CardinalityConstraint(int64_t lower_bound, int64_t upper_bound, absl::Span< const Literal > literals)
std::function< void(Model *)> ExactlyOneConstraint(absl::Span< const Literal > literals)
std::function< void(Model *)> BooleanLinearConstraint(int64_t lower_bound, int64_t upper_bound, std::vector< LiteralWithCoeff > *cst)
const int kUnsatTrailIndex
A constant used by the EnqueueDecision*() API.
std::function< void(Model *)> ReifiedBoolOr(absl::Span< const Literal > literals, Literal r)
r <=> (at least one literal is true). This is a reified clause.
std::function< void(Model *)> ExcludeCurrentSolutionAndBacktrack()
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
In SWIG mode, we don't want anything besides these top-level includes.
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
static int input(yyscan_t yyscanner)
#define DEFINE_STRONG_INDEX_TYPE(index_type_name)
int32_t trail_index
The index of this assignment in the trail.
int64_t minimization_num_true
int64_t num_subsumed_clauses
int64_t num_literals_forgotten
int64_t minimization_num_decisions
int64_t minimization_num_clauses
TryToMinimizeClause() stats.
int64_t num_minimizations
Minimization stats.
int64_t minimization_num_removed_literals
int64_t minimization_num_subsumed
int64_t num_literals_removed
int64_t minimization_num_reused
int64_t num_literals_learned
Clause learning /deletion stats.
int64_t num_learned_pb_literals
PB constraints.
Decision(int i, Literal l)