operations_research::sat::ProbingOptions Struct Reference

#include <probing.h>

Public Member Functions
std::string	ToString () const

Public Attributes
double	deterministic_limit = 1.0
bool	extract_binary_clauses = false
bool	use_tree_look = true
bool	use_queue = true
bool	subsume_with_binary_clause = true
bool	log_info = false
	We assume this is also true if –v 1 is activated.

Detailed Description

Options for the FailedLiteralProbing() code below.

A good reference for the algorithms involved here is the paper "Revisiting Hyper Binary Resolution" Marijn J. H. Heule, Matti Jarvisalo, Armin Biere, http://www.cs.utexas.edu/~marijn/cpaior2013.pdf

Definition at line 164 of file probing.h.

Member Function Documentation

ToString()

std::string operations_research::sat::ProbingOptions::ToString ( ) const

inline

Definition at line 229 of file probing.h.

Member Data Documentation

deterministic_limit

double operations_research::sat::ProbingOptions::deterministic_limit = 1.0

The probing will consume all this deterministic time or stop if nothing else can be deduced and everything has been probed until fix-point. The fix point depend on the extract_binay_clauses option:

• If false, we will just stop when no more failed literal can be found.

• If true, we will do more work and stop when all failed literal have been found and all hyper binary resolution have been performed.

  Todo

  (user): We can also provide a middle ground and probe all failed literal but do not extract all binary clauses.

Note

the fix-point is unique, modulo the equivalent literal detection we do. And if we add binary clauses, modulo the transitive reduction of the binary implication graph.

To be fast, we only use the binary clauses in the binary implication graph for the equivalence detection. So the power of the equivalence detection changes if the extract_binay_clauses option is true or not.

Todo

(user): The fix point is not yet reached since we don't currently simplify non-binary clauses with these equivalence, but we will.

Definition at line 185 of file probing.h.

extract_binary_clauses

bool operations_research::sat::ProbingOptions::extract_binary_clauses = false

This is also called hyper binary resolution. Basically, we make sure that the binary implication graph is augmented with all the implication of the form a => b that can be derived by fixing 'a' at level zero and doing a propagation using all constraints. Note that we only add clauses that cannot be derived by the current implication graph.

With these extra clause the power of the equivalence literal detection using only the binary implication graph with increase. Note that it is possible to do exactly the same thing without adding these binary clause first. This is what is done by yet another probing algorithm (currently in simplification.cc).

Todo

(user): Note that adding binary clause before/during the SAT presolve is currently not always a good idea. This is because we don't simplify the other clause as much as we could. Also, there can be up to a quadratic number of clauses added this way, which might slow down things a lot. But then because of the deterministic limit, we usually cannot add too much clauses, even for huge problems, since we will reach the limit before that.

Definition at line 205 of file probing.h.

log_info

bool operations_research::sat::ProbingOptions::log_info = false

We assume this is also true if –v 1 is activated.

Definition at line 227 of file probing.h.

subsume_with_binary_clause

bool operations_research::sat::ProbingOptions::subsume_with_binary_clause = true

If we detect as we probe that a new binary clause subsumes one of the non-binary clause, we will replace the long clause by the binary one. This is orthogonal to the extract_binary_clauses parameters which will add all binary clauses but not necessarily check for subsumption.

Definition at line 224 of file probing.h.

use_queue

bool operations_research::sat::ProbingOptions::use_queue = true

There is two slightly different implementation of the tree-look algo.

Todo

(user): Decide which one is better, currently the difference seems small but the queue seems slightly faster.

Definition at line 218 of file probing.h.

use_tree_look

bool operations_research::sat::ProbingOptions::use_tree_look = true

Use a version of the "Tree look" algorithm as explained in the paper above. This is usually faster and more efficient. Note that when extracting binary clauses it might currently produce more "redundant" one in the sense that a transitive reduction of the binary implication graph after all hyper binary resolution have been performed may need to do more work.

Definition at line 212 of file probing.h.

---

The documentation for this struct was generated from the following file:

• ortools/sat/probing.h