An helper class to share the code used by the different kind of search. More...

#include <integer_search.h>

Public Member Functions
	IntegerSearchHelper (Model *model)

bool	BeforeTakingDecision ()

bool	GetDecision (const std::function< BooleanOrIntegerLiteral()> &f, LiteralIndex *decision)

LiteralIndex	GetDecisionLiteral (const BooleanOrIntegerLiteral &decision)

void	NotifyThatConflictWasFoundDuringGetDecision ()

bool	TakeDecision (Literal decision)

SatSolver::Status	SolveIntegerProblem ()

Detailed Description

An helper class to share the code used by the different kind of search.

Definition at line 270 of file integer_search.h.

Constructor & Destructor Documentation

◆ IntegerSearchHelper()

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

explicit

Definition at line 1320 of file integer_search.cc.

Member Function Documentation

◆ BeforeTakingDecision()

bool operations_research::sat::IntegerSearchHelper::BeforeTakingDecision ( )

Executes some code before a new decision. Returns false if model is UNSAT.

If we pushed root level deductions, we restart to incorporate them.

Note: in the present of assumptions, it is important to return to the level zero first ! otherwise, the new deductions will not be incorporated and the solver will loop forever.

The rest only trigger at level zero.

Definition at line 1333 of file integer_search.cc.

◆ GetDecision()

bool operations_research::sat::IntegerSearchHelper::GetDecision	(	const std::function< BooleanOrIntegerLiteral()> &	f,
		LiteralIndex *	decision )

Calls the decision heuristics and extract a non-fixed literal.

Note: we do not want to copy the function here.

Returns false if a conflict was found while trying to take a decision.

Definition at line 1387 of file integer_search.cc.

◆ GetDecisionLiteral()

LiteralIndex operations_research::sat::IntegerSearchHelper::GetDecisionLiteral ( const BooleanOrIntegerLiteral & decision )

Inner function used by GetDecision(). It will create a new associated literal if needed.

Convert integer decision to literal one if needed.

Todo: (user): Ideally it would be cool to delay the creation even more until we have a conflict with these decisions, but it is currently hard to do so.

Todo: (user): It would be nicer if this can never happen. For now, it does because of the Propagate() not reaching the fixed point as mentioned in a

Todo

Todo: above. As a work-around, we display a message but do not crash and recall the decision heuristic.

Definition at line 1362 of file integer_search.cc.

◆ NotifyThatConflictWasFoundDuringGetDecision()

void operations_research::sat::IntegerSearchHelper::NotifyThatConflictWasFoundDuringGetDecision ( )

inline

Functions passed to GetDecision() might call this to notify a conflict was detected.

Definition at line 291 of file integer_search.h.

◆ SolveIntegerProblem()

SatSolver::Status operations_research::sat::IntegerSearchHelper::SolveIntegerProblem ( )

Tries to find a feasible solution to the current model.

This function continues from the current state of the solver and loop until all variables are instantiated (i.e. the next decision is kNoLiteralIndex) or a search limit is reached. It uses the heuristic from the SearchHeuristics class in the model to decide when to restart and what next decision to take.

Each time a restart happen, this increment the policy index modulo the number of heuristics to act as a portfolio search.

Note: it is important to do the level-zero propagation if it wasn't already done because EnqueueDecisionAndBackjumpOnConflict() assumes that the solver is in a "propagated" state.

Todo: (user): We have the issue that at level zero. calling the propagation loop more than once can propagate more! This is because we call the LP again and again on each level zero propagation. This is causing some CHECKs() to fail in multithread (rarely) because when we associate new literals to integer ones, Propagate() is indirectly called. Not sure yet how to fix.

Main search loop.

If needed, restart and switch decision_policy.

Note: to properly count the num_times, we do not want to move this function, but actually call that copy.

No decision means that we reached a leave of the search tree and that we have a feasible solution.

Tricky: If the time limit is reached during the final propagation when all variables are fixed, there is no guarantee that the propagation responsible for testing the validity of the solution was run to completion. So we cannot report a feasible solution.

Save the current polarity of all Booleans in the solution. It will be followed for the next SAT decisions. This is known to be a good policy for optimization problem. Note that for decision problem we don't care since we are just done as soon as a solution is found.

This idea is kind of "well known", see for instance the "LinSBPS" submission to the maxSAT 2018 competition by Emir Demirovic and Peter Stuckey where they show it is a good idea and provide more references.

In multi-thread, we really only want to save the LP relaxation for thread with high linearization level to avoid to pollute the repository with sub-par lp solutions.

Todo: (user): Experiment more around dynamically changing the threshold for storing LP solutions in the pool. Alternatively expose this as parameter so this can be tuned later.

Todo: (user): Avoid adding the same solution many time if the LP didn't change. Avoid adding solution that are too deep in the tree (most variable fixed). Also use a callback rather than having this here, we don't want this file to depend on cp_model.proto.

Note: We can actually record LP solutions more frequently. However this process is time consuming and workers waste a lot of time doing this. To avoid this we don't record solutions after each decision.

Definition at line 1450 of file integer_search.cc.

◆ TakeDecision()

bool operations_research::sat::IntegerSearchHelper::TakeDecision ( Literal decision )

Tries to take the current decision, this might backjump. Returns false if the model is UNSAT.

Note: kUnsatTrailIndex might also mean ASSUMPTIONS_UNSAT.

Todo: (user): on some problems, this function can be quite long. Expand so that we can check the time limit at each step?

Update the implied bounds each time we enqueue a literal at level zero. This is "almost free", so we might as well do it.

Update the pseudo costs.

Definition at line 1424 of file integer_search.cc.

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

ortools/sat/integer_search.h
ortools/sat/integer_search.cc

Public Member Functions