C++ Reference: class SatSolver
Note: This documentation is automatically generated.
The main SAT solver. It currently implements the CDCL algorithm. See http://en.wikipedia.org/wiki/Conflict_Driven_Clause_Learning| Method | |
|---|---|
AddBinaryClause | Return type: Arguments: Same as AddProblemClause() below, but for small clauses. |
AddBinaryClauses | Return type: Arguments: |
AddClauseDuringSearch | Return type: Arguments: Adds a clause at any level of the tree and propagate any new deductions. Returns false if the model becomes UNSAT. Important: We currently do not support adding a clause that is already falsified at a positive decision level. Doing that will cause a check fail. TODO(user): Backjump and propagate on a falsified clause? this is currently not needed. |
AddLastPropagator | Return type: Arguments: |
AddLinearConstraint | Return type: Arguments: Adds a pseudo-Boolean constraint to the problem. Returns false if the problem is detected to be UNSAT. If the constraint is always true, this detects it and does nothing. Note(user): There is an optimization if the same constraint is added consecutively (even if the bounds are different). This is particularly useful for an optimization problem when we want to constrain the objective of the problem more and more. Just re-adding such constraint is relatively efficient. OVERFLOW: The sum of the absolute value of all the coefficients in the constraint must not overflow. This is currently CHECKed(). TODO(user): Instead of failing, implement an error handling code. |
AddProblemClause | Return type: Arguments: Adds a clause to the problem. Returns false if the problem is detected to be UNSAT. If is_safe is false, we will do some basic presolving like removing duplicate literals. TODO(user): Rename this to AddClause(), also get rid of the specialized AddUnitClause(), AddBinaryClause() and AddTernaryClause() since they just end up calling this? |
AddPropagator | Return type: Arguments: Adds and registers the given propagator with the sat solver. Note that during propagation, they will be called in the order they were added. |
AddTernaryClause | Return type: Arguments: |
AddUnitClause | Return type: Arguments: Fixes a variable so that the given literal is true. This can be used to solve a subproblem where some variables are fixed. Note that it is more efficient to add such unit clause before all the others. Returns false if the problem is detected to be UNSAT. |
AdvanceDeterministicTime | Return type: Arguments: Advance the given time limit with all the deterministic time that was elapsed since last call. |
Assignment | Return type: |
AssumptionLevel | Return type: Returns the current assumption level. Note that if a solve was done since the last SetAssumptionLevel(), then the returned level may be lower than the one that was set. This is because some assumptions may now be consequences of others before them due to the newly learned clauses. |
Backtrack | Return type: Arguments: Restores the state to the given target decision level. The decision at that level and all its propagation will not be undone. But all the trail after this will be cleared. Calling this with 0 will revert all the decisions and only the fixed variables will be left on the trail. |
ClearNewlyAddedBinaryClauses | Return type: |
CurrentDecisionLevel | Return type: |
Decisions | Return type: Note that the Decisions() vector is always of size NumVariables(), and that only the first CurrentDecisionLevel() entries have a meaning. |
deterministic_time | Return type: A deterministic number that should be correlated with the time spent in the Solve() function. The order of magnitude should be close to the time in seconds. |
EnqueueDecisionAndBackjumpOnConflict | Return type: Arguments: Takes a new decision (the given true_literal must be unassigned) and propagates it. Returns the trail index of the first newly propagated literal. If there is a conflict and the problem is detected to be UNSAT, returns kUnsatTrailIndex. Important: In the presence of assumptions, this also returns kUnsatTrailIndex on ASSUMPTION_UNSAT. One can know the difference with IsModelUnsat(). A client can determine if there is a conflict by checking if the CurrentDecisionLevel() was increased by 1 or not. If there is a conflict, the given decision is not applied and: - The conflict is learned. - The decisions are potentially backtracked to the first decision that propagates more variables because of the newly learned conflict. - The returned value is equal to trail_->Index() after this backtracking and just before the new propagation (due to the conflict) which is also performed by this function. |
EnqueueDecisionAndBacktrackOnConflict | Return type: Arguments: This function starts by calling EnqueueDecisionAndBackjumpOnConflict(). If there is no conflict, it stops there. Otherwise, it tries to reapply all the decisions that were backjumped over until the first one that can't be taken because it is incompatible. Note that during this process, more conflicts may happen and the trail may be backtracked even further. In any case, the new decisions stack will be the largest valid "prefix" of the old stack. Note that decisions that are now consequence of the ones before them will no longer be decisions. Returns INFEASIBLE if the model was proven infeasible, ASSUMPTION_UNSAT if the current decision and the one we are trying to take are not compatible together and FEASIBLE if all decisions are taken. Note(user): This function can be called with an already assigned literal. |
EnqueueDecisionIfNotConflicting | Return type: Arguments: Tries to enqueue the given decision and performs the propagation. Returns true if no conflict occurred. Otherwise, returns false and restores the solver to the state just before this was called. Note(user): With this function, the solver doesn't learn anything. |
ExtractClauses | Return type: Arguments: |
FinishPropagation | Return type: Advanced usage. Finish the progation if it was interrupted. Note that this might run into conflict and will propagate again until a fixed point is reached or the model was proven UNSAT. Returns IsModelUnsat(). |
GetLastIncompatibleDecisions | Return type: This can be called just after SolveWithAssumptions() returned ASSUMPTION_UNSAT or after EnqueueDecisionAndBacktrackOnConflict() leaded to a conflict. It returns a subsequence (in the correct order) of the previously enqueued decisions that cannot be taken together without making the problem UNSAT. |
IsModelUnsat | Return type: Returns true if the model is UNSAT. Note that currently the status is "sticky" and once this happen, nothing else can be done with the solver. Thanks to this function, a client can safely ignore the return value of any Add*() functions. If one of them return false, then IsModelUnsat() will return true. TODO(user): Rename to ModelIsUnsat(). |
LiteralTrail | Return type: |
MinimizeSomeClauses | Return type: Arguments: This must be called at level zero. It will spend the given num decision and use propagation to try to minimize some clauses from the database. |
model | Return type: TODO(user): Remove. This is temporary for accessing the model deep within some old code that didn't use the Model object. |
NewBooleanVariable | Return type: |
NewlyAddedBinaryClauses | Return type: |
NotifyThatModelIsUnsat | Return type: This function is here to deal with the case where a SAT/CP model is found to be trivially UNSAT while the user is constructing the model. Instead of having to test the status of all the lines adding a constraint, one can just check if the solver is not UNSAT once the model is constructed. Note that we usually log a warning on the first constraint that caused a "trival" unsatisfiability. |
num_branches | Return type: Some statistics since the creation of the solver. |
num_failures | Return type: |
num_propagations | Return type: |
num_restarts | Return type: Note that we count the number of backtrack to level zero from a positive level. Those can corresponds to actual restarts, or conflicts that learn unit clauses or any other reason that trigger such backtrack. |
NumFixedVariables | Return type: |
NumVariables | Return type: |
parameters | Return type: |
ProblemIsPureSat | Return type: Returns true iff the loaded problem only contains clauses. |
ProcessNewlyFixedVariables | Return type: Simplifies the problem when new variables are assigned at level 0. |
Propagate | Return type: Performs propagation of the recently enqueued elements. Mainly visible for testing. |
ReapplyAssumptionsIfNeeded | Return type: Advanced usage. If the decision level is smaller than the assumption level, this will try to reapply all assumptions. Returns true if this was doable, otherwise returns false in which case the model is either UNSAT or ASSUMPTION_UNSAT. |
ResetAndSolveWithGivenAssumptions | Return type: Arguments: Simple interface to solve a problem under the given assumptions. This simply ask the solver to solve a problem given a set of variables fixed to a given value (the assumptions). Compared to simply calling AddUnitClause() and fixing the variables once and for all, this allow to backtrack over the assumptions and thus exploit the incrementally between subsequent solves. This function backtrack over all the current decision, tries to enqueue the given assumptions, sets the assumption level accordingly and finally calls Solve(). If, given these assumptions, the model is UNSAT, this returns the ASSUMPTIONS_UNSAT status. INFEASIBLE is reserved for the case where the model is proven to be unsat without any assumptions. If ASSUMPTIONS_UNSAT is returned, it is possible to get a "core" of unsat assumptions by calling GetLastIncompatibleDecisions(). |
ResetDecisionHeuristic | Return type: |
ResetDecisionHeuristicAndSetAllPreferences | Return type: Arguments: |
ResetToLevelZero | Return type: Like Backtrack(0) but make sure the propagation is finished and return false if unsat was detected. This also removes any assumptions level. |
ResetWithGivenAssumptions | Return type: Arguments: Changes the assumptions level and the current solver assumptions. Returns false if the model is UNSAT or ASSUMPTION_UNSAT, true otherwise. This uses the "new" assumptions handling, where all assumptions are enqueued at once at decision level 1 before we start to propagate. This has many advantages. In particular, because we propagate with the binary implications first, if we ever have assumption => not(other_assumptions) we are guaranteed to find it and returns a core of size 2. Paper: "Speeding Up Assumption-Based SAT", Randy Hickey and Fahiem Bacchus http://www.maxhs.org/docs/Hickey-Bacchus2019_Chapter_SpeedingUpAssumption-BasedSAT.pdf |
RestoreSolverToAssumptionLevel | Return type: Advanced usage. This is meant to restore the solver to a "proper" state after a solve was interrupted due to a limit reached. Without assumption (i.e. if AssumptionLevel() is 0), this will revert all decisions and make sure that all the fixed literals are propagated. In presence of assumptions, this will either backtrack to the assumption level or re-enqueue any assumptions that may have been backtracked over due to conflits resolution. In both cases, the propagation is finished. Note that this may prove the model to be UNSAT or ASSUMPTION_UNSAT in which case it will return false. |
SatSolver | |
SatSolver | Return type: Arguments: |
~SatSolver | |
SaveDebugAssignment | Return type: Only used for debugging. Save the current assignment in debug_assignment_. The idea is that if we know that a given assignment is satisfiable, then all the learned clauses or PB constraints must be satisfiable by it. In debug mode, and after this is called, all the learned clauses are tested to satisfy this saved assignment. |
SetAssignmentPreference | Return type: Arguments: Wrapper around the same functions in SatDecisionPolicy. TODO(user): Clean this up by making clients directly talk to SatDecisionPolicy. |
SetAssumptionLevel | Return type: Arguments: Changes the assumption level. All the decisions below this level will be treated as assumptions by the next Solve(). Note that this may impact some heuristics, like the LBD value of a clause. |
SetDratProofHandler | Return type: Arguments: |
SetNumVariables | Return type: Arguments: Increases the number of variables of the current problem. TODO(user): Rename to IncreaseNumVariablesTo() until we support removing variables... |
SetParameters | Return type: Arguments: Parameters management. Note that calling SetParameters() will reset the value of many heuristics. For instance: - The restart strategy will be reinitialized. - The random seed and random generator will be reset to the value given in parameters. - The global TimeLimit singleton will be reset and time will be counted from this call. |
SetShareBinaryClauseCallback | Return type: Arguments: Sets the export function to the shared clauses manager. |
Solve | Return type: |
SolveWithTimeLimit | Return type: Arguments: Same as Solve(), but with a given time limit. Note that this will not update the TimeLimit singleton, but only the passed object instead. |
TakePropagatorOwnership | Return type: Arguments: |
TrackBinaryClauses | Return type: Arguments: Functions to manage the set of learned binary clauses. Only clauses added/learned when TrackBinaryClause() is true are managed. |
UnsatStatus | Return type: Helper functions to get the correct status when one of the functions above returns false. |