#include <sat_solver.h>

Classes
struct	Counters

struct	Decision

Public Types
enum	Status { ASSUMPTIONS_UNSAT , INFEASIBLE , FEASIBLE , LIMIT_REACHED }

Public Member Functions
	SatSolver ()

	SatSolver (Model *model)

	SatSolver (const SatSolver &)=delete
	This type is neither copyable nor movable.

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)
	Same as AddProblemClause() below, but for small clauses.

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

bool	AddProblemClause (absl::Span< const Literal > literals, bool is_safe=true)

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

bool	ModelIsUnsat () const

bool	IsModelUnsat () 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 ()

int	EnqueueDecisionAndBackjumpOnConflict (Literal true_literal)

Status	EnqueueDecisionAndBacktrackOnConflict (Literal true_literal, int *first_propagation_index=nullptr)

bool	EnqueueDecisionIfNotConflicting (Literal true_literal)

void	Backtrack (int target_level)

bool	RestoreSolverToAssumptionLevel ()

ABSL_MUST_USE_RESULT bool	FinishPropagation ()

ABSL_MUST_USE_RESULT 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_t	num_branches () const
	Some statistics since the creation of the solver.

int64_t	num_failures () const

int64_t	num_propagations () const

int64_t	num_backtracks () const

int64_t	num_restarts () const

Counters	counters () const

double	deterministic_time () const

void	SaveDebugAssignment ()

void	LoadDebugSolution (const std::vector< Literal > &solution)

void	SetDratProofHandler (DratProofHandler *drat_proof_handler)

void	NotifyThatModelIsUnsat ()

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

ABSL_MUST_USE_RESULT bool	Propagate ()

bool	MinimizeByPropagation (double dtime)

void	AdvanceDeterministicTime (TimeLimit *limit)

void	ProcessNewlyFixedVariables ()
	Simplifies the problem when new variables are assigned at level 0.

int64_t	NumFixedVariables () const

SolverLogger *	mutable_logger ()
	Hack to allow to temporarily disable logging if it is enabled.

void	ProcessCurrentConflict ()

Detailed Description

The main SAT solver. It currently implements the CDCL algorithm. See http://en.wikipedia.org/wiki/Conflict_Driven_Clause_Learning

Definition at line 63 of file sat_solver.h.

Member Enumeration Documentation

◆ Status

enum operations_research::sat::SatSolver::Status

Solves the problem and returns its status. An empty problem is considered to be SAT.

Note: the conflict limit applies only to this function and starts counting from the time it is called.

This will restart from the current solver configuration. If a previous call to Solve() was interrupted by a conflict or time limit, calling this again will resume the search exactly as it would have continued.

Note: this will use the TimeLimit singleton, so the time limit will be counted since the last time TimeLimit was reset, not from the start of this function.

Enumerator
ASSUMPTIONS_UNSAT
INFEASIBLE
FEASIBLE
LIMIT_REACHED

Definition at line 187 of file sat_solver.h.

Constructor & Destructor Documentation

◆ SatSolver() [1/3]

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

Definition at line 57 of file sat_solver.cc.

◆ SatSolver() [2/3]

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

explicit

Definition at line 63 of file sat_solver.cc.

◆ SatSolver() [3/3]

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

delete

This type is neither copyable nor movable.

◆ ~SatSolver()

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

Definition at line 83 of file sat_solver.cc.

Member Function Documentation

◆ AddBinaryClause()

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

Same as AddProblemClause() below, but for small clauses.

Definition at line 196 of file sat_solver.cc.

◆ AddBinaryClauses()

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

Definition at line 1070 of file sat_solver.cc.

◆ AddClauseDuringSearch()

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

Adds a clause at any level of the tree and propagate any new deductions. Returns false if the model becomes UNSAT. Important: We currently do not support adding a clause that is already falsified at a positive decision level. Doing that will cause a check fail.

Todo: (user): Backjump and propagate on a falsified clause? this is currently not needed.

Let filter clauses if we are at level zero

