operations_research::sat::SatPresolveOptions Struct Reference

#include <sat_inprocessing.h>

Public Attributes
double	deterministic_time_limit = 30.0
	The time budget to spend.
bool	log_info = false
bool	extract_binary_clauses_in_probing = false
	See ProbingOptions in probing.h.
bool	use_transitive_reduction = false

Detailed Description

Definition at line 64 of file sat_inprocessing.h.

Member Data Documentation

deterministic_time_limit

double operations_research::sat::SatPresolveOptions::deterministic_time_limit = 30.0

The time budget to spend.

Definition at line 66 of file sat_inprocessing.h.

extract_binary_clauses_in_probing

bool operations_research::sat::SatPresolveOptions::extract_binary_clauses_in_probing = false

See ProbingOptions in probing.h.

Definition at line 73 of file sat_inprocessing.h.

log_info

bool operations_research::sat::SatPresolveOptions::log_info = false

We assume this is also true if –v 1 is activated and we actually log even more in –v 1.

Definition at line 70 of file sat_inprocessing.h.

use_transitive_reduction

bool operations_research::sat::SatPresolveOptions::use_transitive_reduction = false

Whether we perform a transitive reduction of the binary implication graph after equivalent literal detection and before each probing pass.

Todo

(user): Doing that before the current SAT presolve also change the possible reduction. This shouldn't matter if we use the binary implication graph and its reachability instead of just binary clause though.

Definition at line 81 of file sat_inprocessing.h.

---

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

• ortools/sat/sat_inprocessing.h