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

Return type: double

Arguments: Literal l

Returns the current activity of a BooleanVariable.


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.


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.


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.


Return type: bool


Return type: void

Arguments: bool save_phase

This is used to temporarily disable phase_saving when we do some probing during search for instance.


Return type: Literal

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


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.


Return type: explicit

Arguments: Model* model


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.


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.


Return type: void

Arguments: int target_trail_index

Called on Untrail() so that we can update the set of possible decisions.


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.


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