C++ Reference: class SatSolver

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: bool

Arguments: Literal a, Literal b

Same as AddProblemClause() below, but for small clauses. TODO(user): Remove this and AddUnitClause() when initializer lists can be used in the open-source code like in AddClause({a, b}).

AddBinaryClauseDuringSearch

Return type: void

Arguments: Literal a, Literal b

TODO(user): This internal function should probably not be exposed here.

AddBinaryClauses

Return type: bool

Arguments: const std::vector<BinaryClause>& clauses

AddLastPropagator

Return type: void

Arguments: SatPropagator* propagator

AddLinearConstraint

Return type: bool

Arguments: bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector<LiteralWithCoeff>* cst

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: bool

Arguments: absl::Span<const Literal> literals

Adds a clause to the problem. Returns false if the problem is detected to be UNSAT. TODO(user): Rename this to AddClause().

AddPropagator

Return type: void

Arguments: SatPropagator* propagator

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: bool

Arguments: Literal a, Literal b, Literal c

AddUnitClause

Return type: bool

Arguments: Literal true_literal

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: void

Arguments: TimeLimit* limit

Advance the given time limit with all the deterministic time that was elapsed since last call.

Assignment

Return type: const VariablesAssignment&

AssumptionLevel

Return type: int

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: void

Arguments: int target_level

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: void

CurrentDecisionLevel

Return type: int

Decisions

Return type: const std::vector<Decision>&

Note that the Decisions() vector is always of size NumVariables(), and that only the first CurrentDecisionLevel() entries have a meaning.

deterministic_time

Return type: double

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: int

Arguments: Literal true_literal

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. 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: int

Arguments: Literal true_literal

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. Note(user): This function can be called with an already assigned literal.

EnqueueDecisionIfNotConflicting

Return type: bool

Arguments: Literal true_literal

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: void

Arguments: Output* out

FinishPropagation

Return type: bool

Advanced usage. Finish the progation if it was interupted. 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: std::vector<Literal>

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: bool

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: const Trail&

MinimizeSomeClauses

Return type: void

Arguments: int decisions_budget

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.

NewBooleanVariable

Return type: BooleanVariable

NewlyAddedBinaryClauses

Return type: const std::vector<BinaryClause>&

NotifyThatModelIsUnsat

Return type: void

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: int64

Some statistics since the creation of the solver.

num_failures

Return type: int64

num_propagations

Return type: int64

NumVariables

Return type: int

parameters

Return type: const SatParameters&

ProblemIsPureSat

Return type: bool

Returns true iff the loaded problem only contains clauses.

Propagate

Return type: bool

Performs propagation of the recently enqueued elements. Mainly visible for testing.

ReapplyAssumptionsIfNeeded

Return type: bool

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: Status

Arguments: const std::vector<Literal>& assumptions

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: void

ResetDecisionHeuristicAndSetAllPreferences

Return type: void

Arguments: const std::vector<std::pair<Literal, double>>& prefs

ResetToLevelZero

Return type: bool

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: bool

Arguments: const std::vector<Literal>& assumptions

Changes the assumptions level and the current solver assumptions. Returns false if the model is UNSAT or ASSUMPTION_UNSAT, true otherwise.

RestoreSolverToAssumptionLevel

Return type: bool

Advanced usage. This is meant to restore the solver to a "proper" state after a solve was interupted 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: explicit

Arguments: Model* model

~SatSolver

SaveDebugAssignment

Return type: void

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 assignement.

SetAssignmentPreference

Return type: void

Arguments: Literal literal, double weight

Wrapper around the same functions in SatDecisionPolicy. TODO(user): Clean this up by making clients directly talk to SatDecisionPolicy.

SetAssumptionLevel

Return type: void

Arguments: int assumption_level

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: void

Arguments: DratProofHandler* drat_proof_handler

SetNumVariables

Return type: void

Arguments: int num_variables

Increases the number of variables of the current problem. TODO(user): Rename to IncreaseNumVariablesTo() until we support removing variables...

SetParameters

Return type: void

Arguments: const SatParameters& parameters

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.

Solve

Return type: Status

SolveWithTimeLimit

Return type: Status

Arguments: TimeLimit* time_limit

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: void

Arguments: std::unique_ptr<SatPropagator> propagator

TrackBinaryClauses

Return type: void

Arguments: bool value

Functions to manage the set of learned binary clauses. Only clauses added/learned when TrackBinaryClause() is true are managed.

UnsatStatus

Return type: Status

Helper functions to get the correct status when one of the functions above returns false.