Detailed Description

Definition at line 64 of file sat_solver.h.

#include <sat_solver.h>

Classes
struct	Counters

Public Types
enum	Status { ASSUMPTIONS_UNSAT , INFEASIBLE , FEASIBLE , LIMIT_REACHED }
typedef absl::FunctionRef< void(ClauseId, absl::Span< const Literal >)>	ConflictCallback

Public Member Functions
	SatSolver ()
	SatSolver (Model *model)
	SatSolver (const SatSolver &)=delete
SatSolver &	operator= (const SatSolver &)=delete
	~SatSolver ()
Model *	model ()
void	SetParameters (const SatParameters &parameters)
const SatParameters &	parameters () const
void	SetNumVariables (int num_variables)
int	NumVariables () const
BooleanVariable	NewBooleanVariable ()
ABSL_MUST_USE_RESULT bool	AddUnitClause (Literal true_literal)
bool	AddBinaryClause (Literal a, Literal b)
bool	AddTernaryClause (Literal a, Literal b, Literal c)
bool	AddProblemClause (absl::Span< const Literal > literals, bool shared=false)
bool	AddLinearConstraint (bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< Literal > enforcement_literals, std::vector< LiteralWithCoeff > cst)
bool	AddLinearConstraint (bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
bool	ModelIsUnsat () const
void	AddPropagator (SatPropagator *propagator)
void	AddLastPropagator (SatPropagator *propagator)
void	TakePropagatorOwnership (std::unique_ptr< SatPropagator > propagator)
void	SetAssignmentPreference (Literal literal, float weight)
std::vector< std::pair< Literal, float > >	AllPreferences () const
void	ResetDecisionHeuristic ()
Status	Solve ()
Status	SolveWithTimeLimit (TimeLimit *time_limit)
Status	ResetAndSolveWithGivenAssumptions (const std::vector< Literal > &assumptions, int64_t max_number_of_conflicts=-1)
void	SetAssumptionLevel (int assumption_level)
int	AssumptionLevel () const
std::vector< Literal >	GetLastIncompatibleDecisions ()
std::vector< Literal >	GetDecisionsFixing (absl::Span< const Literal > literals)
int	EnqueueDecisionAndBackjumpOnConflict (Literal true_literal, std::optional< ConflictCallback > callback=std::nullopt)
Status	EnqueueDecisionAndBacktrackOnConflict (Literal true_literal, int *first_propagation_index=nullptr)
bool	EnqueueDecisionIfNotConflicting (Literal true_literal)
void	Backtrack (int target_level)
bool	BacktrackAndPropagateReimplications (int target_level)
ABSL_MUST_USE_RESULT bool	FinishPropagation (std::optional< ConflictCallback > callback=std::nullopt)
ABSL_MUST_USE_RESULT bool	ResetToLevelZero ()
bool	ResetWithGivenAssumptions (const std::vector< Literal > &assumptions)
bool	ReapplyAssumptionsIfNeeded ()
Status	UnsatStatus () const
template<typename Output>
bool	ExtractClauses (Output *out)
void	TrackBinaryClauses (bool value)
bool	AddBinaryClauses (absl::Span< const BinaryClause > clauses)
const std::vector< BinaryClause > &	NewlyAddedBinaryClauses ()
void	ClearNewlyAddedBinaryClauses ()
const std::vector< LiteralWithTrailIndex > &	Decisions () const
int	CurrentDecisionLevel () const
const Trail &	LiteralTrail () const
const VariablesAssignment &	Assignment () const
int64_t	num_branches () const
int64_t	num_failures () const
int64_t	num_propagations () const
int64_t	num_backtracks () const
int64_t	num_restarts () const
int64_t	num_backtracks_to_root () const
void	IncreaseNumRestarts ()
Counters	counters () const
double	deterministic_time () const
void	SaveDebugAssignment ()
void	LoadDebugSolution (absl::Span< const Literal > solution)
void	NotifyThatModelIsUnsat ()
bool	AddClauseDuringSearch (absl::Span< const Literal > literals)
ABSL_MUST_USE_RESULT bool	Propagate ()
bool	MinimizeByPropagation (double dtime, bool minimize_new_clauses_only=false)
void	AdvanceDeterministicTime (TimeLimit *limit)
void	ProcessNewlyFixedVariables ()
int64_t	NumFixedVariables () const
SolverLogger *	mutable_logger ()
void	ProcessCurrentConflict (std::optional< ConflictCallback > callback=std::nullopt)
void	EnsureNewClauseIndexInitialized ()
void	EnableChronologicalBacktracking (bool value)
bool	PropagationIsDone () const
void	BlockClauseDeletion (bool value)

Member Typedef Documentation

◆ ConflictCallback

typedef absl::FunctionRef<void(ClauseId, absl::Span<const Literal>)> operations_research::sat::SatSolver::ConflictCallback

Definition at line 69 of file sat_solver.h.

Member Enumeration Documentation

◆ Status

enum operations_research::sat::SatSolver::Status

Enumerator
ASSUMPTIONS_UNSAT
INFEASIBLE
FEASIBLE
LIMIT_REACHED

Definition at line 206 of file sat_solver.h.

Constructor & Destructor Documentation

◆ SatSolver() [1/3]

operations_research::sat::SatSolver::SatSolver ( )

Definition at line 59 of file sat_solver.cc.

◆ SatSolver() [2/3]

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

explicit

Definition at line 64 of file sat_solver.cc.

◆ SatSolver() [3/3]

operations_research::sat::SatSolver::SatSolver ( const SatSolver & )

delete

◆ ~SatSolver()

operations_research::sat::SatSolver::~SatSolver ( )

Definition at line 88 of file sat_solver.cc.

Member Function Documentation

◆ AddBinaryClause()

bool operations_research::sat::SatSolver::AddBinaryClause	(	Literal	a,
		Literal	b )

Definition at line 203 of file sat_solver.cc.

◆ AddBinaryClauses()

bool operations_research::sat::SatSolver::AddBinaryClauses ( absl::Span< const BinaryClause > clauses )

Definition at line 1574 of file sat_solver.cc.

◆ AddClauseDuringSearch()

bool operations_research::sat::SatSolver::AddClauseDuringSearch ( absl::Span< const Literal > literals )

Definition at line 162 of file sat_solver.cc.

◆ AddLastPropagator()

void operations_research::sat::SatSolver::AddLastPropagator ( SatPropagator * propagator )

Definition at line 543 of file sat_solver.cc.

◆ AddLinearConstraint() [1/2]

bool operations_research::sat::SatSolver::AddLinearConstraint	(	bool	use_lower_bound,
		Coefficient	lower_bound,
		bool	use_upper_bound,
		Coefficient	upper_bound,
		std::vector< Literal > *	enforcement_literals,
		std::vector< LiteralWithCoeff > *	cst )

Definition at line 422 of file sat_solver.cc.

◆ AddLinearConstraint() [2/2]

bool operations_research::sat::SatSolver::AddLinearConstraint	(	bool	use_lower_bound,
		Coefficient	lower_bound,
		bool	use_upper_bound,
		Coefficient	upper_bound,
		std::vector< LiteralWithCoeff > *	cst )

inline

Definition at line 155 of file sat_solver.h.

◆ AddProblemClause()

bool operations_research::sat::SatSolver::AddProblemClause	(	absl::Span< const Literal >	literals,
		bool	shared = false )

Definition at line 217 of file sat_solver.cc.

◆ AddPropagator()

void operations_research::sat::SatSolver::AddPropagator ( SatPropagator * propagator )

Definition at line 536 of file sat_solver.cc.

◆ AddTernaryClause()

bool operations_research::sat::SatSolver::AddTernaryClause	(	Literal	a,
		Literal	b,
		Literal	c )

Definition at line 207 of file sat_solver.cc.

◆ AddUnitClause()

bool operations_research::sat::SatSolver::AddUnitClause ( Literal true_literal )

Definition at line 199 of file sat_solver.cc.

◆ AdvanceDeterministicTime()

void operations_research::sat::SatSolver::AdvanceDeterministicTime ( TimeLimit * limit )

inline

Definition at line 502 of file sat_solver.h.

◆ AllPreferences()

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

inline

Definition at line 186 of file sat_solver.h.

◆ Assignment()

const VariablesAssignment & operations_research::sat::SatSolver::Assignment ( ) const

inline

Definition at line 420 of file sat_solver.h.

◆ AssumptionLevel()

int operations_research::sat::SatSolver::AssumptionLevel ( ) const

inline

Definition at line 247 of file sat_solver.h.

◆ Backtrack()

void operations_research::sat::SatSolver::Backtrack ( int target_level )

Definition at line 1540 of file sat_solver.cc.

◆ BacktrackAndPropagateReimplications()

bool operations_research::sat::SatSolver::BacktrackAndPropagateReimplications ( int target_level )

inline

Definition at line 327 of file sat_solver.h.

◆ BlockClauseDeletion()

void operations_research::sat::SatSolver::BlockClauseDeletion ( bool value )

inline

Definition at line 554 of file sat_solver.h.

◆ ClearNewlyAddedBinaryClauses()

void operations_research::sat::SatSolver::ClearNewlyAddedBinaryClauses ( )

Definition at line 1588 of file sat_solver.cc.

◆ counters()

Counters operations_research::sat::SatSolver::counters ( ) const

inline

Definition at line 461 of file sat_solver.h.

◆ CurrentDecisionLevel()

int operations_research::sat::SatSolver::CurrentDecisionLevel ( ) const

inline

Definition at line 418 of file sat_solver.h.

◆ Decisions()

const std::vector< LiteralWithTrailIndex > & operations_research::sat::SatSolver::Decisions ( ) const

inline

Definition at line 415 of file sat_solver.h.

◆ deterministic_time()

double operations_research::sat::SatSolver::deterministic_time ( ) const

Definition at line 118 of file sat_solver.cc.

◆ EnableChronologicalBacktracking()

void operations_research::sat::SatSolver::EnableChronologicalBacktracking ( bool value )

inline

Definition at line 539 of file sat_solver.h.

◆ EnqueueDecisionAndBackjumpOnConflict()

int operations_research::sat::SatSolver::EnqueueDecisionAndBackjumpOnConflict	(	Literal	true_literal,
		std::optional< ConflictCallback >	callback = std::nullopt )

Definition at line 624 of file sat_solver.cc.

◆ EnqueueDecisionAndBacktrackOnConflict()

SatSolver::Status operations_research::sat::SatSolver::EnqueueDecisionAndBacktrackOnConflict	(	Literal	true_literal,
		int *	first_propagation_index = nullptr )

Definition at line 1511 of file sat_solver.cc.

◆ EnqueueDecisionIfNotConflicting()

bool operations_research::sat::SatSolver::EnqueueDecisionIfNotConflicting ( Literal true_literal )

Definition at line 1525 of file sat_solver.cc.

◆ EnsureNewClauseIndexInitialized()

void operations_research::sat::SatSolver::EnsureNewClauseIndexInitialized ( )

inline

Definition at line 535 of file sat_solver.h.

◆ ExtractClauses()

template<typename Output>

bool operations_research::sat::SatSolver::ExtractClauses ( Output * out )

inline

Definition at line 385 of file sat_solver.h.

◆ FinishPropagation()

bool operations_research::sat::SatSolver::FinishPropagation ( std::optional< ConflictCallback > callback = std::nullopt )

Definition at line 641 of file sat_solver.cc.

◆ GetDecisionsFixing()

std::vector< Literal > operations_research::sat::SatSolver::GetDecisionsFixing ( absl::Span< const Literal > literals )

Definition at line 1768 of file sat_solver.cc.

◆ GetLastIncompatibleDecisions()

std::vector< Literal > operations_research::sat::SatSolver::GetLastIncompatibleDecisions ( )

Definition at line 1747 of file sat_solver.cc.

◆ IncreaseNumRestarts()

void operations_research::sat::SatSolver::IncreaseNumRestarts ( )

inline

Definition at line 436 of file sat_solver.h.

◆ LiteralTrail()

const Trail & operations_research::sat::SatSolver::LiteralTrail ( ) const

inline

Definition at line 419 of file sat_solver.h.

◆ LoadDebugSolution()

void operations_research::sat::SatSolver::LoadDebugSolution ( absl::Span< const Literal > solution )

Definition at line 570 of file sat_solver.cc.

◆ MinimizeByPropagation()

bool operations_research::sat::SatSolver::MinimizeByPropagation	(	double	dtime,
		bool	minimize_new_clauses_only = false )

◆ model()

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

inline

Definition at line 82 of file sat_solver.h.

◆ ModelIsUnsat()

bool operations_research::sat::SatSolver::ModelIsUnsat ( ) const

inline

Definition at line 169 of file sat_solver.h.

◆ mutable_logger()

SolverLogger * operations_research::sat::SatSolver::mutable_logger ( )

inline

Definition at line 520 of file sat_solver.h.

◆ NewBooleanVariable()

BooleanVariable operations_research::sat::SatSolver::NewBooleanVariable ( )

inline

Definition at line 100 of file sat_solver.h.

◆ NewlyAddedBinaryClauses()

const std::vector< BinaryClause > & operations_research::sat::SatSolver::NewlyAddedBinaryClauses ( )

Definition at line 1584 of file sat_solver.cc.

◆ NotifyThatModelIsUnsat()

void operations_research::sat::SatSolver::NotifyThatModelIsUnsat ( )

inline

Definition at line 482 of file sat_solver.h.

◆ num_backtracks()

int64_t operations_research::sat::SatSolver::num_backtracks ( ) const

Definition at line 111 of file sat_solver.cc.

◆ num_backtracks_to_root()

int64_t operations_research::sat::SatSolver::num_backtracks_to_root ( ) const

Definition at line 114 of file sat_solver.cc.

◆ num_branches()

int64_t operations_research::sat::SatSolver::num_branches ( ) const

Definition at line 103 of file sat_solver.cc.

◆ num_failures()

int64_t operations_research::sat::SatSolver::num_failures ( ) const

Definition at line 105 of file sat_solver.cc.

◆ num_propagations()

int64_t operations_research::sat::SatSolver::num_propagations ( ) const

Definition at line 107 of file sat_solver.cc.

◆ num_restarts()

int64_t operations_research::sat::SatSolver::num_restarts ( ) const

Definition at line 113 of file sat_solver.cc.

◆ NumFixedVariables()

int64_t operations_research::sat::SatSolver::NumFixedVariables ( ) const

inline

Definition at line 512 of file sat_solver.h.

◆ NumVariables()

int operations_research::sat::SatSolver::NumVariables ( ) const

inline

Definition at line 99 of file sat_solver.h.

◆ operator=()

SatSolver & operations_research::sat::SatSolver::operator= ( const SatSolver & )

delete

◆ parameters()

const SatParameters & operations_research::sat::SatSolver::parameters ( ) const

Definition at line 136 of file sat_solver.cc.

◆ ProcessCurrentConflict()

void operations_research::sat::SatSolver::ProcessCurrentConflict ( std::optional< ConflictCallback > callback = std::nullopt )

Definition at line 738 of file sat_solver.cc.

◆ ProcessNewlyFixedVariables()

void operations_research::sat::SatSolver::ProcessNewlyFixedVariables ( )

Definition at line 2017 of file sat_solver.cc.

◆ Propagate()

bool operations_research::sat::SatSolver::Propagate ( )

Definition at line 2119 of file sat_solver.cc.

◆ PropagationIsDone()

bool operations_research::sat::SatSolver::PropagationIsDone ( ) const

Definition at line 2106 of file sat_solver.cc.

◆ ReapplyAssumptionsIfNeeded()

bool operations_research::sat::SatSolver::ReapplyAssumptionsIfNeeded ( )

Definition at line 694 of file sat_solver.cc.

◆ ResetAndSolveWithGivenAssumptions()

SatSolver::Status operations_research::sat::SatSolver::ResetAndSolveWithGivenAssumptions	(	const std::vector< Literal > &	assumptions,
		int64_t	max_number_of_conflicts = -1 )

Definition at line 1599 of file sat_solver.cc.

◆ ResetDecisionHeuristic()

void operations_research::sat::SatSolver::ResetDecisionHeuristic ( )

inline

Definition at line 189 of file sat_solver.h.

◆ ResetToLevelZero()

bool operations_research::sat::SatSolver::ResetToLevelZero ( )

Definition at line 669 of file sat_solver.cc.

◆ ResetWithGivenAssumptions()

bool operations_research::sat::SatSolver::ResetWithGivenAssumptions ( const std::vector< Literal > & assumptions )

Definition at line 677 of file sat_solver.cc.

◆ SaveDebugAssignment()

void operations_research::sat::SatSolver::SaveDebugAssignment ( )

Definition at line 562 of file sat_solver.cc.

◆ SetAssignmentPreference()

void operations_research::sat::SatSolver::SetAssignmentPreference	(	Literal	literal,
		float	weight )

inline

Definition at line 183 of file sat_solver.h.

◆ SetAssumptionLevel()

void operations_research::sat::SatSolver::SetAssumptionLevel ( int assumption_level )

Definition at line 1616 of file sat_solver.cc.

◆ SetNumVariables()

void operations_research::sat::SatSolver::SetNumVariables ( int num_variables )

Definition at line 90 of file sat_solver.cc.

◆ SetParameters()

void operations_research::sat::SatSolver::SetParameters ( const SatParameters & parameters )

Definition at line 141 of file sat_solver.cc.

◆ Solve()

SatSolver::Status operations_research::sat::SatSolver::Solve ( )

Definition at line 1633 of file sat_solver.cc.

◆ SolveWithTimeLimit()

SatSolver::Status operations_research::sat::SatSolver::SolveWithTimeLimit ( TimeLimit * time_limit )

Definition at line 1628 of file sat_solver.cc.

◆ TakePropagatorOwnership()

void operations_research::sat::SatSolver::TakePropagatorOwnership ( std::unique_ptr< SatPropagator > propagator )

inline

Definition at line 175 of file sat_solver.h.

◆ TrackBinaryClauses()

void operations_research::sat::SatSolver::TrackBinaryClauses ( bool value )

inline

Definition at line 410 of file sat_solver.h.

◆ UnsatStatus()

Status operations_research::sat::SatSolver::UnsatStatus ( ) const

inline

Definition at line 368 of file sat_solver.h.

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

ortools/sat/sat_solver.h
ortools/sat/sat_solver.cc

Detailed Description

Classes

Public Types

Public Member Functions

Member Typedef Documentation

◆ ConflictCallback

Member Enumeration Documentation

◆ Status

Constructor & Destructor Documentation

◆ SatSolver() [1/3]

◆ SatSolver() [2/3]

◆ SatSolver() [3/3]

◆ ~SatSolver()

Member Function Documentation

◆ AddBinaryClause()

◆ AddBinaryClauses()

◆ AddClauseDuringSearch()

◆ AddLastPropagator()

◆ AddLinearConstraint() [1/2]

◆ AddLinearConstraint() [2/2]

◆ AddProblemClause()

◆ AddPropagator()

◆ AddTernaryClause()

◆ AddUnitClause()

◆ AdvanceDeterministicTime()

◆ AllPreferences()

◆ Assignment()

◆ AssumptionLevel()

◆ Backtrack()

◆ BacktrackAndPropagateReimplications()

◆ BlockClauseDeletion()

◆ ClearNewlyAddedBinaryClauses()

◆ counters()

◆ CurrentDecisionLevel()

◆ Decisions()

◆ deterministic_time()

◆ EnableChronologicalBacktracking()

◆ EnqueueDecisionAndBackjumpOnConflict()

◆ EnqueueDecisionAndBacktrackOnConflict()

◆ EnqueueDecisionIfNotConflicting()

◆ EnsureNewClauseIndexInitialized()

◆ ExtractClauses()

◆ FinishPropagation()

◆ GetDecisionsFixing()

◆ GetLastIncompatibleDecisions()

◆ IncreaseNumRestarts()

◆ LiteralTrail()

◆ LoadDebugSolution()

◆ MinimizeByPropagation()

◆ model()

◆ ModelIsUnsat()

◆ mutable_logger()

◆ NewBooleanVariable()

◆ NewlyAddedBinaryClauses()

◆ NotifyThatModelIsUnsat()

◆ num_backtracks()

◆ num_backtracks_to_root()

◆ num_branches()

◆ num_failures()

◆ num_propagations()

◆ num_restarts()

◆ NumFixedVariables()

◆ NumVariables()

◆ operator=()

◆ parameters()

◆ ProcessCurrentConflict()

◆ ProcessNewlyFixedVariables()

◆ Propagate()

◆ PropagationIsDone()

◆ ReapplyAssumptionsIfNeeded()

◆ ResetAndSolveWithGivenAssumptions()

◆ ResetDecisionHeuristic()

◆ ResetToLevelZero()

◆ ResetWithGivenAssumptions()

◆ SaveDebugAssignment()

◆ SetAssignmentPreference()

◆ SetAssumptionLevel()

◆ SetNumVariables()

◆ SetParameters()

◆ Solve()