Todo: (user): We generate in some corner cases clauses with literals[0].Variable() == literals[1].Variable(). Avoid doing that and adding such binary clauses to the graph?

Tricky: Even if nothing new is propagated, calling Propagate() might, via the LP, deduce new things. This is problematic because some code assumes that when we create newly associated literals, nothing else changes.

Definition at line 159 of file sat_solver.cc.

◆ AddLastPropagator()

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

Definition at line 452 of file sat_solver.cc.

◆ AddLinearConstraint()

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

Adds a pseudo-Boolean constraint to the problem. Returns false if the problem is detected to be UNSAT. If the constraint is always true, this detects it and does nothing.

Note(user): There is an optimization if the same constraint is added consecutively (even if the bounds are different). This is particularly useful for an optimization problem when we want to constrain the objective of the problem more and more. Just re-adding such constraint is relatively efficient.

OVERFLOW: The sum of the absolute value of all the coefficients in the constraint must not overflow. This is currently CHECKed().

Todo: (user): Instead of failing, implement an error handling code.

We need to "re-canonicalize" in case some literal were fixed while we processed one direction.

We transform the constraint into an upper-bounded one.

Tricky: The PropagationIsDone() condition shouldn't change anything for a pure SAT problem, however in the CP-SAT context, calling Propagate() can tigger computation (like the LP) even if no domain changed since the last call. We do not want to do that.

Definition at line 355 of file sat_solver.cc.

◆ AddProblemClause()

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

Adds a clause to the problem. Returns false if the problem is detected to be UNSAT. If is_safe is false, we will do some basic presolving like removing duplicate literals.

Todo: (user): Rename this to AddClause(), also get rid of the specialized AddUnitClause(), AddBinaryClause() and AddTernaryClause() since they just end up calling this?

Note(user): we assume there is no duplicate literals in the clauses added here if is_safe is true. Most of the code works, but some advanced algo might be wrong/suboptimal if this is the case. So even when presolve is off we need some "cleanup" to enforce this invariant. Alternatively we could have robut algo in all the stack, but that seems a worse design.

Filter already assigned literals.

Tricky: The PropagationIsDone() condition shouldn't change anything for a pure SAT problem, however in the CP-SAT context, calling Propagate() can tigger computation (like the LP) even if no domain changed since the last call. We do not want to do that.

Definition at line 209 of file sat_solver.cc.

◆ AddPropagator()

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

Adds and registers the given propagator with the sat solver. Note that during propagation, they will be called in the order they were added.

Definition at line 445 of file sat_solver.cc.

◆ AddTernaryClause()

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

Definition at line 200 of file sat_solver.cc.

◆ AddUnitClause()

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

Fixes a variable so that the given literal is true. This can be used to solve a subproblem where some variables are fixed. Note that it is more efficient to add such unit clause before all the others. Returns false if the problem is detected to be UNSAT.

Definition at line 192 of file sat_solver.cc.

◆ AdvanceDeterministicTime()

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

inline

Advance the given time limit with all the deterministic time that was elapsed since last call.

Definition at line 475 of file sat_solver.h.

◆ AllPreferences()

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

inline

Definition at line 167 of file sat_solver.h.

◆ Assignment()

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

inline

Definition at line 388 of file sat_solver.h.

◆ AssumptionLevel()

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

inline

Returns the current assumption level. Note that if a solve was done since the last SetAssumptionLevel(), then the returned level may be lower than the one that was set. This is because some assumptions may now be consequences of others before them due to the newly learned clauses.

Definition at line 228 of file sat_solver.h.

◆ Backtrack()

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

Restores the state to the given target decision level. The decision at that level and all its propagation will not be undone. But all the trail after this will be cleared. Calling this with 0 will revert all the decisions and only the fixed variables will be left on the trail.

Todo: (user): The backtrack method should not be called when the model is unsat. Add a DCHECK to prevent that, but before fix the bop::BopOptimizerBase architecture.

Do nothing if the CurrentDecisionLevel() is already correct. This is needed, otherwise target_trail_index below will remain at zero and that will cause some problems. Note that we could forbid a user to call Backtrack() with the current level, but that is annoying when you just want to reset the solver with Backtrack(0).

