19 #ifndef OR_TOOLS_SAT_SAT_SOLVER_H_
20 #define OR_TOOLS_SAT_SAT_SOLVER_H_
29 #include "absl/container/flat_hash_map.h"
30 #include "absl/types/span.h"
44 #include "ortools/sat/sat_parameters.pb.h"
89 return BooleanVariable(num_vars);
125 bool use_upper_bound, Coefficient upper_bound,
126 std::vector<LiteralWithCoeff>* cst);
143 owned_propagators_.push_back(std::move(propagator));
160 const std::vector<std::pair<Literal, double>>& prefs) {
162 for (
const std::pair<Literal, double> p : prefs) {
209 const std::vector<Literal>& assumptions);
319 template <
typename Output>
327 if (num_processed_fixed_variables_ < trail_->
Index()) {
338 out->AddClause(clause->AsSpan());
359 const std::vector<Decision>&
Decisions()
const {
return decisions_; }
390 drat_proof_handler_ = drat_proof_handler;
425 current - deterministic_time_at_last_advanced_time_limit_);
426 deterministic_time_at_last_advanced_time_limit_ = current;
433 if (!decisions_.empty())
return decisions_[0].trail_index;
435 return trail_->
Index();
442 bool PropagateAndStopAfterOneConflictResolution();
454 bool ClauseIsValidUnderDebugAssignement(
455 const std::vector<Literal>& clause)
const;
456 bool PBConstraintIsValidUnderDebugAssignment(
457 const std::vector<LiteralWithCoeff>& cst,
const Coefficient rhs)
const;
465 Status SolveInternal(
int assumption_level);
482 Status ReapplyDecisionsUpTo(
int level,
int* first_propagation_index);
485 bool IsMemoryLimitReached()
const;
488 bool SetModelUnsat();
491 int DecisionLevel(BooleanVariable
var)
const {
498 SatClause* ReasonClauseOrNull(BooleanVariable
var)
const;
499 UpperBoundedLinearConstraint* ReasonPbConstraintOrNull(
500 BooleanVariable
var)
const;
511 bool ResolvePBConflict(BooleanVariable
var,
512 MutableUpperBoundedLinearConstraint* conflict,
521 bool ClauseIsUsedAsReason(SatClause* clause)
const {
522 const BooleanVariable
var = clause->PropagatedLiteral().Variable();
525 ReasonClauseOrNull(
var) == clause;
530 bool AddProblemClauseInternal(absl::Span<const Literal> literals);
535 bool AddLinearConstraintInternal(
const std::vector<LiteralWithCoeff>& cst,
536 Coefficient rhs, Coefficient max_value);
544 int AddLearnedClauseAndEnqueueUnitPropagation(
545 const std::vector<Literal>& literals,
bool is_redundant);
549 void EnqueueNewDecision(Literal
literal);
555 bool PropagationIsDone()
const;
558 void InitializePropagators();
562 void Untrail(
int target_trail_index);
565 void ProcessNewlyFixedVariablesForDratProof();
569 int ComputeMaxTrailIndex(absl::Span<const Literal> clause)
const;
583 void ComputeFirstUIPConflict(
584 int max_trail_index, std::vector<Literal>* conflict,
585 std::vector<Literal>* reason_used_to_infer_the_conflict,
586 std::vector<SatClause*>* subsumed_clauses);
591 void ComputeUnionOfReasons(
const std::vector<Literal>&
input,
592 std::vector<Literal>* literals);
599 void FillUnsatAssumptions(Literal false_assumption,
600 std::vector<Literal>* unsat_assumptions);
606 void ComputePBConflict(
int max_trail_index, Coefficient initial_slack,
607 MutableUpperBoundedLinearConstraint* conflict,
608 int* backjump_level);
618 void MinimizeConflict(
619 std::vector<Literal>* conflict,
620 std::vector<Literal>* reason_used_to_infer_the_conflict);
621 void MinimizeConflictExperimental(std::vector<Literal>* conflict);
622 void MinimizeConflictSimple(std::vector<Literal>* conflict);
623 void MinimizeConflictRecursively(std::vector<Literal>* conflict);
626 bool CanBeInferedFromConflictVariables(BooleanVariable variable);
633 bool IsConflictValid(
const std::vector<Literal>& literals);
637 int ComputeBacktrackLevel(
const std::vector<Literal>& literals);
652 template <
typename LiteralList>
653 int ComputeLbd(
const LiteralList& literals);
657 void CleanClauseDatabaseIfNeeded();
661 void BumpReasonActivities(
const std::vector<Literal>& literals);
662 void BumpClauseActivity(SatClause* clause);
663 void RescaleClauseActivities(
double scaling_factor);
664 void UpdateClauseActivityIncrement();
666 std::string DebugString(
const SatClause& clause)
const;
667 std::string StatusString(
Status status)
const;
668 std::string RunningStatisticsString()
const;
672 void KeepAllClauseUsedToInfer(BooleanVariable variable);
678 void TryToMinimizeClause(SatClause* clause);
682 std::unique_ptr<Model> owned_model_;
684 BooleanVariable num_variables_ = BooleanVariable(0);
688 BinaryImplicationGraph* binary_implication_graph_;
689 LiteralWatchers* clauses_propagator_;
690 PbConstraints* pb_constraints_;
693 std::vector<SatPropagator*> propagators_;
696 std::vector<SatPropagator*> external_propagators_;
697 SatPropagator* last_propagator_ =
nullptr;
700 std::vector<std::unique_ptr<SatPropagator>> owned_propagators_;
703 bool track_binary_clauses_;
704 BinaryClauseManager binary_clauses_;
708 TimeLimit* time_limit_;
709 SatParameters* parameters_;
710 RestartPolicy* restart_;
711 SatDecisionPolicy* decision_policy_;
714 VariablesAssignment debug_assignment_;
720 int current_decision_level_ = 0;
721 std::vector<Decision> decisions_;
725 int last_decision_or_backtrack_trail_index_ = 0;
728 int assumption_level_ = 0;
733 int num_processed_fixed_variables_ = 0;
734 double deterministic_time_of_last_fixed_variables_cleanup_ = 0.0;
737 int drat_num_processed_fixed_variables_ = 0;
746 int64 num_minimizations = 0;
747 int64 num_literals_removed = 0;
750 int64 num_learned_pb_literals = 0;
753 int64 num_literals_learned = 0;
754 int64 num_literals_forgotten = 0;
755 int64 num_subsumed_clauses = 0;
758 int64 minimization_num_clauses = 0;
759 int64 minimization_num_decisions = 0;
760 int64 minimization_num_true = 0;
761 int64 minimization_num_subsumed = 0;
762 int64 minimization_num_removed_literals = 0;
771 bool model_is_unsat_ =
false;
774 double clause_activity_increment_;
778 int num_learned_clause_before_cleanup_ = 0;
781 SparseBitset<BooleanVariable> is_marked_;
782 SparseBitset<BooleanVariable> is_independent_;
783 SparseBitset<BooleanVariable> tmp_mark_;
784 std::vector<int> min_trail_index_per_level_;
787 std::vector<BooleanVariable> dfs_stack_;
788 std::vector<BooleanVariable> variable_to_process_;
791 std::vector<Literal> literals_scratchpad_;
794 DEFINE_INT_TYPE(SatDecisionLevel,
int);
795 SparseBitset<SatDecisionLevel> is_level_marked_;
798 std::vector<Literal> learned_conflict_;
799 std::vector<Literal> reason_used_to_infer_the_conflict_;
800 std::vector<Literal> extra_reason_literals_;
801 std::vector<SatClause*> subsumed_clauses_;
808 bool block_clause_deletion_ =
false;
812 VariableWithSameReasonIdentifier same_reason_identifier_;
815 std::vector<LiteralWithCoeff> tmp_pb_constraint_;
818 bool is_relevant_for_core_computation_;
821 MutableUpperBoundedLinearConstraint pb_conflict_;
826 double deterministic_time_at_last_advanced_time_limit_ = 0;
829 bool problem_is_pure_sat_;
831 DratProofHandler* drat_proof_handler_;
833 mutable StatsGroup stats_;
844 void MinimizeCore(SatSolver* solver, std::vector<Literal>* core);
853 int64 lower_bound,
int64 upper_bound, std::vector<LiteralWithCoeff>* cst) {
856 true, Coefficient(lower_bound),
857 true, Coefficient(upper_bound), cst);
863 const std::vector<Literal>& literals) {
865 std::vector<LiteralWithCoeff> cst;
866 cst.reserve(literals.size());
867 for (
int i = 0; i < literals.size(); ++i) {
868 cst.emplace_back(literals[i], 1);
871 true, Coefficient(lower_bound),
872 true, Coefficient(upper_bound), &cst);
877 const std::vector<Literal>& literals) {
879 std::vector<LiteralWithCoeff> cst;
880 cst.reserve(literals.size());
881 for (
const Literal l : literals) {
882 cst.emplace_back(l, Coefficient(1));
885 true, Coefficient(1),
886 true, Coefficient(1), &cst);
891 const std::vector<Literal>& literals) {
893 std::vector<LiteralWithCoeff> cst;
894 cst.reserve(literals.size());
895 for (
const Literal l : literals) {
896 cst.emplace_back(l, Coefficient(1));
899 false, Coefficient(0),
900 true, Coefficient(1), &cst);
905 absl::Span<const Literal> literals) {
907 std::vector<LiteralWithCoeff> cst;
908 cst.reserve(literals.size());
909 for (
const Literal l : literals) {
910 cst.emplace_back(l, Coefficient(1));
913 true, Coefficient(1),
914 false, Coefficient(1), &cst);
935 const std::vector<Literal>& literals,
Literal r) {
937 std::vector<Literal> clause;
938 for (
const Literal l : literals) {
951 absl::Span<const Literal> enforcement_literals,
952 absl::Span<const Literal> clause) {
954 std::vector<Literal> tmp;
955 for (
const Literal l : enforcement_literals) {
956 tmp.push_back(l.Negated());
958 for (
const Literal l : clause) {
969 const std::vector<Literal>& literals,
Literal r) {
971 std::vector<Literal> clause;
972 for (
const Literal l : literals) {
974 clause.push_back(l.Negated());
1022 std::vector<Literal> clause_to_exclude_solution;
1023 clause_to_exclude_solution.reserve(current_level);
1024 for (
int i = 0; i < current_level; ++i) {
1025 clause_to_exclude_solution.push_back(
1026 sat_solver->
Decisions()[i].literal.Negated());
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
void ExtractAllBinaryClauses(Output *out) const
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
BooleanVariable Variable() const
const std::vector< SatClause * > & AllClausesInCreationOrder() const
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
bool IsRemovable(SatClause *const clause) const
void DeleteRemovedClauses()
Class that owns everything related to a particular optimization model.
std::vector< std::pair< Literal, double > > AllPreferences() const
void ResetDecisionHeuristic()
void SetAssignmentPreference(Literal literal, double weight)
const Trail & LiteralTrail() const
std::vector< std::pair< Literal, double > > AllPreferences() const
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
bool EnqueueDecisionIfNotConflicting(Literal true_literal)
void SetNumVariables(int num_variables)
bool AddTernaryClause(Literal a, Literal b, Literal c)
void AddLastPropagator(SatPropagator *propagator)
const SatParameters & parameters() const
void ResetDecisionHeuristicAndSetAllPreferences(const std::vector< std::pair< Literal, double >> &prefs)
void ResetDecisionHeuristic()
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
Status SolveWithTimeLimit(TimeLimit *time_limit)
void ProcessNewlyFixedVariables()
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions)
void AddPropagator(SatPropagator *propagator)
int64 NumFixedVariables() const
int64 num_failures() const
BooleanVariable NewBooleanVariable()
const std::vector< BinaryClause > & NewlyAddedBinaryClauses()
void NotifyThatModelIsUnsat()
int64 num_branches() const
bool AddBinaryClauses(const std::vector< BinaryClause > &clauses)
Status UnsatStatus() const
void SetAssumptionLevel(int assumption_level)
bool ProblemIsPureSat() const
void SaveDebugAssignment()
void AdvanceDeterministicTime(TimeLimit *limit)
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
int64 num_propagations() const
int AssumptionLevel() const
void MinimizeSomeClauses(int decisions_budget)
int64 num_restarts() const
void SetAssignmentPreference(Literal literal, double weight)
const VariablesAssignment & Assignment() const
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void SetParameters(const SatParameters ¶meters)
void TrackBinaryClauses(bool value)
bool AddBinaryClause(Literal a, Literal b)
void ExtractClauses(Output *out)
int EnqueueDecisionAndBacktrackOnConflict(Literal true_literal)
void Backtrack(int target_level)
bool RestoreSolverToAssumptionLevel()
std::vector< Literal > GetLastIncompatibleDecisions()
void TakePropagatorOwnership(std::unique_ptr< SatPropagator > propagator)
bool ReapplyAssumptionsIfNeeded()
bool IsModelUnsat() const
bool ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)
int CurrentDecisionLevel() const
double deterministic_time() const
bool AddProblemClause(absl::Span< const Literal > literals)
const std::vector< Decision > & Decisions() const
bool AddUnitClause(Literal true_literal)
void ClearNewlyAddedBinaryClauses()
const AssignmentInfo & Info(BooleanVariable var) const
const VariablesAssignment & Assignment() const
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
SharedTimeLimit * time_limit
std::function< void(Model *)> ReifiedBoolLe(Literal a, Literal b, Literal r)
std::function< void(Model *)> ExcludeCurrentSolutionAndBacktrack()
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
std::function< int64(const Model &)> Value(IntegerVariable v)
std::function< void(Model *)> BooleanLinearConstraint(int64 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst)
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
std::function< void(Model *)> EnforcedClause(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
std::string SatStatusString(SatSolver::Status status)
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
std::function< void(Model *)> AtMostOneConstraint(const std::vector< Literal > &literals)
std::function< void(Model *)> CardinalityConstraint(int64 lower_bound, int64 upper_bound, const std::vector< Literal > &literals)
const int kUnsatTrailIndex
std::function< void(Model *)> ReifiedBoolOr(const std::vector< Literal > &literals, Literal r)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
static int input(yyscan_t yyscanner)
Decision(int i, Literal l)