C++ Reference: class SatDecisionPolicy

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

NextBranch

Return type: Literal

Returns next decision to branch upon. This shouldn't be called if all the variables are assigned.

OnConflict

Return type: void

Called on a new conflict.

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.

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 occurences in constraints. Input is a canonical linear constraint of the form (terms <= rhs).