Google OR-Tools v9.11
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
Public Member Functions | List of all members
operations_research::sat::SatDecisionPolicy Class Reference

#include <sat_decision.h>

Public Member Functions

 SatDecisionPolicy (Model *model)
 
void IncreaseNumVariables (int num_variables)
 
void ResetDecisionHeuristic ()
 
Literal NextBranch ()
 
void BumpVariableActivities (absl::Span< const Literal > literals)
 
void UpdateVariableActivityIncrement ()
 
void Untrail (int target_trail_index)
 Called on Untrail() so that we can update the set of possible decisions.
 
void BeforeConflict (int trail_index)
 
void SetStablePhase (bool is_stable)
 
bool InStablePhase () const
 
void MaybeEnablePhaseSaving (bool save_phase)
 
void SetAssignmentPreference (Literal literal, float weight)
 
std::vector< std::pair< Literal, float > > AllPreferences () const
 Returns the vector of the current assignment preferences.
 
double Activity (Literal l) const
 Returns the current activity of a BooleanVariable.
 
void SetTargetPolarity (Literal l)
 Like SetAssignmentPreference() but it can be overridden by phase-saving.
 
absl::Span< const Literal > GetBestPartialAssignment () const
 
void ClearBestPartialAssignment ()
 

Detailed Description

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

Definition at line 37 of file sat_decision.h.

Constructor & Destructor Documentation

◆ SatDecisionPolicy()

operations_research::sat::SatDecisionPolicy::SatDecisionPolicy ( Model * model)
explicit

Definition at line 37 of file sat_decision.cc.

Member Function Documentation

◆ Activity()

double operations_research::sat::SatDecisionPolicy::Activity ( Literal l) const
inline

Returns the current activity of a BooleanVariable.

Definition at line 104 of file sat_decision.h.

◆ AllPreferences()

std::vector< std::pair< Literal, float > > operations_research::sat::SatDecisionPolicy::AllPreferences ( ) const

Returns the vector of the current assignment preferences.

Todo
(user): we currently assume that if the tie_breaker is zero then no preference was set (which is not 100% correct). Fix that.

Definition at line 264 of file sat_decision.cc.

◆ BeforeConflict()

void operations_research::sat::SatDecisionPolicy::BeforeConflict ( 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.

Definition at line 69 of file sat_decision.cc.

◆ BumpVariableActivities()

void operations_research::sat::SatDecisionPolicy::BumpVariableActivities ( absl::Span< const 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.

Note
we don't really need to bump level 0 variables since they will never be backtracked over. However it is faster to simply bump them.

Definition at line 278 of file sat_decision.cc.

◆ ClearBestPartialAssignment()

void operations_research::sat::SatDecisionPolicy::ClearBestPartialAssignment ( )
inline

Definition at line 116 of file sat_decision.h.

◆ GetBestPartialAssignment()

absl::Span< const Literal > operations_research::sat::SatDecisionPolicy::GetBestPartialAssignment ( ) const
inline

Definition at line 113 of file sat_decision.h.

◆ IncreaseNumVariables()

void operations_research::sat::SatDecisionPolicy::IncreaseNumVariables ( 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.

Update the priority queue. Note that each addition is in O(1) because the priority is 0.0.

Definition at line 42 of file sat_decision.cc.

◆ InStablePhase()

bool operations_research::sat::SatDecisionPolicy::InStablePhase ( ) const
inline

Definition at line 79 of file sat_decision.h.

◆ MaybeEnablePhaseSaving()

void operations_research::sat::SatDecisionPolicy::MaybeEnablePhaseSaving ( bool save_phase)
inline

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

Definition at line 83 of file sat_decision.h.

◆ NextBranch()

Literal operations_research::sat::SatDecisionPolicy::NextBranch ( )

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

Lazily initialize var_ordering_ if needed.

Choose the variable.

Todo
(user): This may not be super efficient if almost all the variables are assigned.

The loop is done this way in order to leave the final choice in the heap.

Choose its polarity (i.e. True of False).

Definition at line 330 of file sat_decision.cc.

◆ ResetDecisionHeuristic()

void operations_research::sat::SatDecisionPolicy::ResetDecisionHeuristic ( )

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.

Definition at line 141 of file sat_decision.cc.

◆ SetAssignmentPreference()

void operations_research::sat::SatDecisionPolicy::SetAssignmentPreference ( Literal literal,
float 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.

The tie_breaker is changed, so we need to reinitialize the priority queue.

Note
this doesn't change the activity though.

Definition at line 250 of file sat_decision.cc.

◆ SetStablePhase()

void operations_research::sat::SatDecisionPolicy::SetStablePhase ( bool is_stable)
inline

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.

Definition at line 78 of file sat_decision.h.

◆ SetTargetPolarity()

void operations_research::sat::SatDecisionPolicy::SetTargetPolarity ( Literal l)
inline

Like SetAssignmentPreference() but it can be overridden by phase-saving.

Definition at line 110 of file sat_decision.h.

◆ Untrail()

void operations_research::sat::SatDecisionPolicy::Untrail ( int target_trail_index)

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

Todo
(user): avoid looping twice over the trail?

The ERWA parameter between the new estimation of the learning rate and the old one.

Todo
(user): Expose parameters for these values.

This counts the number of conflicts since the assignment of the variable at the current trail_index that we are about to untrail.

Todo
(user): This heuristic can make this code quite slow because all the untrailed variable will cause a priority queue update.

Trail index of the next variable that will need a priority queue update.

Invariant.

Definition at line 389 of file sat_decision.cc.

◆ UpdateVariableActivityIncrement()

void operations_research::sat::SatDecisionPolicy::UpdateVariableActivityIncrement ( )

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.

Definition at line 326 of file sat_decision.cc.

The documentation for this class was generated from the following files: