operations_research::sat::Inprocessing Class Reference

#include <sat_inprocessing.h>

Public Member Functions
	Inprocessing (Model *model)
bool	PresolveLoop (SatPresolveOptions options)
bool	InprocessingRound ()
bool	LevelZeroPropagate ()
bool	DetectEquivalencesAndStamp (bool use_transitive_reduction, bool log_info)
bool	RemoveFixedAndEquivalentVariables (bool log_info)
bool	MoreFixedVariableToClean () const
bool	MoreRedundantVariableToClean () const
bool	SubsumeAndStrenghtenRound (bool log_info)
void	ProvideLogger (SolverLogger *logger)
	A bit hacky. Only needed during refactoring.

Detailed Description

We need to keep some information from one call to the next, so we use a class. Note that as this becomes big, we can probably split it.

Todo

(user): Some algorithms here use the normal SAT propagation engine. However we might want to temporarily disable activities/phase saving and so on if we want to run them as in-processing steps so that they do not "pollute" the normal SAT search.

Todo

(user): For the propagation, this depends on the SatSolver class, which mean we cannot really use it without some refactoring as an in-processing from the SatSolver::Solve() function. So we do need a special InprocessingSolve() that lives outside SatSolver. Alternatively, we can extract the propagation main loop and conflict analysis from SatSolver.

Definition at line 97 of file sat_inprocessing.h.

Constructor & Destructor Documentation

Inprocessing()

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

inlineexplicit

Definition at line 99 of file sat_inprocessing.h.

Member Function Documentation

DetectEquivalencesAndStamp()

bool operations_research::sat::Inprocessing::DetectEquivalencesAndStamp	(	bool	use_transitive_reduction,
		bool	log_info )

Detects equivalences in the implication graph and propagates any failed literal found during the process.

It make sense to do the pre-stamping right after the equivalence detection since it needs a DAG and can detect extra failed literal.

Todo

(user): consider doing the transitive reduction after each SCC. It might be slow but we could try to make it more incremental to compensate and it should allow further reduction.

Definition at line 314 of file sat_inprocessing.cc.

InprocessingRound()

bool operations_research::sat::Inprocessing::InprocessingRound

(

)

When the option use_sat_inprocessing is true, then this is called at each restart. It is up to the heuristics here to decide what inprocessing we do or if we wait for the next call before doing anything.

Mainly useful for development.

Store the dtime of the first call (first restart) and wait for the next restart.

Try to spend a given ratio of time in the inprocessing.

Todo

(user): Tune the heuristic, in particular, with the current code we start some inprocessing before the first search.

LP Propagation during inprocessing can be really slow, so we temporarily disable it.

Todo

(user): The LP and incremental structure will still be called though, which can take some time, try to disable it more cleanly.

We make sure we do not "pollute" the current saved polarities. We will restore them at the end.

Todo

(user): We should probably also disable the variable/clauses activity updates.

Probing.

Todo

(user): Add a small wrapper function to time this.

Todo

(user): try to enable these? The problem is that we can only remove variables not used the non-pure SAT part of a model.

Definition at line 172 of file sat_inprocessing.cc.

LevelZeroPropagate()

bool operations_research::sat::Inprocessing::LevelZeroPropagate

(

)

Simple wrapper that makes sure all the clauses are attached before a propagation is performed.

Definition at line 306 of file sat_inprocessing.cc.

MoreFixedVariableToClean()

bool operations_research::sat::Inprocessing::MoreFixedVariableToClean

(

)

const

Returns true if there is new fixed variables or new equivalence relations since RemoveFixedAndEquivalentVariables() was last called.

Definition at line 295 of file sat_inprocessing.cc.

MoreRedundantVariableToClean()

bool operations_research::sat::Inprocessing::MoreRedundantVariableToClean

(

)

const

Definition at line 300 of file sat_inprocessing.cc.

PresolveLoop()

bool operations_research::sat::Inprocessing::PresolveLoop

(

SatPresolveOptions

options

)

Does some simplifications until a fix point is reached or the given deterministic time is passed.

Mainly useful for development.

We currently do the transformations in a given order and restart each time we did something to make sure that the earlier step cannot strengthen more. This might not be the best, but it is really good during development phase to make sure each individual functions is as incremental and as fast as possible.

This one is fast since only newly fixed variables are considered.

This also prepare the stamping below so that we do that on a DAG and do not consider potential new implications added by RemoveFixedAndEquivalentVariables().

Todo

(user): This should/could be integrated with the stamping since it seems better to do just one loop instead of two over all clauses. Because of memory access. it isn't that clear though.

IMPORTANT: Since we only run this on pure sat problem, we can just get rid of equivalent variable right away and do not need to keep them in the implication_graph_ for propagation.

