operations_research::sat::RestartPolicy Class Reference

Contain the logic to decide when to restart a SAT tree search. More...

#include <restart.h>

Public Member Functions
	RestartPolicy (Model *model)
void	Reset ()
	Resets the policy using the current model parameters.
bool	ShouldRestart ()
void	OnConflict (int conflict_trail_index, int conflict_decision_level, int conflict_lbd)
int	NumRestarts () const
	Returns the number of restarts since the last Reset().
std::string	InfoString () const
	Returns a string with the current restart statistics.
double	LbdAverageSinceReset () const

Detailed Description

Contain the logic to decide when to restart a SAT tree search.

Definition at line 32 of file restart.h.

Constructor & Destructor Documentation

RestartPolicy()

operations_research::sat::RestartPolicy::RestartPolicy ( Model * model )

inlineexplicit

Definition at line 34 of file restart.h.

Member Function Documentation

InfoString()

std::string operations_research::sat::RestartPolicy::InfoString

(

)

const

Returns a string with the current restart statistics.

Definition at line 180 of file restart.cc.

LbdAverageSinceReset()

double operations_research::sat::RestartPolicy::LbdAverageSinceReset ( ) const

inline

Definition at line 60 of file restart.h.

NumRestarts()

int operations_research::sat::RestartPolicy::NumRestarts ( ) const

inline

Returns the number of restarts since the last Reset().

Definition at line 55 of file restart.h.

OnConflict()

void operations_research::sat::RestartPolicy::OnConflict	(	int	conflict_trail_index,
		int	conflict_decision_level,
		int	conflict_lbd )

This will be called by the solver engine after each conflict. The arguments reflect the state of the solver when the conflict was detected and before the backjump.

Decrement the restart counter if needed.

Block the restart. Note(user): glucose only activate this after 10000 conflicts.

Definition at line 151 of file restart.cc.

Reset()

void operations_research::sat::RestartPolicy::Reset

(

)

Resets the policy using the current model parameters.

Compute the list of restart algorithms to cycle through.

Todo

(user): for some reason, strategies_.assign() does not work as the returned type of the proto enum iterator is int ?!

Definition at line 30 of file restart.cc.

ShouldRestart()

bool operations_research::sat::RestartPolicy::ShouldRestart

(

)

Returns true if the solver should be restarted before the next decision is taken. Note that this will return true just once and then assumes that the search was restarted and starts worrying about the next restart.

Strategy switch?

The LUBY_RESTART strategy is considered the "stable" mode and we change the polariy heuristic while under it.

Reset the various restart strategies.

Definition at line 88 of file restart.cc.

---

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

• ortools/sat/restart.h
• ortools/sat/restart.cc