Any backtrack to the root from a positive one is counted as a restart.

Per the SatPropagator interface, this is needed before calling Untrail.

Definition at line 1032 of file sat_solver.cc.

◆ ClearNewlyAddedBinaryClauses()

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

Definition at line 1084 of file sat_solver.cc.

◆ counters()

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

inline

Definition at line 429 of file sat_solver.h.

◆ CurrentDecisionLevel()

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

inline

Definition at line 386 of file sat_solver.h.

◆ Decisions()

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

inline

Note: the Decisions() vector is always of size NumVariables(), and that only the first CurrentDecisionLevel() entries have a meaning.

Definition at line 385 of file sat_solver.h.

◆ deterministic_time()

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

A deterministic number that should be correlated with the time spent in the Solve() function. The order of magnitude should be close to the time in seconds.

Each of these counters mesure really basic operations. The weight are just an estimate of the operation complexity. Note that these counters are never reset to zero once a SatSolver is created.

Todo: (user): Find a better procedure to fix the weight than just educated guess.

Here there is a factor 2 because of the untrail.

Definition at line 115 of file sat_solver.cc.

◆ EnqueueDecisionAndBackjumpOnConflict()

int operations_research::sat::SatSolver::EnqueueDecisionAndBackjumpOnConflict ( Literal true_literal )

Advanced usage. The next 3 functions allow to drive the search from outside the solver. Takes a new decision (the given true_literal must be unassigned) and propagates it. Returns the trail index of the first newly propagated literal. If there is a conflict and the problem is detected to be UNSAT, returns kUnsatTrailIndex.

Important: In the presence of assumptions, this also returns kUnsatTrailIndex on ASSUMPTION_UNSAT. One can know the difference with IsModelUnsat().

A client can determine if there is a conflict by checking if the CurrentDecisionLevel() was increased by 1 or not.

If there is a conflict, the given decision is not applied and:

The conflict is learned.
The decisions are potentially backtracked to the first decision that propagates more variables because of the newly learned conflict.
The returned value is equal to trail_->Index() after this backtracking and just before the new propagation (due to the conflict) which is also performed by this function.

We should never enqueue before the assumptions_.

Definition at line 557 of file sat_solver.cc.

◆ EnqueueDecisionAndBacktrackOnConflict()

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

This function starts by calling EnqueueDecisionAndBackjumpOnConflict(). If there is no conflict, it stops there. Otherwise, it tries to reapply all the decisions that were backjumped over until the first one that can't be taken because it is incompatible. Note that during this process, more conflicts may happen and the trail may be backtracked even further.

In any case, the new decisions stack will be the largest valid "prefix" of the old stack. Note that decisions that are now consequence of the ones before them will no longer be decisions.

Returns INFEASIBLE if the model was proven infeasible, ASSUMPTION_UNSAT if the current decision and the one we are trying to take are not compatible together and FEASIBLE if all decisions are taken.

Note(user): This function can be called with an already assigned literal.

Definition at line 1003 of file sat_solver.cc.

◆ EnqueueDecisionIfNotConflicting()

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

Tries to enqueue the given decision and performs the propagation. Returns true if no conflict occurred. Otherwise, returns false and restores the solver to the state just before this was called.

Note(user): With this function, the solver doesn't learn anything.

Definition at line 1017 of file sat_solver.cc.

◆ ExtractClauses()

template<typename Output >

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

inline

Extract the current problem clauses. The Output type must support the two functions:

void AddBinaryClause(Literal a, Literal b);
void AddClause(absl::Span<const Literal> clause);

Todo: (user): also copy the removable clauses?

It is important to process the newly fixed variables, so they are not present in the clauses we export.

Note(user): Putting the binary clauses first help because the presolver currently process the clauses in order.

Definition at line 346 of file sat_solver.h.

◆ FinishPropagation()

bool operations_research::sat::SatSolver::FinishPropagation ( )

