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/container/flat_hash_map.h"
33#include "absl/log/check.h"
34#include "absl/strings/string_view.h"
35#include "absl/types/span.h"
47#include "ortools/sat/sat_parameters.pb.h"
98 CHECK_LT(2 * num_vars, std::numeric_limits<int32_t>::max());
100 return BooleanVariable(num_vars);
122 bool is_safe =
true);
139 std::vector<LiteralWithCoeff>* cst);
157 owned_propagators_.push_back(std::move(propagator));
216 const std::vector<Literal>& assumptions,
217 int64_t max_number_of_conflicts = -1);
277 Literal true_literal,
int* first_propagation_index =
nullptr);
345 template <
typename Output>
353 if (num_processed_fixed_variables_ < trail_->Index()) {
364 out->AddClause(clause->AsSpan());
385 const std::vector<Decision>&
Decisions()
const {
return decisions_; }
446 drat_proof_handler_ = drat_proof_handler;
479 current - deterministic_time_at_last_advanced_time_limit_);
480 deterministic_time_at_last_advanced_time_limit_ = current;
487 if (!decisions_.empty())
return decisions_[0].trail_index;
489 return trail_->
Index();
514 bool ClauseIsValidUnderDebugAssignment(
515 absl::Span<const Literal> clause)
const;
516 bool PBConstraintIsValidUnderDebugAssignment(
517 const std::vector<LiteralWithCoeff>& cst, Coefficient rhs)
const;
525 Status SolveInternal(
int assumption_level);
542 Status ReapplyDecisionsUpTo(
int level,
543 int* first_propagation_index =
nullptr);
546 bool IsMemoryLimitReached()
const;
549 bool SetModelUnsat();
552 int DecisionLevel(BooleanVariable
var)
const {
559 SatClause* ReasonClauseOrNull(BooleanVariable
var)
const;
560 UpperBoundedLinearConstraint* ReasonPbConstraintOrNull(
561 BooleanVariable
var)
const;
572 bool ResolvePBConflict(BooleanVariable
var,
573 MutableUpperBoundedLinearConstraint* conflict,
582 bool ClauseIsUsedAsReason(SatClause* clause)
const {
583 const BooleanVariable
var = clause->PropagatedLiteral().Variable();
586 ReasonClauseOrNull(
var) == clause;
591 bool AddProblemClauseInternal(absl::Span<const Literal> literals);
596 bool AddLinearConstraintInternal(
const std::vector<LiteralWithCoeff>& cst,
597 Coefficient rhs, Coefficient max_value);
600 void CanonicalizeLinear(std::vector<LiteralWithCoeff>* cst,
601 Coefficient* bound_shift, Coefficient* max_value);
609 int AddLearnedClauseAndEnqueueUnitPropagation(
610 const std::vector<Literal>& literals,
bool is_redundant);
614 void EnqueueNewDecision(Literal
literal);
620 bool PropagationIsDone()
const;
623 void InitializePropagators();
626 void ProcessNewlyFixedVariablesForDratProof();
630 int ComputeMaxTrailIndex(absl::Span<const Literal> clause)
const;
644 void ComputeFirstUIPConflict(
645 int max_trail_index, std::vector<Literal>* conflict,
646 std::vector<Literal>* reason_used_to_infer_the_conflict,
647 std::vector<SatClause*>* subsumed_clauses);
652 void ComputeUnionOfReasons(
const std::vector<Literal>&
input,
653 std::vector<Literal>* literals);
659 void ComputePBConflict(
int max_trail_index, Coefficient initial_slack,
660 MutableUpperBoundedLinearConstraint* conflict,
661 int* backjump_level);
671 void MinimizeConflict(std::vector<Literal>* conflict);
672 void MinimizeConflictExperimental(std::vector<Literal>* conflict);
673 void MinimizeConflictSimple(std::vector<Literal>* conflict);
674 void MinimizeConflictRecursively(std::vector<Literal>* conflict);
677 bool CanBeInferedFromConflictVariables(BooleanVariable variable);
684 bool IsConflictValid(
const std::vector<Literal>& literals);
688 int ComputeBacktrackLevel(
const std::vector<Literal>& literals);
703 template <
typename LiteralList>
704 int ComputeLbd(
const LiteralList& literals);
708 void CleanClauseDatabaseIfNeeded();
712 void BumpReasonActivities(
const std::vector<Literal>& literals);
713 void BumpClauseActivity(SatClause* clause);
714 void RescaleClauseActivities(
double scaling_factor);
715 void UpdateClauseActivityIncrement();
717 std::string DebugString(
const SatClause& clause)
const;
719 std::string RunningStatisticsString()
const;
723 void KeepAllClauseUsedToInfer(BooleanVariable variable);
724 bool SubsumptionIsInteresting(BooleanVariable variable);
730 void TryToMinimizeClause(SatClause* clause);
734 std::unique_ptr<Model> owned_model_;
736 BooleanVariable num_variables_ = BooleanVariable(0);
740 BinaryImplicationGraph* binary_implication_graph_;
741 ClauseManager* clauses_propagator_;
742 PbConstraints* pb_constraints_;
745 std::vector<SatPropagator*> propagators_;
746 std::vector<SatPropagator*> non_empty_propagators_;
749 std::vector<SatPropagator*> external_propagators_;
750 SatPropagator* last_propagator_ =
nullptr;
753 std::vector<std::unique_ptr<SatPropagator>> owned_propagators_;
756 bool track_binary_clauses_;
757 BinaryClauseManager binary_clauses_;
761 TimeLimit* time_limit_;
762 SatParameters* parameters_;
763 RestartPolicy* restart_;
764 SatDecisionPolicy* decision_policy_;
765 SolverLogger* logger_;
768 VariablesAssignment debug_assignment_;
774 int current_decision_level_ = 0;
775 std::vector<Decision> decisions_;
779 int last_decision_or_backtrack_trail_index_ = 0;
782 int assumption_level_ = 0;
783 std::vector<Literal> assumptions_;
788 int num_processed_fixed_variables_ = 0;
789 double deterministic_time_of_last_fixed_variables_cleanup_ = 0.0;
792 int drat_num_processed_fixed_variables_ = 0;
801 bool model_is_unsat_ =
false;
804 double clause_activity_increment_;
808 int num_learned_clause_before_cleanup_ = 0;
810 int64_t minimization_by_propagation_threshold_ = 0;
813 SparseBitset<BooleanVariable> is_marked_;
814 SparseBitset<BooleanVariable> is_independent_;
815 SparseBitset<BooleanVariable> tmp_mark_;
816 std::vector<int> min_trail_index_per_level_;
819 std::vector<BooleanVariable> dfs_stack_;
820 std::vector<BooleanVariable> variable_to_process_;
823 std::vector<Literal> literals_scratchpad_;
827 SparseBitset<SatDecisionLevel> is_level_marked_;
830 std::vector<Literal> learned_conflict_;
831 std::vector<Literal> reason_used_to_infer_the_conflict_;
832 std::vector<Literal> extra_reason_literals_;
833 std::vector<SatClause*> subsumed_clauses_;
840 bool block_clause_deletion_ =
false;
844 VariableWithSameReasonIdentifier same_reason_identifier_;
847 bool is_relevant_for_core_computation_;
850 MutableUpperBoundedLinearConstraint pb_conflict_;
855 double deterministic_time_at_last_advanced_time_limit_ = 0;
858 bool problem_is_pure_sat_;
860 DratProofHandler* drat_proof_handler_;
862 mutable StatsGroup stats_;
874void MinimizeCore(SatSolver* solver, std::vector<Literal>* core);
884 std::vector<LiteralWithCoeff>* cst) {
894 const std::vector<Literal>& literals) {
896 std::vector<LiteralWithCoeff> cst;
897 cst.reserve(literals.size());
898 for (
int i = 0;
i < literals.size(); ++
i) {
899 cst.emplace_back(literals[
i], 1);
908 const std::vector<Literal>& literals) {
910 std::vector<LiteralWithCoeff> cst;
911 cst.reserve(literals.size());
912 for (
const Literal l : literals) {
913 cst.emplace_back(l, Coefficient(1));
916 true, Coefficient(1),
917 true, Coefficient(1), &cst);
922 const std::vector<Literal>& literals) {
924 std::vector<LiteralWithCoeff> cst;
925 cst.reserve(literals.size());
926 for (
const Literal l : literals) {
927 cst.emplace_back(l, Coefficient(1));
930 false, Coefficient(0),
931 true, Coefficient(1), &cst);
936 absl::Span<const Literal> literals) {
944inline std::function<void(Model*)>
Implication(Literal
a, Literal
b) {
945 return [=](Model*
model) {
951inline std::function<void(Model*)>
Equality(Literal
a, Literal
b) {
952 return [=](Model*
model) {
960 const std::vector<Literal>& literals, Literal r) {
962 std::vector<Literal> clause;
963 for (
const Literal l : literals) {
969 clause.push_back(r.Negated());
976 absl::Span<const Literal> enforcement_literals,
977 absl::Span<const Literal> clause) {
979 std::vector<Literal> tmp;
980 for (
const Literal l : enforcement_literals) {
981 tmp.push_back(l.Negated());
983 for (
const Literal l : clause) {
994 const std::vector<Literal>& literals, Literal r) {
996 std::vector<Literal> clause;
997 for (
const Literal l : literals) {
999 clause.push_back(l.Negated());
1003 clause.push_back(r);
1019inline std::function<int64_t(
const Model&)>
Value(Literal l) {
1020 return [=](
const Model&
model) {
1028inline std::function<int64_t(
const Model&)>
Value(BooleanVariable
b) {
1029 return [=](
const Model&
model) {
1041 return [=](Model*
model) {
1047 std::vector<Literal> clause_to_exclude_solution;
1048 clause_to_exclude_solution.reserve(current_level);
1049 for (
int i = 0;
i < current_level; ++
i) {
1050 clause_to_exclude_solution.push_back(
1051 sat_solver->
Decisions()[
i].literal.Negated());
void AdvanceDeterministicTime(double deterministic_duration)
void ExtractAllBinaryClauses(Output *out) const
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
bool IsRemovable(SatClause *const clause) const
void DeleteRemovedClauses()
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
const std::vector< SatClause * > & AllClausesInCreationOrder() const
std::vector< std::pair< Literal, float > > AllPreferences() const
Returns the vector of the current assignment preferences.
void SetAssignmentPreference(Literal literal, float weight)
void ResetDecisionHeuristic()
Base class for all the SAT constraints.
void ExtractClauses(Output *out)
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)
Status SolveWithTimeLimit(TimeLimit *time_limit)
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
double deterministic_time() const
bool AddBinaryClauses(const std::vector< BinaryClause > &clauses)
bool AddProblemClause(absl::Span< const Literal > literals, bool is_safe=true)
bool MinimizeByPropagation(double dtime)
const std::vector< BinaryClause > & NewlyAddedBinaryClauses()
SatSolver(const SatSolver &)=delete
This type is neither copyable nor movable.
void ProcessCurrentConflict()
Status UnsatStatus() const
SolverLogger * mutable_logger()
Hack to allow to temporarily disable logging if it is enabled.
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 LoadDebugSolution(const std::vector< Literal > &solution)
void NotifyThatModelIsUnsat()
bool ProblemIsPureSat() const
Returns true iff the loaded problem only contains clauses.
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)
int64_t num_failures() const
void ResetDecisionHeuristic()
bool ModelIsUnsat() const
void Backtrack(int target_level)
bool ReapplyAssumptionsIfNeeded()
void ClearNewlyAddedBinaryClauses()
int64_t num_propagations() const
bool IsModelUnsat() const
const SatParameters & parameters() const
bool EnqueueDecisionIfNotConflicting(Literal true_literal)
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
ABSL_MUST_USE_RESULT bool Propagate()
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::unique_ptr< SharedClausesManager > clauses
std::function< void(Model *) ReifiedBoolOr)(const std::vector< Literal > &literals, Literal r)
r <=> (at least one literal is true). This is a reified clause.
std::string SatStatusString(SatSolver::Status status)
Returns a string representation of a SatSolver::Status.
std::function< void(Model *) AtMostOneConstraint)(const std::vector< Literal > &literals)
std::function< void(Model *) Equality)(IntegerVariable v, int64_t value)
Fix v to a given value.
std::function< int64_t(const Model &) Value)(IntegerVariable v)
This checks that the variable is fixed.
std::function< void(Model *) ClauseConstraint)(absl::Span< const Literal > literals)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
std::function< void(Model *) ReifiedBoolLe)(Literal a, Literal b, Literal r)
r <=> (a <= b).
std::function< void(Model *) EnforcedClause)(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
enforcement_literals => clause.
std::function< void(Model *) Implication)(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
a => b.
std::function< void(Model *) BooleanLinearConstraint)(int64_t lower_bound, int64_t upper_bound, std::vector< LiteralWithCoeff > *cst)
std::function< void(Model *) ExactlyOneConstraint)(const std::vector< Literal > &literals)
const int kUnsatTrailIndex
A constant used by the EnqueueDecision*() API.
std::function< void(Model *) ReifiedBoolAnd)(const std::vector< Literal > &literals, Literal r)
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
std::function< void(Model *) ExcludeCurrentSolutionAndBacktrack)()
std::function< void(Model *) CardinalityConstraint)(int64_t lower_bound, int64_t upper_bound, const std::vector< Literal > &literals)
In SWIG mode, we don't want anything besides these top-level includes.
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)