This is needed for the correctness of the bounded variable elimination.

We wait for the fix-point to be reached before doing the other simplifications below.

Todo

(user): Combine the two? this way we don't create a full literal <-> clause graph twice. It might make sense to reach the BCE fix point which is unique before each variable elimination.

Todo

(user): this break some binary graph invariant. Fix!

Probing.

Todo

(user): Maintain the total number of literals in the watched clauses.

Definition at line 67 of file sat_inprocessing.cc.

ProvideLogger()

void operations_research::sat::Inprocessing::ProvideLogger ( SolverLogger * logger )

inline

A bit hacky. Only needed during refactoring.

Definition at line 150 of file sat_inprocessing.h.

RemoveFixedAndEquivalentVariables()

bool operations_research::sat::Inprocessing::RemoveFixedAndEquivalentVariables

(

bool

log_info

)

Removes fixed variables and exploit equivalence relations to cleanup the clauses. Returns false if UNSAT.

Preconditions.

Todo

(user): The level zero is required because we remove fixed variables but if we split this into two functions, we could rewrite clause at any level.

Test if some work is needed.

Todo

(user): If only new fixed variables are there, we can use a faster function. We should also merge the code with the deletion code in sat_solver_.cc, but that require some refactoring of the dependence between files.

Start the round.

We need this temporary vector for the DRAT proof settings, otherwise we could just have done an in-place transformation.

Used to mark clause literals.

We first do a loop to see if there is anything to do.

Todo

(user): we should output literal to the proof right away, currently if we remove clauses before fixing literal the proof is wrong.

Rewrite the clause.

Restore marked.

Todo

(user): find a way to auto-tune that after a run on borg...

Definition at line 336 of file sat_inprocessing.cc.

SubsumeAndStrenghtenRound()

bool operations_research::sat::Inprocessing::SubsumeAndStrenghtenRound

(

bool

log_info

)

Processes all clauses and see if there is any subsumption/strenghtening reductions that can be performed. Returns false if UNSAT.

Todo

(user): Use better work limits, see SAT09.CRAFTED.ramseycube.Q3inK12

Todo

(user): Be more incremental, each time a clause is added/reduced track which literal are impacted? Also try to do orthogonal reductions from one round to the next.

We need this temporary vector for the DRAT proof settings, otherwise we could just have done an in-place transformation.

This function needs the watcher to be detached as we might remove some of the watched literals.

Todo

(user): We could do that only if we do some reduction, but this is quite fast though.

Process clause by increasing sizes.

Todo

(user): probably faster without the size indirection.

Used to mark clause literals.

Clause index in clauses.

Todo

(user): Storing signatures here might be faster?

Clause signatures in the same order as clauses.

Todo

(user): Better abort limit. We could also limit the watcher sizes and never look at really long clauses. Note that for an easier incrementality, it is better to reach some kind of completion so we know what new stuff need to be done.

Check for subsumption, note that this currently ignore all clauses in the binary implication graphs. Stamping is doing some of that (and some also happen during probing), but we could consider only direct implications here and be a bit more exhaustive than what stamping do with them (at least for node with many incoming and outgoing implications).

Todo

(user): Do some reduction using binary clauses. Note that only clause that never propagated since last round need to be checked for binary subsumption.

Compute hash and mark literals.

Look for clause that subsumes this one. Note that because we inspect all one watcher lists for the literals of this clause, if a clause is included inside this one, it must appear in one of these lists.

For strengthenning we also need to check the negative watcher lists.

Any literal here can be removed, but afterwards the other might not. For now we just remove the first one.

Todo

(user): remove first and see if other still removable. Alternatively use a "removed" marker and redo a check for each clause that simplifies this one? Or just remove the first one, and wait for next round.

Recompute signature.

Register one literal to watch. Any literal works, but we choose the smallest list.

Todo

(user): No need to add this clause if we know it cannot subsume any new clause since last round. i.e. unchanged clause that do not contains any literals of newly added clause do not need to be added here. We can track two bitset in LiteralWatchers via a register mechanism:

• literal of newly watched clauses since last clear.
• literal of reduced clauses since last clear.

Important: we can only use this clause to subsume/strenghten others if it cannot be deleted later.

Todo

(user): We could/should sort the literal in this clause by using literals that appear in a small number of clauses first so that we maximize the chance of early abort in the critical loops above.

Todo

(user): We could also move the watched literal first so we always skip it.

We might have fixed variables, finish the propagation.

Todo

(user): tune the deterministic time.

Definition at line 445 of file sat_inprocessing.cc.

---

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

• ortools/sat/sat_inprocessing.h
• ortools/sat/sat_inprocessing.cc