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