OR-Tools  8.2
Classes | Public Types | Public Member Functions | List of all members
SatSolver

Detailed Description

Definition at line 57 of file sat_solver.h.

Classes

struct  Decision
 

Public Types

enum  Status { ASSUMPTIONS_UNSAT , INFEASIBLE , FEASIBLE , LIMIT_REACHED }
 

Public Member Functions

 SatSolver ()
 
 SatSolver (Model *model)
 
 ~SatSolver ()
 
Model * model ()
 
void SetParameters (const SatParameters &parameters)
 
const SatParameters & parameters () const
 
void SetNumVariables (int num_variables)
 
int NumVariables () const
 
BooleanVariable NewBooleanVariable ()
 
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 AddLinearConstraint (bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
 
bool IsModelUnsat () const
 
void AddPropagator (SatPropagator *propagator)
 
void AddLastPropagator (SatPropagator *propagator)
 
void TakePropagatorOwnership (std::unique_ptr< SatPropagator > propagator)
 
void SetAssignmentPreference (Literal literal, double weight)
 
std::vector< std::pair< Literal, double > > AllPreferences () const
 
void ResetDecisionHeuristic ()
 
void ResetDecisionHeuristicAndSetAllPreferences (const std::vector< std::pair< Literal, double > > &prefs)
 
Status Solve ()
 
Status SolveWithTimeLimit (TimeLimit *time_limit)
 
Status ResetAndSolveWithGivenAssumptions (const std::vector< Literal > &assumptions)
 
void SetAssumptionLevel (int assumption_level)
 
int AssumptionLevel () const
 
std::vector< Literal > GetLastIncompatibleDecisions ()
 
int EnqueueDecisionAndBackjumpOnConflict (Literal true_literal)
 
int EnqueueDecisionAndBacktrackOnConflict (Literal true_literal)
 
bool EnqueueDecisionIfNotConflicting (Literal true_literal)
 
void Backtrack (int target_level)
 
bool RestoreSolverToAssumptionLevel ()
 
bool FinishPropagation ()
 
bool ResetToLevelZero ()
 
bool ResetWithGivenAssumptions (const std::vector< Literal > &assumptions)
 
bool ReapplyAssumptionsIfNeeded ()
 
Status UnsatStatus () const
 
template<typename Output >
void ExtractClauses (Output *out)
 
void TrackBinaryClauses (bool value)
 
bool AddBinaryClauses (const std::vector< BinaryClause > &clauses)
 
const std::vector< BinaryClause > & NewlyAddedBinaryClauses ()
 
void ClearNewlyAddedBinaryClauses ()
 
const std::vector< Decision > & Decisions () const
 
int CurrentDecisionLevel () const
 
const Trail & LiteralTrail () const
 
const VariablesAssignment & Assignment () const
 
int64 num_branches () const
 
int64 num_failures () const
 
int64 num_propagations () const
 
int64 num_restarts () const
 
double deterministic_time () const
 
void SaveDebugAssignment ()
 
bool ProblemIsPureSat () const
 
void SetDratProofHandler (DratProofHandler *drat_proof_handler)
 
void NotifyThatModelIsUnsat ()
 
bool AddClauseDuringSearch (absl::Span< const Literal > literals)
 
bool Propagate ()
 
void MinimizeSomeClauses (int decisions_budget)
 
void AdvanceDeterministicTime (TimeLimit *limit)
 
void ProcessNewlyFixedVariables ()
 
int64 NumFixedVariables () const
 

Member Enumeration Documentation

◆ Status

enum Status
Enumerator
ASSUMPTIONS_UNSAT 
INFEASIBLE 
FEASIBLE 
LIMIT_REACHED 

Definition at line 180 of file sat_solver.h.

Constructor & Destructor Documentation

◆ SatSolver() [1/2]

SatSolver ( )

Definition at line 37 of file sat_solver.cc.

◆ SatSolver() [2/2]

SatSolver ( Model *  model)
explicit

Definition at line 42 of file sat_solver.cc.

◆ ~SatSolver()

~SatSolver ( )

Definition at line 62 of file sat_solver.cc.

Member Function Documentation

◆ AddBinaryClause()

bool AddBinaryClause ( Literal  a,
Literal  b 
)

Definition at line 180 of file sat_solver.cc.

◆ AddBinaryClauses()

bool AddBinaryClauses ( const std::vector< BinaryClause > &  clauses)

Definition at line 918 of file sat_solver.cc.

◆ AddClauseDuringSearch()

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

Definition at line 134 of file sat_solver.cc.

◆ AddLastPropagator()

void AddLastPropagator ( SatPropagator *  propagator)

Definition at line 413 of file sat_solver.cc.

◆ AddLinearConstraint()

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

Definition at line 299 of file sat_solver.cc.

◆ AddProblemClause()

bool AddProblemClause ( absl::Span< const Literal >  literals)

Definition at line 203 of file sat_solver.cc.

◆ AddPropagator()

void AddPropagator ( SatPropagator *  propagator)

Definition at line 405 of file sat_solver.cc.

◆ AddTernaryClause()

bool AddTernaryClause ( Literal  a,
Literal  b,
Literal  c 
)

Definition at line 191 of file sat_solver.cc.

◆ AddUnitClause()

bool AddUnitClause ( Literal  true_literal)

Definition at line 164 of file sat_solver.cc.

◆ AdvanceDeterministicTime()

void AdvanceDeterministicTime ( TimeLimit *  limit)
inline

Definition at line 422 of file sat_solver.h.

◆ AllPreferences()

std::vector< std::pair< Literal, double > > AllPreferences ( ) const
inline

Definition at line 153 of file sat_solver.h.

◆ Assignment()

const VariablesAssignment & Assignment ( ) const
inline

Definition at line 362 of file sat_solver.h.

◆ AssumptionLevel()

int AssumptionLevel ( ) const
inline

Definition at line 220 of file sat_solver.h.

◆ Backtrack()

void Backtrack ( int  target_level)

Definition at line 888 of file sat_solver.cc.

◆ ClearNewlyAddedBinaryClauses()

void ClearNewlyAddedBinaryClauses ( )

Definition at line 936 of file sat_solver.cc.

◆ CurrentDecisionLevel()

int CurrentDecisionLevel ( ) const
inline

Definition at line 360 of file sat_solver.h.

◆ Decisions()

const std::vector< Decision > & Decisions ( ) const
inline

Definition at line 359 of file sat_solver.h.

◆ deterministic_time()

double deterministic_time ( ) const

Definition at line 92 of file sat_solver.cc.

◆ EnqueueDecisionAndBackjumpOnConflict()

int EnqueueDecisionAndBackjumpOnConflict ( Literal  true_literal)

Definition at line 499 of file sat_solver.cc.

◆ EnqueueDecisionAndBacktrackOnConflict()

int EnqueueDecisionAndBacktrackOnConflict ( Literal  true_literal)

Definition at line 861 of file sat_solver.cc.

◆ EnqueueDecisionIfNotConflicting()

bool EnqueueDecisionIfNotConflicting ( Literal  true_literal)

Definition at line 873 of file sat_solver.cc.

◆ ExtractClauses()

void ExtractClauses ( Output *  out)
inline

Definition at line 320 of file sat_solver.h.

◆ FinishPropagation()

bool FinishPropagation ( )

Definition at line 521 of file sat_solver.cc.

◆ GetLastIncompatibleDecisions()

std::vector< Literal > GetLastIncompatibleDecisions ( )

Definition at line 1272 of file sat_solver.cc.

◆ IsModelUnsat()

bool IsModelUnsat ( ) const
inline

Definition at line 136 of file sat_solver.h.

◆ LiteralTrail()

const Trail & LiteralTrail ( ) const
inline

Definition at line 361 of file sat_solver.h.

◆ MinimizeSomeClauses()

void MinimizeSomeClauses ( int  decisions_budget)

Definition at line 1247 of file sat_solver.cc.

◆ model()

Model * model ( )
inline

Definition at line 65 of file sat_solver.h.

◆ NewBooleanVariable()

BooleanVariable NewBooleanVariable ( )
inline

Definition at line 83 of file sat_solver.h.

◆ NewlyAddedBinaryClauses()

const std::vector< BinaryClause > & NewlyAddedBinaryClauses ( )

Definition at line 932 of file sat_solver.cc.

◆ NotifyThatModelIsUnsat()

void NotifyThatModelIsUnsat ( )
inline

Definition at line 401 of file sat_solver.h.

◆ num_branches()

int64 num_branches ( ) const

Definition at line 82 of file sat_solver.cc.

◆ num_failures()

int64 num_failures ( ) const

Definition at line 84 of file sat_solver.cc.

◆ num_propagations()

int64 num_propagations ( ) const

Definition at line 86 of file sat_solver.cc.

◆ num_restarts()

int64 num_restarts ( ) const

Definition at line 90 of file sat_solver.cc.

◆ NumFixedVariables()

int64 NumFixedVariables ( ) const
inline

Definition at line 432 of file sat_solver.h.

◆ NumVariables()

int NumVariables ( ) const
inline

Definition at line 82 of file sat_solver.h.

◆ parameters()

const SatParameters & parameters ( ) const

Definition at line 110 of file sat_solver.cc.

◆ ProblemIsPureSat()

bool ProblemIsPureSat ( ) const
inline

Definition at line 387 of file sat_solver.h.

◆ ProcessNewlyFixedVariables()

void ProcessNewlyFixedVariables ( )

Definition at line 1563 of file sat_solver.cc.

◆ Propagate()

bool Propagate ( )

Definition at line 1622 of file sat_solver.cc.

◆ ReapplyAssumptionsIfNeeded()

bool ReapplyAssumptionsIfNeeded ( )

Definition at line 554 of file sat_solver.cc.

◆ ResetAndSolveWithGivenAssumptions()

SatSolver::Status ResetAndSolveWithGivenAssumptions ( const std::vector< Literal > &  assumptions)

Definition at line 947 of file sat_solver.cc.

◆ ResetDecisionHeuristic()

void ResetDecisionHeuristic ( )
inline

Definition at line 156 of file sat_solver.h.

◆ ResetDecisionHeuristicAndSetAllPreferences()

void ResetDecisionHeuristicAndSetAllPreferences ( const std::vector< std::pair< Literal, double > > &  prefs)
inline

Definition at line 159 of file sat_solver.h.

◆ ResetToLevelZero()

bool ResetToLevelZero ( )

Definition at line 529 of file sat_solver.cc.

◆ ResetWithGivenAssumptions()

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

Definition at line 536 of file sat_solver.cc.

◆ RestoreSolverToAssumptionLevel()

bool RestoreSolverToAssumptionLevel ( )

Definition at line 511 of file sat_solver.cc.

◆ SaveDebugAssignment()

void SaveDebugAssignment ( )

Definition at line 442 of file sat_solver.cc.

◆ SetAssignmentPreference()

void SetAssignmentPreference ( Literal  literal,
double  weight 
)
inline

Definition at line 150 of file sat_solver.h.

◆ SetAssumptionLevel()

void SetAssumptionLevel ( int  assumption_level)

Definition at line 962 of file sat_solver.cc.

◆ SetDratProofHandler()

void SetDratProofHandler ( DratProofHandler *  drat_proof_handler)
inline

Definition at line 389 of file sat_solver.h.

◆ SetNumVariables()

void SetNumVariables ( int  num_variables)

Definition at line 64 of file sat_solver.cc.

◆ SetParameters()

void SetParameters ( const SatParameters &  parameters)

Definition at line 115 of file sat_solver.cc.

◆ Solve()

SatSolver::Status Solve ( )

Definition at line 972 of file sat_solver.cc.

◆ SolveWithTimeLimit()

SatSolver::Status SolveWithTimeLimit ( TimeLimit *  time_limit)

Definition at line 968 of file sat_solver.cc.

◆ TakePropagatorOwnership()

void TakePropagatorOwnership ( std::unique_ptr< SatPropagator >  propagator)
inline

Definition at line 142 of file sat_solver.h.

◆ TrackBinaryClauses()

void TrackBinaryClauses ( bool  value)
inline

Definition at line 345 of file sat_solver.h.

◆ UnsatStatus()

Status UnsatStatus ( ) const
inline

Definition at line 309 of file sat_solver.h.

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