C++ Reference: class SatDecisionPolicy

Note: This documentation is automatically generated.

Implement the SAT branching policy responsible for deciding the next Boolean variable to branch on, and its polarity (true or false).

Method
Activity	Return type: double Arguments: Literal l Returns the current activity of a BooleanVariable.
BeforeConflict	Return type: void Arguments: int trail_index Called on a new conflict before Untrail(). The trail before the given index is used in the phase saving heuristic as a partial assignment.
BumpVariableActivities	Return type: void Arguments: const std::vector<Literal>& literals Bumps the activity of all variables appearing in the conflict. All literals must be currently assigned. See VSIDS decision heuristic: Chaff: Engineering an Efficient SAT Solver. M.W. Moskewicz et al. ANNUAL ACM IEEE DESIGN AUTOMATION CONFERENCE 2001.
IncreaseNumVariables	Return type: void Arguments: int num_variables Notifies that more variables are now present. Note that currently this may change the current variable order because the priority queue need to be reconstructed.
InStablePhase	Return type: bool
MaybeEnablePhaseSaving	Return type: void Arguments: bool save_phase This is used to temporarily disable phase_saving when we do some probing during search for instance.
NextBranch	Return type: Literal Returns next decision to branch upon. This shouldn't be called if all the variables are assigned.
ResetDecisionHeuristic	Return type: void Reinitializes the decision heuristics (which variables to choose with which polarity) according to the current parameters. Note that this also resets the activity of the variables to 0. Note that this function is lazy, and the work will only happen on the first NextBranch() to cover the cases when this policy is not used at all.
SatDecisionPolicy	Return type: explicit Arguments: Model* model
SetAssignmentPreference	Return type: void Arguments: Literal literal, double weight Gives a hint so the solver tries to find a solution with the given literal set to true. Currently this take precedence over the phase saving heuristic and a variable with a preference will always be branched on according to this preference. The weight is used as a tie-breaker between variable with the same activities. Larger weight will be selected first. A weight of zero is the default value for the other variables. Note(user): Having a lot of different weights may slow down the priority queue operations if there is millions of variables.
SetStablePhase	Return type: void Arguments: bool is_stable By default, we alternate between a stable phase (better suited for finding SAT solution) and a more restart heavy phase more suited for proving UNSAT. This changes a bit the polarity heuristics and is controlled from within SatRestartPolicy.
Untrail	Return type: void Arguments: int target_trail_index Called on Untrail() so that we can update the set of possible decisions.
UpdateVariableActivityIncrement	Return type: void Updates the increment used for activity bumps. This is basically the same as decaying all the variable activities, but it is a lot more efficient.
UpdateWeightedSign	Return type: void Arguments: const std::vector<LiteralWithCoeff>& terms, Coefficient rhs Updates statistics about literal occurrences in constraints. Input is a canonical linear constraint of the form (terms <= rhs).