Advanced usage. Finish the progation if it was interrupted. Note that this might run into conflict and will propagate again until a fixed point is reached or the model was proven UNSAT. Returns IsModelUnsat().

Todo: (user): Exiting like this might cause issue since the propagation is not "finished" but some code might assume it is. However since we already might repropagate in the LP constraint, most of the code should support "not finished propagation".

Definition at line 582 of file sat_solver.cc.

◆ GetLastIncompatibleDecisions()

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

This can be called just after SolveWithAssumptions() returned ASSUMPTION_UNSAT or after EnqueueDecisionAndBacktrackOnConflict() leaded to a conflict. It returns a subsequence (in the correct order) of the previously enqueued decisions that cannot be taken together without making the problem UNSAT.

literal at true in the conflict must be decision/assumptions that could not be taken.

We just expand the conflict until we only have decisions.

Find next marked literal to expand from the trail.

Marks all the literals of its reason.

We reverse the assumptions so they are in the same order as the one in which the decision were made.

Definition at line 1506 of file sat_solver.cc.

◆ IsModelUnsat()

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

inline

Todo: (user): remove this function.

Definition at line 150 of file sat_solver.h.

◆ LiteralTrail()

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

inline

Definition at line 387 of file sat_solver.h.

◆ LoadDebugSolution()

void operations_research::sat::SatSolver::LoadDebugSolution ( const std::vector< Literal > & solution )

We should only call this with complete solution.

Definition at line 488 of file sat_solver.cc.

◆ MinimizeByPropagation()

bool operations_research::sat::SatSolver::MinimizeByPropagation ( double dtime )

Tricky: we don't want TryToMinimizeClause() to delete to_minimize while we are processing it.

Note(user): In some corner cases, the function above might find a feasible assignment. I think it is okay to ignore this special case that should only happen on trivial problems and just reset the solver.

Definition at line 1468 of file sat_solver.cc.

◆ model()

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

inline

Todo: (user): Remove. This is temporary for accessing the model deep within some old code that didn't use the Model object.

Definition at line 76 of file sat_solver.h.

◆ ModelIsUnsat()

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

inline

Returns true if the model is UNSAT. Note that currently the status is "sticky" and once this happen, nothing else can be done with the solver.

Thanks to this function, a client can safely ignore the return value of any Add*() functions. If one of them return false, then ModelIsUnsat() will return true.

Definition at line 147 of file sat_solver.h.

◆ mutable_logger()

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

inline

Hack to allow to temporarily disable logging if it is enabled.

Definition at line 492 of file sat_solver.h.

◆ NewBooleanVariable()

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

inline

We need to be able to encode the variable as a literal.

Definition at line 94 of file sat_solver.h.

◆ NewlyAddedBinaryClauses()

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

Definition at line 1080 of file sat_solver.cc.

◆ NotifyThatModelIsUnsat()

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

inline

This function is here to deal with the case where a SAT/CP model is found to be trivially UNSAT while the user is constructing the model. Instead of having to test the status of all the lines adding a constraint, one can just check if the solver is not UNSAT once the model is constructed. Note that we usually log a warning on the first constraint that caused a "trival" unsatisfiability.

Definition at line 456 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_branches()

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

Some statistics since the creation of the solver.

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

Note: we count the number of backtrack to level zero from a positive level. Those can corresponds to actual restarts, or conflicts that learn unit clauses or any other reason that trigger such backtrack.

Definition at line 113 of file sat_solver.cc.

◆ NumFixedVariables()

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

inline

Definition at line 485 of file sat_solver.h.

◆ NumVariables()

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

inline

Definition at line 93 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 133 of file sat_solver.cc.

◆ ProcessCurrentConflict()

void operations_research::sat::SatSolver::ProcessCurrentConflict ( )

Processes the current conflict from trail->FailingClause().

This learns the conflict, backtracks, enqueues the consequence of the learned conflict and return. When handling assumptions, this might return false without backtracking in case of ASSUMPTIONS_UNSAT. This is only exposed to allow processing a conflict detected outside normal propagation.

A conflict occurred, compute a nice reason for this failure.

