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"
32 #include "ortools/base/int_type.h"
34 #include "ortools/base/logging.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"
42 #include "ortools/sat/sat_base.h"
44 #include "ortools/sat/sat_parameters.pb.h"
45 #include "ortools/util/stats.h"
47 
48 namespace operations_research {
49 namespace sat {
50 
51 // A constant used by the EnqueueDecision*() API.
52 const 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
57 class 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.
309  Status UnsatStatus() const {
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) {
321  CHECK(!IsModelUnsat());
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 {
351  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 {
741  int64 num_branches = 0;
742  int64 num_failures = 0;
743  int64 num_restarts = 0;
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.
844 void 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 
852 inline 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 
861 inline 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 
876 inline 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 
890 inline 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 
904 inline 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.
919 inline 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.
926 inline 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.
934 inline 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.
950 inline 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.
968 inline 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).
984 inline 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.
994 inline 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.
1003 inline std::function<int64(const Model&)> Value(BooleanVariable b) {
1004  return [=](const Model& model) {
1005  const Trail* trail = model.Get<Trail>();
1006  CHECK(trail->Assignment().VariableIsAssigned(b));
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.
1015 inline 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.
1034 std::string SatStatusString(SatSolver::Status status);
1035 inline 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
const std::vector< SatClause * > & AllClausesInCreationOrder() const
Definition: clause.h:211
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
Definition: clause.h:239
bool IsRemovable(SatClause *const clause) const
Definition: clause.h:219
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)
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
std::vector< std::pair< Literal, double > > AllPreferences() const
Definition: sat_solver.h:153
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
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
void ResetDecisionHeuristicAndSetAllPreferences(const std::vector< std::pair< Literal, double >> &prefs)
Definition: sat_solver.h:159
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 std::vector< BinaryClause > & NewlyAddedBinaryClauses()
Definition: sat_solver.cc:932
bool AddBinaryClauses(const std::vector< BinaryClause > &clauses)
Definition: sat_solver.cc:918
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
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
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
const std::vector< Decision > & Decisions() const
Definition: sat_solver.h:359
bool AddUnitClause(Literal true_literal)
Definition: sat_solver.cc:164
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
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::function< void(Model *)> ReifiedBoolLe(Literal a, Literal b, Literal r)
Definition: sat_solver.h:984
std::function< void(Model *)> ExcludeCurrentSolutionAndBacktrack()
Definition: sat_solver.h:1015
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
Definition: cp_model.cc:65
std::function< void(Model *)> ClauseConstraint(absl::Span< const Literal > literals)
Definition: sat_solver.h:904
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:876
std::function< int64(const Model &)> Value(IntegerVariable v)
Definition: integer.h:1487
std::function< void(Model *)> BooleanLinearConstraint(int64 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst)
Definition: sat_solver.h:852
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
Definition: integer.h:1524
std::function< void(Model *)> EnforcedClause(absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
Definition: sat_solver.h:950
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
Definition: sat_solver.cc:2547
std::string SatStatusString(SatSolver::Status status)
Definition: sat_solver.cc:2530
std::function< void(Model *)> Implication(const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
Definition: integer.h:1537
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:968
std::function< void(Model *)> AtMostOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:890
std::function< void(Model *)> CardinalityConstraint(int64 lower_bound, int64 upper_bound, const std::vector< Literal > &literals)
Definition: sat_solver.h:861
const int kUnsatTrailIndex
Definition: sat_solver.h:52
std::function< void(Model *)> ReifiedBoolOr(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:934
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)