Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
sat_solver.h
Go to the documentation of this file.
1// Copyright 2010-2025 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14// This file implements a SAT solver.
15// see http://en.wikipedia.org/wiki/Boolean_satisfiability_problem
16// for more detail.
17// TODO(user): Expand.
18
19#ifndef OR_TOOLS_SAT_SAT_SOLVER_H_
20#define OR_TOOLS_SAT_SAT_SOLVER_H_
21
22#include <cstdint>
23#include <functional>
24#include <limits>
25#include <memory>
26#include <ostream>
27#include <string>
28#include <utility>
29#include <vector>
30
31#include "absl/base/attributes.h"
32#include "absl/log/check.h"
33#include "absl/types/span.h"
35#include "ortools/base/timer.h"
36#include "ortools/sat/clause.h"
38#include "ortools/sat/model.h"
40#include "ortools/sat/restart.h"
44#include "ortools/util/bitset.h"
46#include "ortools/util/stats.h"
49
50namespace operations_research {
51namespace sat {
52
53// A constant used by the EnqueueDecision*() API.
54const int kUnsatTrailIndex = -1;
55
56// The main SAT solver.
57// It currently implements the CDCL algorithm. See
58// http://en.wikipedia.org/wiki/Conflict_Driven_Clause_Learning
59class SatSolver {
60 public:
61 SatSolver();
62 explicit SatSolver(Model* model);
63
64 // This type is neither copyable nor movable.
65 SatSolver(const SatSolver&) = delete;
66 SatSolver& operator=(const SatSolver&) = delete;
67
68 ~SatSolver();
69
70 // TODO(user): Remove. This is temporary for accessing the model deep within
71 // some old code that didn't use the Model object.
72 Model* model() { return model_; }
73
74 // Parameters management. Note that calling SetParameters() will reset the
75 // value of many heuristics. For instance:
76 // - The restart strategy will be reinitialized.
77 // - The random seed and random generator will be reset to the value given in
78 // parameters.
79 // - The global TimeLimit singleton will be reset and time will be
80 // counted from this call.
82 const SatParameters& parameters() const;
83
84 // Increases the number of variables of the current problem.
85 //
86 // TODO(user): Rename to IncreaseNumVariablesTo() until we support removing
87 // variables...
88 void SetNumVariables(int num_variables);
89 int NumVariables() const { return num_variables_.value(); }
90 BooleanVariable NewBooleanVariable() {
91 const int num_vars = NumVariables();
92
93 // We need to be able to encode the variable as a literal.
94 CHECK_LT(2 * num_vars, std::numeric_limits<int32_t>::max());
95 SetNumVariables(num_vars + 1);
96 return BooleanVariable(num_vars);
97 }
98
99 // Fixes a variable so that the given literal is true. This can be used to
100 // solve a subproblem where some variables are fixed. Note that it is more
101 // efficient to add such unit clause before all the others.
102 // Returns false if the problem is detected to be UNSAT.
103 ABSL_MUST_USE_RESULT bool AddUnitClause(Literal true_literal);
104
105 // Same as AddProblemClause() below, but for small clauses.
108
109 // Adds a clause to the problem.
110 // Returns false if the problem is detected to be UNSAT.
111 //
112 // This must only be called at level zero, use AddClauseDuringSearch() for
113 // adding clause at a positive level.
114 //
115 // We call this a "problem" clause just because we will never delete such
116 // clause unless it is proven to always be satisfied. So this can be called
117 // with the initial clause of a problem, but also infered clause that we
118 // don't want to delete.
119 //
120 // TODO(user): Rename this to AddClause() ? Also get rid of the specialized
121 // AddUnitClause(), AddBinaryClause() and AddTernaryClause() since they
122 // just end up calling this?
123 bool AddProblemClause(absl::Span<const Literal> literals);
124
125 // Adds a pseudo-Boolean constraint to the problem. Returns false if the
126 // problem is detected to be UNSAT. If the constraint is always true, this
127 // detects it and does nothing.
128 //
129 // Note(user): There is an optimization if the same constraint is added
130 // consecutively (even if the bounds are different). This is particularly
131 // useful for an optimization problem when we want to constrain the objective
132 // of the problem more and more. Just re-adding such constraint is relatively
133 // efficient.
134 //
135 // OVERFLOW: The sum of the absolute value of all the coefficients
136 // in the constraint must not overflow. This is currently CHECKed().
137 // TODO(user): Instead of failing, implement an error handling code.
138 bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound,
139 bool use_upper_bound, Coefficient upper_bound,
140 std::vector<LiteralWithCoeff>* cst);
141
142 // Returns true if the model is UNSAT. Note that currently the status is
143 // "sticky" and once this happen, nothing else can be done with the solver.
144 //
145 // Thanks to this function, a client can safely ignore the return value of any
146 // Add*() functions. If one of them return false, then ModelIsUnsat() will
147 // return true.
148 bool ModelIsUnsat() const { return model_is_unsat_; }
149
150 // Adds and registers the given propagator with the sat solver. Note that
151 // during propagation, they will be called in the order they were added.
152 void AddPropagator(SatPropagator* propagator);
153 void AddLastPropagator(SatPropagator* propagator);
154 void TakePropagatorOwnership(std::unique_ptr<SatPropagator> propagator) {
155 owned_propagators_.push_back(std::move(propagator));
156 }
157
158 // Wrapper around the same functions in SatDecisionPolicy.
159 //
160 // TODO(user): Clean this up by making clients directly talk to
161 // SatDecisionPolicy.
162 void SetAssignmentPreference(Literal literal, float weight) {
163 decision_policy_->SetAssignmentPreference(literal, weight);
164 }
165 std::vector<std::pair<Literal, float>> AllPreferences() const {
166 return decision_policy_->AllPreferences();
167 }
169 return decision_policy_->ResetDecisionHeuristic();
170 }
171
172 // Solves the problem and returns its status.
173 // An empty problem is considered to be SAT.
174 //
175 // Note that the conflict limit applies only to this function and starts
176 // counting from the time it is called.
177 //
178 // This will restart from the current solver configuration. If a previous call
179 // to Solve() was interrupted by a conflict or time limit, calling this again
180 // will resume the search exactly as it would have continued.
181 //
182 // Note that this will use the TimeLimit singleton, so the time limit
183 // will be counted since the last time TimeLimit was reset, not from
184 // the start of this function.
191 Status Solve();
192
193 // Same as Solve(), but with a given time limit. Note that this will not
194 // update the TimeLimit singleton, but only the passed object instead.
196
197 // Simple interface to solve a problem under the given assumptions. This
198 // simply ask the solver to solve a problem given a set of variables fixed to
199 // a given value (the assumptions). Compared to simply calling AddUnitClause()
200 // and fixing the variables once and for all, this allow to backtrack over the
201 // assumptions and thus exploit the incrementally between subsequent solves.
202 //
203 // This function backtrack over all the current decision, tries to enqueue the
204 // given assumptions, sets the assumption level accordingly and finally calls
205 // Solve().
206 //
207 // If, given these assumptions, the model is UNSAT, this returns the
208 // ASSUMPTIONS_UNSAT status. INFEASIBLE is reserved for the case where the
209 // model is proven to be unsat without any assumptions.
210 //
211 // If ASSUMPTIONS_UNSAT is returned, it is possible to get a "core" of unsat
212 // assumptions by calling GetLastIncompatibleDecisions().
214 const std::vector<Literal>& assumptions,
215 int64_t max_number_of_conflicts = -1);
216
217 // Changes the assumption level. All the decisions below this level will be
218 // treated as assumptions by the next Solve(). Note that this may impact some
219 // heuristics, like the LBD value of a clause.
220 void SetAssumptionLevel(int assumption_level);
221
222 // Returns the current assumption level. Note that if a solve was done since
223 // the last SetAssumptionLevel(), then the returned level may be lower than
224 // the one that was set. This is because some assumptions may now be
225 // consequences of others before them due to the newly learned clauses.
226 int AssumptionLevel() const { return assumption_level_; }
227
228 // This can be called just after SolveWithAssumptions() returned
229 // ASSUMPTION_UNSAT or after EnqueueDecisionAndBacktrackOnConflict() leaded
230 // to a conflict. It returns a subsequence (in the correct order) of the
231 // previously enqueued decisions that cannot be taken together without making
232 // the problem UNSAT.
233 std::vector<Literal> GetLastIncompatibleDecisions();
234
235 // Returns a subset of decisions that are sufficient to ensure all literals in
236 // `literals` are fixed to their current value.
237 std::vector<Literal> GetDecisionsFixing(absl::Span<const Literal> literals);
238
239 // Advanced usage. The next 3 functions allow to drive the search from outside
240 // the solver.
241
242 // Takes a new decision (the given true_literal must be unassigned) and
243 // propagates it. Returns the trail index of the first newly propagated
244 // literal. If there is a conflict and the problem is detected to be UNSAT,
245 // returns kUnsatTrailIndex.
246 //
247 // Important: In the presence of assumptions, this also returns
248 // kUnsatTrailIndex on ASSUMPTION_UNSAT. One can know the difference with
249 // IsModelUnsat().
250 //
251 // A client can determine if there is a conflict by checking if the
252 // CurrentDecisionLevel() was increased by 1 or not.
253 //
254 // If there is a conflict, the given decision is not applied and:
255 // - The conflict is learned.
256 // - The decisions are potentially backtracked to the first decision that
257 // propagates more variables because of the newly learned conflict.
258 // - The returned value is equal to trail_->Index() after this backtracking
259 // and just before the new propagation (due to the conflict) which is also
260 // performed by this function.
262
263 // This function starts by calling EnqueueDecisionAndBackjumpOnConflict(). If
264 // there is no conflict, it stops there. Otherwise, it tries to reapply all
265 // the decisions that were backjumped over until the first one that can't be
266 // taken because it is incompatible. Note that during this process, more
267 // conflicts may happen and the trail may be backtracked even further.
268 //
269 // In any case, the new decisions stack will be the largest valid "prefix"
270 // of the old stack. Note that decisions that are now consequence of the ones
271 // before them will no longer be decisions.
272 //
273 // Returns INFEASIBLE if the model was proven infeasible, ASSUMPTION_UNSAT if
274 // the current decision and the one we are trying to take are not compatible
275 // together and FEASIBLE if all decisions are taken.
276 //
277 // Note(user): This function can be called with an already assigned literal.
279 Literal true_literal, int* first_propagation_index = nullptr);
280
281 // Tries to enqueue the given decision and performs the propagation.
282 // Returns true if no conflict occurred. Otherwise, returns false and restores
283 // the solver to the state just before this was called.
284 //
285 // Note(user): With this function, the solver doesn't learn anything.
286 bool EnqueueDecisionIfNotConflicting(Literal true_literal);
287
288 // Restores the state to the given target decision level. The decision at that
289 // level and all its propagation will not be undone. But all the trail after
290 // this will be cleared. Calling this with 0 will revert all the decisions and
291 // only the fixed variables will be left on the trail.
292 void Backtrack(int target_level);
293
294 // Advanced usage. This is meant to restore the solver to a "proper" state
295 // after a solve was interrupted due to a limit reached.
296 //
297 // Without assumption (i.e. if AssumptionLevel() is 0), this will revert all
298 // decisions and make sure that all the fixed literals are propagated. In
299 // presence of assumptions, this will either backtrack to the assumption level
300 // or re-enqueue any assumptions that may have been backtracked over due to
301 // conflits resolution. In both cases, the propagation is finished.
302 //
303 // Note that this may prove the model to be UNSAT or ASSUMPTION_UNSAT in which
304 // case it will return false.
306
307 // Advanced usage. Finish the progation if it was interrupted. Note that this
308 // might run into conflict and will propagate again until a fixed point is
309 // reached or the model was proven UNSAT. Returns IsModelUnsat().
310 ABSL_MUST_USE_RESULT bool FinishPropagation();
311
312 // Like Backtrack(0) but make sure the propagation is finished and return
313 // false if unsat was detected. This also removes any assumptions level.
314 ABSL_MUST_USE_RESULT bool ResetToLevelZero();
315
316 // Changes the assumptions level and the current solver assumptions. Returns
317 // false if the model is UNSAT or ASSUMPTION_UNSAT, true otherwise.
318 //
319 // This uses the "new" assumptions handling, where all assumptions are
320 // enqueued at once at decision level 1 before we start to propagate. This has
321 // many advantages. In particular, because we propagate with the binary
322 // implications first, if we ever have assumption => not(other_assumptions) we
323 // are guaranteed to find it and returns a core of size 2.
324 //
325 // Paper: "Speeding Up Assumption-Based SAT", Randy Hickey and Fahiem Bacchus
326 // http://www.maxhs.org/docs/Hickey-Bacchus2019_Chapter_SpeedingUpAssumption-BasedSAT.pdf
327 bool ResetWithGivenAssumptions(const std::vector<Literal>& assumptions);
328
329 // Advanced usage. If the decision level is smaller than the assumption level,
330 // this will try to reapply all assumptions. Returns true if this was doable,
331 // otherwise returns false in which case the model is either UNSAT or
332 // ASSUMPTION_UNSAT.
334
335 // Helper functions to get the correct status when one of the functions above
336 // returns false.
339 }
340
341 // Extract the current problem clauses. The Output type must support the two
342 // functions:
343 // - void AddBinaryClause(Literal a, Literal b);
344 // - void AddClause(absl::Span<const Literal> clause);
345 //
346 // TODO(user): also copy the removable clauses?
347 template <typename Output>
348 bool ExtractClauses(Output* out) {
349 if (!ResetToLevelZero()) return false;
350
351 // It is important to process the newly fixed variables, so they are not
352 // present in the clauses we export.
353 if (num_processed_fixed_variables_ < trail_->Index()) {
355 }
356 clauses_propagator_->DeleteRemovedClauses();
357
358 // Note(user): Putting the binary clauses first help because the presolver
359 // currently process the clauses in order.
360 out->SetNumVariables(NumVariables());
361 binary_implication_graph_->ExtractAllBinaryClauses(out);
362 for (SatClause* clause : clauses_propagator_->AllClausesInCreationOrder()) {
363 if (!clauses_propagator_->IsRemovable(clause)) {
364 out->AddClause(clause->AsSpan());
365 }
366 }
367
368 return true;
369 }
370
371 // Functions to manage the set of learned binary clauses.
372 // Only clauses added/learned when TrackBinaryClause() is true are managed.
373 void TrackBinaryClauses(bool value) { track_binary_clauses_ = value; }
374 bool AddBinaryClauses(absl::Span<const BinaryClause> clauses);
375 const std::vector<BinaryClause>& NewlyAddedBinaryClauses();
377
378 struct Decision {
379 Decision() = default;
381 int trail_index = 0;
383 };
384
385 // Note that the Decisions() vector is always of size NumVariables(), and that
386 // only the first CurrentDecisionLevel() entries have a meaning.
387 const std::vector<Decision>& Decisions() const { return decisions_; }
388 int CurrentDecisionLevel() const { return current_decision_level_; }
389 const Trail& LiteralTrail() const { return *trail_; }
390 const VariablesAssignment& Assignment() const { return trail_->Assignment(); }
391
392 // Some statistics since the creation of the solver.
393 int64_t num_branches() const;
394 int64_t num_failures() const;
395 int64_t num_propagations() const;
396 int64_t num_backtracks() const;
397
398 // Note that we count the number of backtrack to level zero from a positive
399 // level. Those can corresponds to actual restarts, or conflicts that learn
400 // unit clauses or any other reason that trigger such backtrack.
401 int64_t num_restarts() const;
402
403 // Access to all counters.
404 // Tracks various information about the solver progress.
405 struct Counters {
406 int64_t num_branches = 0;
407 int64_t num_failures = 0;
408 int64_t num_restarts = 0;
409 int64_t num_backtracks = 0;
410
411 // Minimization stats.
412 int64_t num_minimizations = 0;
414
415 // PB constraints.
417
418 // Clause learning /deletion stats.
422
423 // TryToMinimizeClause() stats.
430 };
431 Counters counters() const { return counters_; }
432
433 // A deterministic number that should be correlated with the time spent in
434 // the Solve() function. The order of magnitude should be close to the time
435 // in seconds.
436 double deterministic_time() const;
437
438 // Only used for debugging. Save the current assignment in debug_assignment_.
439 // The idea is that if we know that a given assignment is satisfiable, then
440 // all the learned clauses or PB constraints must be satisfiable by it. In
441 // debug mode, and after this is called, all the learned clauses are tested to
442 // satisfy this saved assignment.
443 void SaveDebugAssignment();
444 void LoadDebugSolution(absl::Span<const Literal> solution);
445
446 void SetDratProofHandler(DratProofHandler* drat_proof_handler) {
447 drat_proof_handler_ = drat_proof_handler;
448 clauses_propagator_->SetDratProofHandler(drat_proof_handler_);
449 binary_implication_graph_->SetDratProofHandler(drat_proof_handler_);
450 }
451
452 // This function is here to deal with the case where a SAT/CP model is found
453 // to be trivially UNSAT while the user is constructing the model. Instead of
454 // having to test the status of all the lines adding a constraint, one can
455 // just check if the solver is not UNSAT once the model is constructed. Note
456 // that we usually log a warning on the first constraint that caused a
457 // "trival" unsatisfiability.
458 void NotifyThatModelIsUnsat() { model_is_unsat_ = true; }
459
460 // Adds a clause at any level of the tree and propagate any new deductions.
461 // Returns false if the model becomes UNSAT. Important: We currently do not
462 // support adding a clause that is already falsified at a positive decision
463 // level. Doing that will cause a check fail.
464 //
465 // TODO(user): Backjump and propagate on a falsified clause? this is currently
466 // not needed.
467 bool AddClauseDuringSearch(absl::Span<const Literal> literals);
468
469 // Performs propagation of the recently enqueued elements.
470 // Mainly visible for testing.
471 ABSL_MUST_USE_RESULT bool Propagate();
472
473 bool MinimizeByPropagation(double dtime,
474 bool minimize_new_clauses_only = false);
475
476 // Advance the given time limit with all the deterministic time that was
477 // elapsed since last call.
479 const double current = deterministic_time();
481 current - deterministic_time_at_last_advanced_time_limit_);
482 deterministic_time_at_last_advanced_time_limit_ = current;
483 }
484
485 // Simplifies the problem when new variables are assigned at level 0.
487
488 int64_t NumFixedVariables() const {
489 if (!decisions_.empty()) return decisions_[0].trail_index;
490 CHECK_EQ(CurrentDecisionLevel(), 0);
491 return trail_->Index();
492 }
493
494 // Hack to allow to temporarily disable logging if it is enabled.
495 SolverLogger* mutable_logger() { return logger_; }
496
497 // Processes the current conflict from trail->FailingClause().
498 //
499 // This learns the conflict, backtracks, enqueues the consequence of the
500 // learned conflict and return. When handling assumptions, this might return
501 // false without backtracking in case of ASSUMPTIONS_UNSAT. This is only
502 // exposed to allow processing a conflict detected outside normal propagation.
504
506 clauses_propagator_->EnsureNewClauseIndexInitialized();
507 }
508
509 private:
510 // All Solve() functions end up calling this one.
511 Status SolveInternal(TimeLimit* time_limit, int64_t max_number_of_conflicts);
512
513 // Adds a binary clause to the BinaryImplicationGraph and to the
514 // BinaryClauseManager when track_binary_clauses_ is true.
515 void AddBinaryClauseInternal(Literal a, Literal b);
516
517 // See SaveDebugAssignment(). Note that these functions only consider the
518 // variables at the time the debug_assignment_ was saved. If new variables
519 // were added since that time, they will be considered unassigned.
520 bool ClauseIsValidUnderDebugAssignment(
521 absl::Span<const Literal> clause) const;
522 bool PBConstraintIsValidUnderDebugAssignment(
523 absl::Span<const LiteralWithCoeff> cst, Coefficient rhs) const;
524
525 // Logs the given status if parameters_.log_search_progress() is true.
526 // Also returns it.
527 Status StatusWithLog(Status status);
528
529 // Main function called from SolveWithAssumptions() or from Solve() with an
530 // assumption_level of 0 (meaning no assumptions).
531 Status SolveInternal(int assumption_level);
532
533 // Applies the previous decisions (which are still on decisions_), in order,
534 // starting from the one at the current decision level. Stops at the one at
535 // decisions_[level] or on the first decision already propagated to "false"
536 // and thus incompatible.
537 //
538 // Note that during this process, conflicts may arise which will lead to
539 // backjumps. In this case, we will simply keep reapplying decisions from the
540 // last one backtracked over and so on.
541 //
542 // Returns FEASIBLE if no conflict occurred, INFEASIBLE if the model was
543 // proven unsat and ASSUMPTION_UNSAT otherwise. In the last case the first non
544 // taken old decision will be propagated to false by the ones before.
545 //
546 // first_propagation_index will be filled with the trail index of the first
547 // newly propagated literal, or with -1 if INFEASIBLE is returned.
548 Status ReapplyDecisionsUpTo(int level,
549 int* first_propagation_index = nullptr);
550
551 // Returns false if the thread memory is over the limit.
552 bool IsMemoryLimitReached() const;
553
554 // Sets model_is_unsat_ to true and return false.
555 bool SetModelUnsat();
556
557 // Returns the decision level of a given variable.
558 int DecisionLevel(BooleanVariable var) const {
559 return trail_->Info(var).level;
560 }
561
562 // Returns the relevant pointer if the given variable was propagated by the
563 // constraint in question. This is used to bump the activity of the learned
564 // clauses or pb constraints.
565 SatClause* ReasonClauseOrNull(BooleanVariable var) const;
566 UpperBoundedLinearConstraint* ReasonPbConstraintOrNull(
567 BooleanVariable var) const;
568
569 // This does one step of a pseudo-Boolean resolution:
570 // - The variable var has been assigned to l at a given trail_index.
571 // - The reason for var propagates it to l.
572 // - The conflict propagates it to not(l)
573 // The goal of the operation is to combine the two constraints in order to
574 // have a new conflict at a lower trail_index.
575 //
576 // Returns true if the reason for var was a normal clause. In this case,
577 // the *slack is updated to its new value.
578 bool ResolvePBConflict(BooleanVariable var,
579 MutableUpperBoundedLinearConstraint* conflict,
580 Coefficient* slack);
581
582 // Returns true iff the clause is the reason for an assigned variable.
583 //
584 // TODO(user): With our current data structures, we could also return true
585 // for clauses that were just used as a reason (like just before an untrail).
586 // This may be beneficial, but should properly be defined so that we can
587 // have the same behavior if we change the implementation.
588 bool ClauseIsUsedAsReason(SatClause* clause) const {
589 const BooleanVariable var = clause->PropagatedLiteral().Variable();
590 return trail_->Info(var).trail_index < trail_->Index() &&
591 (*trail_)[trail_->Info(var).trail_index].Variable() == var &&
592 ReasonClauseOrNull(var) == clause;
593 }
594
595 // Add a problem clause. The clause is assumed to be "cleaned", that is no
596 // duplicate variables (not strictly required) and not empty.
597 bool AddProblemClauseInternal(absl::Span<const Literal> literals);
598
599 // This is used by all the Add*LinearConstraint() functions. It detects
600 // infeasible/trivial constraints or clause constraints and takes the proper
601 // action.
602 bool AddLinearConstraintInternal(const std::vector<LiteralWithCoeff>& cst,
603 Coefficient rhs, Coefficient max_value);
604
605 // Makes sure a pseudo boolean constraint is in canonical form.
606 void CanonicalizeLinear(std::vector<LiteralWithCoeff>* cst,
607 Coefficient* bound_shift, Coefficient* max_value);
608
609 // Adds a learned clause to the problem. This should be called after
610 // Backtrack(). The backtrack is such that after it is applied, all the
611 // literals of the learned close except one will be false. Thus the last one
612 // will be implied True. This function also Enqueue() the implied literal.
613 //
614 // Returns the LBD of the clause.
615 int AddLearnedClauseAndEnqueueUnitPropagation(
616 const std::vector<Literal>& literals, bool is_redundant);
617
618 // Creates a new decision which corresponds to setting the given literal to
619 // True and Enqueue() this change.
620 void EnqueueNewDecision(Literal literal);
621
622 // Returns true if everything has been propagated.
623 //
624 // TODO(user): This test is fast but not exhaustive, especially regarding the
625 // integer propagators. Fix.
626 bool PropagationIsDone() const;
627
628 // Update the propagators_ list with the relevant propagators.
629 void InitializePropagators();
630
631 // Output to the DRAT proof handler any newly fixed variables.
632 void ProcessNewlyFixedVariablesForDratProof();
633
634 // Returns the maximum trail_index of the literals in the given clause.
635 // All the literals must be assigned. Returns -1 if the clause is empty.
636 int ComputeMaxTrailIndex(absl::Span<const Literal> clause) const;
637
638 // Computes what is known as the first UIP (Unique implication point) conflict
639 // clause starting from the failing clause. For a definition of UIP and a
640 // comparison of the different possible conflict clause computation, see the
641 // reference below.
642 //
643 // The conflict will have only one literal at the highest decision level, and
644 // this literal will always be the first in the conflict vector.
645 //
646 // L Zhang, CF Madigan, MH Moskewicz, S Malik, "Efficient conflict driven
647 // learning in a boolean satisfiability solver" Proceedings of the 2001
648 // IEEE/ACM international conference on Computer-aided design, Pages 279-285.
649 // http://www.cs.tau.ac.il/~msagiv/courses/ATP/iccad2001_final.pdf
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);
654
655 // Fills literals with all the literals in the reasons of the literals in the
656 // given input. The output vector will have no duplicates and will not contain
657 // the literals already present in the input.
658 void ComputeUnionOfReasons(absl::Span<const Literal> input,
659 std::vector<Literal>* literals);
660
661 // Do the full pseudo-Boolean constraint analysis. This calls multiple
662 // time ResolvePBConflict() on the current conflict until we have a conflict
663 // that allow us to propagate more at a lower decision level. This level
664 // is the one returned in backjump_level.
665 void ComputePBConflict(int max_trail_index, Coefficient initial_slack,
666 MutableUpperBoundedLinearConstraint* conflict,
667 int* backjump_level);
668
669 // Applies some heuristics to a conflict in order to minimize its size and/or
670 // replace literals by other literals from lower decision levels. The first
671 // function choose which one of the other functions to call depending on the
672 // parameters.
673 //
674 // Precondition: is_marked_ should be set to true for all the variables of
675 // the conflict. It can also contains false non-conflict variables that
676 // are implied by the negation of the 1-UIP conflict literal.
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);
681
682 // Utility function used by MinimizeConflictRecursively().
683 bool CanBeInferedFromConflictVariables(BooleanVariable variable);
684
685 // To be used in DCHECK(). Verifies some property of the conflict clause:
686 // - There is an unique literal with the highest decision level.
687 // - This literal appears in the first position.
688 // - All the other literals are of smaller decision level.
689 // - There is no literal with a decision level of zero.
690 bool IsConflictValid(absl::Span<const Literal> literals);
691
692 // Given the learned clause after a conflict, this computes the correct
693 // backtrack level to call Backtrack() with.
694 int ComputeBacktrackLevel(absl::Span<const Literal> literals);
695
696 // The LBD (Literal Blocks Distance) is the number of different decision
697 // levels at which the literals of the clause were assigned. Note that we
698 // ignore the decision level 0 whereas the definition in the paper below
699 // doesn't:
700 //
701 // G. Audemard, L. Simon, "Predicting Learnt Clauses Quality in Modern SAT
702 // Solver" in Twenty-first International Joint Conference on Artificial
703 // Intelligence (IJCAI'09), july 2009.
704 // http://www.ijcai.org/papers09/Papers/IJCAI09-074.pdf
705 //
706 // IMPORTANT: All the literals of the clause must be assigned, and the first
707 // literal must be of the highest decision level. This will be the case for
708 // all the reason clauses.
709 template <typename LiteralList>
710 int ComputeLbd(const LiteralList& literals);
711
712 // Checks if we need to reduce the number of learned clauses and do
713 // it if needed. Also updates the learned clause limit for the next cleanup.
714 void CleanClauseDatabaseIfNeeded();
715
716 // Activity management for clauses. This work the same way at the ones for
717 // variables, but with different parameters.
718 void BumpReasonActivities(absl::Span<const Literal> literals);
719 void BumpClauseActivity(SatClause* clause);
720 void RescaleClauseActivities(double scaling_factor);
721 void UpdateClauseActivityIncrement();
722
723 std::string DebugString(const SatClause& clause) const;
724 std::string StatusString(Status status) const;
725 std::string RunningStatisticsString() const;
726
727 // Returns true if variable is fixed in the current assignment due to
728 // non-removable clauses, plus at most one removable clause with size <=
729 // max_size.
730 bool SubsumptionIsInteresting(BooleanVariable variable, int max_size);
731 void KeepAllClausesUsedToInfer(BooleanVariable variable);
732
733 // Use propagation to try to minimize the given clause. This is really similar
734 // to MinimizeCoreWithPropagation(). Note that because this does a small tree
735 // search, it will impact the variable/clause activities and may add new
736 // conflicts.
737 void TryToMinimizeClause(SatClause* clause);
738
739 // This is used by the old non-model constructor.
740 Model* model_;
741 std::unique_ptr<Model> owned_model_;
742
743 BooleanVariable num_variables_ = BooleanVariable(0);
744
745 // Internal propagators. We keep them here because we need more than the
746 // SatPropagator interface for them.
747 BinaryImplicationGraph* binary_implication_graph_;
748 ClauseManager* clauses_propagator_;
749 PbConstraints* pb_constraints_;
750
751 // Ordered list of propagators used by Propagate()/Untrail().
752 std::vector<SatPropagator*> propagators_;
753 std::vector<SatPropagator*> non_empty_propagators_;
754
755 // Ordered list of propagators added with AddPropagator().
756 std::vector<SatPropagator*> external_propagators_;
757 SatPropagator* last_propagator_ = nullptr;
758
759 // For the old, non-model interface.
760 std::vector<std::unique_ptr<SatPropagator>> owned_propagators_;
761
762 // Keep track of all binary clauses so they can be exported.
763 bool track_binary_clauses_;
764 BinaryClauseManager binary_clauses_;
765
766 // Pointers to singleton Model objects.
767 Trail* trail_;
768 TimeLimit* time_limit_;
769 SatParameters* parameters_;
770 RestartPolicy* restart_;
771 SatDecisionPolicy* decision_policy_;
772 SolverLogger* logger_;
773
774 // Used for debugging only. See SaveDebugAssignment().
775 VariablesAssignment debug_assignment_;
776
777 // The stack of decisions taken by the solver. They are stored in [0,
778 // current_decision_level_). The vector is of size num_variables_ so it can
779 // store all the decisions. This is done this way because in some situation we
780 // need to remember the previously taken decisions after a backtrack.
781 int current_decision_level_ = 0;
782 std::vector<Decision> decisions_;
783
784 // The trail index after the last Backtrack() call or before the last
785 // EnqueueNewDecision() call.
786 int last_decision_or_backtrack_trail_index_ = 0;
787
788 // The assumption level. See SolveWithAssumptions().
789 int assumption_level_ = 0;
790 std::vector<Literal> assumptions_;
791
792 // The size of the trail when ProcessNewlyFixedVariables() was last called.
793 // Note that the trail contains only fixed literals (that is literals of
794 // decision levels 0) before this point.
795 int num_processed_fixed_variables_ = 0;
796 double deterministic_time_of_last_fixed_variables_cleanup_ = 0.0;
797
798 // Used in ProcessNewlyFixedVariablesForDratProof().
799 int drat_num_processed_fixed_variables_ = 0;
800
801 Counters counters_;
802
803 // Solver information.
804 WallTimer timer_;
805
806 // This is set to true if the model is found to be UNSAT when adding new
807 // constraints.
808 bool model_is_unsat_ = false;
809
810 // Increment used to bump the variable activities.
811 double clause_activity_increment_;
812
813 // This counter is decremented each time we learn a clause that can be
814 // deleted. When it reaches zero, a clause cleanup is triggered.
815 int num_learned_clause_before_cleanup_ = 0;
816
817 int64_t minimization_by_propagation_threshold_ = 0;
818
819 // Temporary members used during conflict analysis.
820 SparseBitset<BooleanVariable> is_marked_;
821 SparseBitset<BooleanVariable> is_independent_;
822 SparseBitset<BooleanVariable> tmp_mark_;
823 std::vector<int> min_trail_index_per_level_;
824
825 // Temporary members used by CanBeInferedFromConflictVariables().
826 std::vector<BooleanVariable> dfs_stack_;
827 std::vector<BooleanVariable> variable_to_process_;
828
829 // Temporary member used when adding clauses.
830 std::vector<Literal> literals_scratchpad_;
831
832 // A boolean vector used to temporarily mark decision levels.
833 DEFINE_STRONG_INDEX_TYPE(SatDecisionLevel);
834 SparseBitset<SatDecisionLevel> is_level_marked_;
835
836 // Temporary vectors used by EnqueueDecisionAndBackjumpOnConflict().
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_;
841
842 // When true, temporarily disable the deletion of clauses that are not needed
843 // anymore. This is a hack for TryToMinimizeClause() because we use
844 // propagation in this function which might trigger a clause database
845 // deletion, but we still want the pointer to the clause we wants to minimize
846 // to be valid until the end of that function.
847 bool block_clause_deletion_ = false;
848
849 // "cache" to avoid inspecting many times the same reason during conflict
850 // analysis.
851 VariableWithSameReasonIdentifier same_reason_identifier_;
852
853 // Boolean used to include/exclude constraints from the core computation.
854 bool is_relevant_for_core_computation_;
855
856 // The current pseudo-Boolean conflict used in PB conflict analysis.
857 MutableUpperBoundedLinearConstraint pb_conflict_;
858
859 // The deterministic time when the time limit was updated.
860 // As the deterministic time in the time limit has to be advanced manually,
861 // it is necessary to keep track of the last time the time was advanced.
862 double deterministic_time_at_last_advanced_time_limit_ = 0;
863
864 DratProofHandler* drat_proof_handler_;
865
866 mutable StatsGroup stats_;
867};
868
869// Tries to minimize the given UNSAT core with a really simple heuristic.
870// The idea is to remove literals that are consequences of others in the core.
871// We already know that in the initial order, no literal is propagated by the
872// one before it, so we just look for propagation in the reverse order.
873//
874// Important: The given SatSolver must be the one that just produced the given
875// core.
876//
877// TODO(user): One should use MinimizeCoreWithPropagation() instead.
878void MinimizeCore(SatSolver* solver, std::vector<Literal>* core);
879
880// ============================================================================
881// Model based functions.
882//
883// TODO(user): move them in another file, and unit-test them.
884// ============================================================================
885
886inline std::function<void(Model*)> BooleanLinearConstraint(
887 int64_t lower_bound, int64_t upper_bound,
888 std::vector<LiteralWithCoeff>* cst) {
889 return [=](Model* model) {
890 model->GetOrCreate<SatSolver>()->AddLinearConstraint(
891 /*use_lower_bound=*/true, Coefficient(lower_bound),
892 /*use_upper_bound=*/true, Coefficient(upper_bound), cst);
893 };
894}
895
896inline std::function<void(Model*)> CardinalityConstraint(
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())](
900 Model* model) {
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);
905 }
906 model->GetOrCreate<SatSolver>()->AddLinearConstraint(
907 /*use_lower_bound=*/true, Coefficient(lower_bound),
908 /*use_upper_bound=*/true, Coefficient(upper_bound), &cst);
909 };
910}
911
912inline std::function<void(Model*)> ExactlyOneConstraint(
913 absl::Span<const Literal> literals) {
914 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
915 Model* model) {
916 std::vector<LiteralWithCoeff> cst;
917 cst.reserve(literals.size());
918 for (const Literal l : literals) {
919 cst.emplace_back(l, Coefficient(1));
920 }
921 model->GetOrCreate<SatSolver>()->AddLinearConstraint(
922 /*use_lower_bound=*/true, Coefficient(1),
923 /*use_upper_bound=*/true, Coefficient(1), &cst);
924 };
925}
926
927inline std::function<void(Model*)> AtMostOneConstraint(
928 absl::Span<const Literal> literals) {
929 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
930 Model* model) {
931 std::vector<LiteralWithCoeff> cst;
932 cst.reserve(literals.size());
933 for (const Literal l : literals) {
934 cst.emplace_back(l, Coefficient(1));
935 }
936 model->GetOrCreate<SatSolver>()->AddLinearConstraint(
937 /*use_lower_bound=*/false, Coefficient(0),
938 /*use_upper_bound=*/true, Coefficient(1), &cst);
939 };
940}
941
942inline std::function<void(Model*)> ClauseConstraint(
943 absl::Span<const Literal> literals) {
944 return [=](Model* model) {
945 model->GetOrCreate<SatSolver>()->AddProblemClause(literals);
946 };
947}
948
949// a => b.
950inline std::function<void(Model*)> Implication(Literal a, Literal b) {
951 return [=](Model* model) {
952 model->GetOrCreate<SatSolver>()->AddBinaryClause(a.Negated(), b);
953 };
954}
955
956// a == b.
957inline std::function<void(Model*)> Equality(Literal a, Literal b) {
958 return [=](Model* model) {
959 model->GetOrCreate<SatSolver>()->AddBinaryClause(a.Negated(), b);
960 model->GetOrCreate<SatSolver>()->AddBinaryClause(a, b.Negated());
961 };
962}
963
964// r <=> (at least one literal is true). This is a reified clause.
965inline std::function<void(Model*)> ReifiedBoolOr(
966 absl::Span<const Literal> literals, Literal r) {
967 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
968 Model* model) {
969 std::vector<Literal> clause;
970 for (const Literal l : literals) {
971 model->Add(Implication(l, r)); // l => r.
972 clause.push_back(l);
973 }
974
975 // All false => r false.
976 clause.push_back(r.Negated());
977 model->Add(ClauseConstraint(clause));
978 };
979}
980
981// enforcement_literals => clause.
982inline std::function<void(Model*)> EnforcedClause(
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());
989 }
990 for (const Literal l : clause) {
991 tmp.push_back(l);
992 }
993 model->Add(ClauseConstraint(tmp));
994 };
995}
996
997// r <=> (all literals are true).
998//
999// Note(user): we could have called ReifiedBoolOr() with everything negated.
1000inline std::function<void(Model*)> ReifiedBoolAnd(
1001 absl::Span<const Literal> literals, Literal r) {
1002 return [=, literals = std::vector<Literal>(literals.begin(), literals.end())](
1003 Model* model) {
1004 std::vector<Literal> clause;
1005 for (const Literal l : literals) {
1006 model->Add(Implication(r, l)); // r => l.
1007 clause.push_back(l.Negated());
1008 }
1009
1010 // All true => r true.
1011 clause.push_back(r);
1012 model->Add(ClauseConstraint(clause));
1013 };
1014}
1015
1016// r <=> (a <= b).
1017inline std::function<void(Model*)> ReifiedBoolLe(Literal a, Literal b,
1018 Literal r) {
1019 return [=](Model* model) {
1020 // r <=> (a <= b) is the same as r <=> not(a=1 and b=0).
1021 // So r <=> a=0 OR b=1.
1022 model->Add(ReifiedBoolOr({a.Negated(), b}, r));
1023 };
1024}
1025
1026// This checks that the variable is fixed.
1027inline std::function<int64_t(const Model&)> Value(Literal l) {
1028 return [=](const Model& model) {
1029 const Trail* trail = model.Get<Trail>();
1030 CHECK(trail->Assignment().VariableIsAssigned(l.Variable()));
1031 return trail->Assignment().LiteralIsTrue(l);
1032 };
1033}
1034
1035// This checks that the variable is fixed.
1036inline std::function<int64_t(const Model&)> Value(BooleanVariable b) {
1037 return [=](const Model& model) {
1038 const Trail* trail = model.Get<Trail>();
1039 CHECK(trail->Assignment().VariableIsAssigned(b));
1040 return trail->Assignment().LiteralIsTrue(Literal(b, true));
1041 };
1042}
1043
1044// This can be used to enumerate all the solutions. After each SAT call to
1045// Solve(), calling this will reset the solver and exclude the current solution
1046// so that the next call to Solve() will give a new solution or UNSAT is there
1047// is no more new solutions.
1048inline std::function<void(Model*)> ExcludeCurrentSolutionAndBacktrack() {
1049 return [=](Model* model) {
1050 SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
1051
1052 // Note that we only exclude the current decisions, which is an efficient
1053 // way to not get the same SAT assignment.
1054 const int current_level = sat_solver->CurrentDecisionLevel();
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());
1060 }
1061 sat_solver->Backtrack(0);
1062 model->Add(ClauseConstraint(clause_to_exclude_solution));
1063 };
1064}
1065
1066// Returns a string representation of a SatSolver::Status.
1067std::string SatStatusString(SatSolver::Status status);
1068inline std::ostream& operator<<(std::ostream& os, SatSolver::Status status) {
1069 os << SatStatusString(status);
1070 return os;
1071}
1072
1073} // namespace sat
1074} // namespace operations_research
1075
1076#endif // OR_TOOLS_SAT_SAT_SOLVER_H_
Definition model.h:341
void AdvanceDeterministicTime(double deterministic_duration)
Definition time_limit.h:184
T Add(std::function< T(Model *)> f)
Definition model.h:87
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
Definition model.h:93
Base class for all the SAT constraints.
Definition sat_base.h:533
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)
Definition sat_solver.h:446
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)
SolverLogger * mutable_logger()
Hack to allow to temporarily disable logging if it is enabled.
Definition sat_solver.h:495
bool AddBinaryClauses(absl::Span< const BinaryClause > clauses)
void SetAssignmentPreference(Literal literal, float weight)
Definition sat_solver.h:162
BooleanVariable NewBooleanVariable()
Definition sat_solver.h:90
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.
bool AddProblemClause(absl::Span< const Literal > literals)
std::vector< Literal > GetLastIncompatibleDecisions()
bool AddBinaryClause(Literal a, Literal b)
Same as AddProblemClause() below, but for small clauses.
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void Backtrack(int target_level)
const SatParameters & parameters() const
bool EnqueueDecisionIfNotConflicting(Literal true_literal)
bool AddClauseDuringSearch(absl::Span< const Literal > literals)
ABSL_MUST_USE_RESULT bool Propagate()
std::vector< Literal > GetDecisionsFixing(absl::Span< const Literal > literals)
void SetAssumptionLevel(int assumption_level)
std::vector< std::pair< Literal, float > > AllPreferences() const
Definition sat_solver.h:165
ABSL_MUST_USE_RESULT bool AddUnitClause(Literal true_literal)
bool AddTernaryClause(Literal a, Literal b, Literal c)
void TakePropagatorOwnership(std::unique_ptr< SatPropagator > propagator)
Definition sat_solver.h:154
SatSolver & operator=(const SatSolver &)=delete
void AdvanceDeterministicTime(TimeLimit *limit)
Definition sat_solver.h:478
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions, int64_t max_number_of_conflicts=-1)
const VariablesAssignment & Assignment() const
Definition sat_solver.h:390
ABSL_MUST_USE_RESULT bool ResetToLevelZero()
void AddLastPropagator(SatPropagator *propagator)
const std::vector< Decision > & Decisions() const
Definition sat_solver.h:387
ABSL_MUST_USE_RESULT bool FinishPropagation()
const Trail & LiteralTrail() const
Definition sat_solver.h:389
void SetNumVariables(int num_variables)
Definition sat_solver.cc:86
void AddPropagator(SatPropagator *propagator)
void SetParameters(const SatParameters &parameters)
const AssignmentInfo & Info(BooleanVariable var) const
Definition sat_base.h:463
const VariablesAssignment & Assignment() const
Definition sat_base.h:462
bool VariableIsAssigned(BooleanVariable var) const
Returns true iff the given variable is assigned.
Definition sat_base.h:196
bool LiteralIsTrue(Literal literal) const
Definition sat_base.h:188
time_limit
Definition solve.cc:22
std::function< void(Model *)> Equality(IntegerVariable v, int64_t value)
Fix v to a given value.
Definition integer.h:1638
std::string SatStatusString(SatSolver::Status status)
Returns a string representation of a SatSolver::Status.
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition sat_solver.h:944
std::function< void(Model *)> EnforcedClause(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
enforcement_literals => clause.
Definition sat_solver.h:984
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)
Definition integer.h:1651
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
Definition cp_model.cc:89
std::function< int64_t(const Model &)> Value(IntegerVariable v)
This checks that the variable is fixed.
Definition integer.h:1601
std::function< void(Model *)> AtMostOneConstraint(absl::Span< const Literal > literals)
Definition sat_solver.h:929
std::function< void(Model *)> CardinalityConstraint(int64_t lower_bound, int64_t upper_bound, absl::Span< const Literal > literals)
Definition sat_solver.h:898
std::function< void(Model *)> ExactlyOneConstraint(absl::Span< const Literal > literals)
Definition sat_solver.h:914
std::function< void(Model *)> BooleanLinearConstraint(int64_t lower_bound, int64_t upper_bound, std::vector< LiteralWithCoeff > *cst)
Definition sat_solver.h:888
const int kUnsatTrailIndex
A constant used by the EnqueueDecision*() API.
Definition sat_solver.h:54
std::function< void(Model *)> ReifiedBoolOr(absl::Span< const Literal > literals, Literal r)
r <=> (at least one literal is true). This is a reified clause.
Definition sat_solver.h:967
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.
Definition sat_base.h:263
int64_t minimization_num_clauses
TryToMinimizeClause() stats.
Definition sat_solver.h:424
int64_t num_minimizations
Minimization stats.
Definition sat_solver.h:412
int64_t num_literals_learned
Clause learning /deletion stats.
Definition sat_solver.h:419