If the failing clause only contains literal at the assumptions level, we cannot use the ComputeFirstUIPConflict() code as we might have more than one decision.

Todo: (user): We might still want to "learn" the clause, especially if it reduces to only one literal in which case we can just fix it.

An empty conflict means that the problem is UNSAT.

Update the activity of all the variables in the first UIP clause. Also update the activity of the last level variables expanded (and thus discarded) during the first UIP computation. Note that both sets are disjoint.

Bump the clause activities.

Note: the activity of the learned clause will be bumped too by AddLearnedClauseAndEnqueueUnitPropagation().

Decay the activities.

Hack from Glucose that seems to perform well.

PB resolution. There is no point using this if the conflict and all the reasons involved in its resolution were clauses.

Todo: (user): Note that we use the clause above to update the variable activities and not the pb conflict. Experiment.

Generic clause case.

We have a pseudo-Boolean conflict, so we start from there.

Convert the conflict into the vector<LiteralWithCoeff> form.

Check if the learned PB conflict is just a clause: all its coefficient must be 1, and the rhs must be its size minus 1.

Use the PB conflict.

Continue with the normal clause flow, but use the PB conflict clause if it has a lower backjump level.

The minimization functions below expect the conflict to be marked!

Todo: (user): This is error prone, find a better way?

Minimizing the conflict with binary clauses first has two advantages. First, there is no need to compute a reason for the variables eliminated this way. Second, more variables may be marked (in is_marked_) and MinimizeConflict() can take advantage of that. Because of this, the LBD of the learned conflict can change.

Minimize the learned conflict.

Minimize it further with binary clauses?

Note: on the contrary to the MinimizeConflict() above that just uses the reason graph, this minimization can change the clause LBD and even the backtracking level.

We notify the decision before backtracking so that we can save the phase. The current heuristic is to try to take a trail prefix for which there is currently no conflict (hence just before the last decision was taken).

Todo: (user): It is unclear what the best heuristic is here. Both the current trail index or the trail before the current decision perform well, but using the full trail seems slightly better even though it will contain the current conflicting literal.

Backtrack and add the reason to the set of learned clause.

Note: we need to output the learned clause before cleaning the clause database. This is because we already backtracked and some of the clauses that were needed to infer the conflict may not be "reasons" anymore and may be deleted.

Because we might change the conflict with this minimization algorithm, we cannot just subsume clauses with it blindly.

Todo: (user): Either remove that algorithm or support subsumption by just checking if it is okay to do so, or doing it on the fly while computing the first UIP.

Detach any subsumed clause. They will actually be deleted on the next clause cleanup phase.

Create and attach the new learned clause.

Definition at line 686 of file sat_solver.cc.

◆ ProcessNewlyFixedVariables()

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

Simplifies the problem when new variables are assigned at level 0.

We remove the clauses that are always true and the fixed literals from the others. Note that none of the clause should be all false because we should have detected a conflict before this is called.

The clause is always true, detach it.

This clause is now a binary clause, treat it separately. Note that it is safe to do that because this clause can't be used as a reason since we are at level zero and the clause is not satisfied.

Note: we will only delete the clauses during the next database cleanup.

We also clean the binary implication graph. Tricky: If we added the first binary clauses above, the binary graph is not in "propagated" state as it should be, so we call Propagate() so all the checks are happy.

Definition at line 1790 of file sat_solver.cc.

◆ Propagate()

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

Performs propagation of the recently enqueued elements. Mainly visible for testing.

Todo: (user): Support propagating only the "first" propagators. That can be useful for probing/in-processing, so we can control if we do only the SAT part or the full integer part...

Because we might potentially iterate often on this list below, we remove empty propagators.

Todo: (user): This might not really be needed.

The idea here is to abort the inspection as soon as at least one propagation occurs so we can loop over and test again the highest priority constraint types using the new information.

Note: the first propagators_ should be the binary_implication_graph_ and that its Propagate() functions will not abort on the first propagation to be slightly more efficient.

In some corner cases, we might add new constraint during propagation, which might trigger new propagator addition or some propagator to become non-empty() now.

Definition at line 1861 of file sat_solver.cc.

◆ ReapplyAssumptionsIfNeeded()

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

Advanced usage. If the decision level is smaller than the assumption level, this will try to reapply all assumptions. Returns true if this was doable, otherwise returns false in which case the model is either UNSAT or ASSUMPTION_UNSAT.

Note: we do not count these as "branches" for a reporting purpose.

When assumptions_ is not empty, the first "decision" actually contains multiple one, and we should never use its literal.

We enqueue all assumptions at once at decision level 1.

See GetLastIncompatibleDecisions().

This is needed to avoid an empty level that cause some CHECK fail.

Corner case: all assumptions are fixed at level zero, we ignore them.

Now that everything is enqueued, we propagate.

Definition at line 635 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 )

Simple interface to solve a problem under the given assumptions. This simply ask the solver to solve a problem given a set of variables fixed to a given value (the assumptions). Compared to simply calling AddUnitClause() and fixing the variables once and for all, this allow to backtrack over the assumptions and thus exploit the incrementally between subsequent solves.

This function backtrack over all the current decision, tries to enqueue the given assumptions, sets the assumption level accordingly and finally calls Solve().

If, given these assumptions, the model is UNSAT, this returns the ASSUMPTIONS_UNSAT status. INFEASIBLE is reserved for the case where the model is proven to be unsat without any assumptions.

If ASSUMPTIONS_UNSAT is returned, it is possible to get a "core" of unsat assumptions by calling GetLastIncompatibleDecisions().

Definition at line 1095 of file sat_solver.cc.

◆ ResetDecisionHeuristic()

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

inline

Definition at line 170 of file sat_solver.h.

◆ ResetToLevelZero()

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

Like Backtrack(0) but make sure the propagation is finished and return false if unsat was detected. This also removes any assumptions level.

Definition at line 610 of file sat_solver.cc.

◆ ResetWithGivenAssumptions()

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

Changes the assumptions level and the current solver assumptions. Returns false if the model is UNSAT or ASSUMPTION_UNSAT, true otherwise.

This uses the "new" assumptions handling, where all assumptions are enqueued at once at decision level 1 before we start to propagate. This has many advantages. In particular, because we propagate with the binary implications first, if we ever have assumption => not(other_assumptions) we are guaranteed to find it and returns a core of size 2.

Paper: "Speeding Up Assumption-Based SAT", Randy Hickey and Fahiem Bacchus http://www.maxhs.org/docs/Hickey-Bacchus2019_Chapter_SpeedingUpAssumption-BasedSAT.pdf

For assumptions and core-based search, it is really important to add as many binary clauses as possible. This is because we do not wan to miss any early core of size 2.

Definition at line 618 of file sat_solver.cc.

◆ RestoreSolverToAssumptionLevel()

bool operations_research::sat::SatSolver::RestoreSolverToAssumptionLevel ( )

Advanced usage. This is meant to restore the solver to a "proper" state after a solve was interrupted due to a limit reached.

Without assumption (i.e. if AssumptionLevel() is 0), this will revert all decisions and make sure that all the fixed literals are propagated. In presence of assumptions, this will either backtrack to the assumption level or re-enqueue any assumptions that may have been backtracked over due to conflits resolution. In both cases, the propagation is finished.

Note: this may prove the model to be UNSAT or ASSUMPTION_UNSAT in which case it will return false.

Definition at line 572 of file sat_solver.cc.

◆ SaveDebugAssignment()

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

Only used for debugging. Save the current assignment in debug_assignment_. The idea is that if we know that a given assignment is satisfiable, then all the learned clauses or PB constraints must be satisfiable by it. In debug mode, and after this is called, all the learned clauses are tested to satisfy this saved assignment.

Definition at line 480 of file sat_solver.cc.

◆ SetAssignmentPreference()

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

inline

Wrapper around the same functions in SatDecisionPolicy.

Todo: (user): Clean this up by making clients directly talk to SatDecisionPolicy.

Definition at line 164 of file sat_solver.h.

◆ SetAssumptionLevel()

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

Changes the assumption level. All the decisions below this level will be treated as assumptions by the next Solve(). Note that this may impact some heuristics, like the LBD value of a clause.

New assumption code.

Definition at line 1111 of file sat_solver.cc.

◆ SetDratProofHandler()

void operations_research::sat::SatSolver::SetDratProofHandler ( DratProofHandler * drat_proof_handler )

inline

Definition at line 444 of file sat_solver.h.

◆ SetNumVariables()

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

Increases the number of variables of the current problem.

Todo: (user): Rename to IncreaseNumVariablesTo() until we support removing variables...

The +1 is a bit tricky, it is because in EnqueueDecisionAndBacktrackOnConflict() we artificially enqueue the decision before checking if it is not already assigned.

Definition at line 85 of file sat_solver.cc.

◆ SetParameters()

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

Parameters management. Note that calling SetParameters() will reset the value of many heuristics. For instance:

The restart strategy will be reinitialized.
The random seed and random generator will be reset to the value given in parameters.
The global TimeLimit singleton will be reset and time will be counted from this call.

Definition at line 138 of file sat_solver.cc.

◆ Solve()

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

Definition at line 1128 of file sat_solver.cc.

◆ SolveWithTimeLimit()

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

Same as Solve(), but with a given time limit. Note that this will not update the TimeLimit singleton, but only the passed object instead.

Definition at line 1123 of file sat_solver.cc.

◆ TakePropagatorOwnership()

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

inline

Definition at line 156 of file sat_solver.h.

◆ TrackBinaryClauses()

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

inline

Functions to manage the set of learned binary clauses. Only clauses added/learned when TrackBinaryClause() is true are managed.

Definition at line 371 of file sat_solver.h.

◆ UnsatStatus()

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

inline

Helper functions to get the correct status when one of the functions above returns false.

Definition at line 335 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

Classes

Public Types

Public Member Functions

Detailed Description

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

◆ AddProblemClause()

◆ AddPropagator()

◆ AddTernaryClause()

◆ AddUnitClause()

◆ AdvanceDeterministicTime()

◆ AllPreferences()

◆ Assignment()

◆ AssumptionLevel()

◆ Backtrack()

◆ ClearNewlyAddedBinaryClauses()

◆ counters()

◆ CurrentDecisionLevel()

◆ Decisions()

◆ deterministic_time()

◆ EnqueueDecisionAndBackjumpOnConflict()

◆ EnqueueDecisionAndBacktrackOnConflict()

◆ EnqueueDecisionIfNotConflicting()

◆ ExtractClauses()

◆ FinishPropagation()

◆ GetLastIncompatibleDecisions()

◆ IsModelUnsat()

◆ LiteralTrail()

◆ LoadDebugSolution()

◆ MinimizeByPropagation()

◆ model()

◆ ModelIsUnsat()

◆ mutable_logger()

◆ NewBooleanVariable()

◆ NewlyAddedBinaryClauses()

◆ NotifyThatModelIsUnsat()

◆ num_backtracks()

◆ num_branches()

◆ num_failures()

◆ num_propagations()

◆ num_restarts()

◆ NumFixedVariables()

◆ NumVariables()

◆ operator=()

◆ parameters()

◆ ProcessCurrentConflict()

◆ ProcessNewlyFixedVariables()

◆ Propagate()

◆ ReapplyAssumptionsIfNeeded()

◆ ResetAndSolveWithGivenAssumptions()

◆ ResetDecisionHeuristic()

◆ ResetToLevelZero()

◆ ResetWithGivenAssumptions()

◆ RestoreSolverToAssumptionLevel()

◆ SaveDebugAssignment()

◆ SetAssignmentPreference()

◆ SetAssumptionLevel()

◆ SetDratProofHandler()

◆ SetNumVariables()

◆ SetParameters()

◆ Solve()

◆ SolveWithTimeLimit()

◆ TakePropagatorOwnership()

◆ TrackBinaryClauses()

◆ UnsatStatus()